On the Sequence Rule for the Floyd-Hoare Logic with Partial Pre- and Post-Conditions
Ievgen Ivanov, Mykola S. Nikitchenko · 2017
Classical Floyd-Hoare logic is valid when total pre- and post- conditions are considered. In the case of partial conditions (predicates) the logic becomes invalid. This situation may be corrected by introducing additional constraints for the rules of the logic. But such constraints, especially for the sequence and while rules, are rather complicated. In this paper we propose a new simpler sequence rule formulated in an extended program algebra. The same considerations also allow to reformulate the while rule. The obtained results can be useful for software verification.