The semantics of Hoare's Iteration Rule |
| |
Authors: | Robert Goldblatt |
| |
Institution: | (1) Mathematics Department, Victoria University, Private Bag, Wellington, New Zealand |
| |
Abstract: | Hoare's Iteration Rule is a principle of reasoning that is used to derive correctness assertions about the effects of implementing a while-command. We show that the propositional modal logic of this type of command is axiomatised by Hoare's rule in conjunction with two additional axioms. The proof also establishes decidability of the logic. The paper concludes with a discussion of the relationship between the logic of while and Segerberg's axiomatisation of propositional dynamic logic. |
| |
Keywords: | |
本文献已被 SpringerLink 等数据库收录! |
|