@article {IOPORT.03961581, author = {Goldblatt, Robert}, title = {The semantics of Hoare's iteration rule.}, year = {1982}, journal = {Studia Logica}, volume = {41}, issn = {0039-3215}, pages = {141-158}, publisher = {Institute of Philosophy and Sociology of the Polish Academy of Sciences, Warsaw; Springer, Dordrecht}, doi = {10.1007/BF00370341}, abstract = {Summary: 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.}, identifier = {03961581}, }