On Hoare logic and Kleene algebra with tests

ABSTRACT

We show that Kleene algebra with tests (KAT) subsumes propositional Hoare logic (PHL). Thus the specialized syntax and deductive apparatus of Hoare logic are inessential and can be replaced by simple equational reasoning. In addition, we show that all relationally valid inference rules are derivable in KAT and that deciding the relational validity of such rules is PSPACE-complete.

REFERENCES

• 1: Stephen L. Bloom , Zoltán Ésik, Floyd-Hoare logic in iteration theories, Journal of the ACM (JACM), v.38 n.4, p.887-934, Oct. 1991 [doi>10.1145/115234.115352]
• 2: Stephen L Bloom , Zoltán Ésik, Program Correctness and Matricial Iteration Theories, Proceedings of the 7th International Conference on Mathematical Foundations of Programming Semantics, p.457-476, March 25-28, 1991
• 3: Edmund M. Clarke, Jr. , Steven M. German , Joseph Y. Halpern, Effective Axiomatizations of Hoare Logics, Journal of the ACM (JACM), v.30 n.3, p.612-636, July 1983 [doi>10.1145/2402.322394]
• 4: COHEN, E. 1994. Hypotheses in Kleene algebra. Available as ftp://ftp.telcordia.com/pub/ernie/ research/homepage.html.
• 5: Ernie Cohen , Dexter Kozen , Frederick Smith, The Complexity of Kleene Algebra with Tests, Cornell University, Ithaca, NY, 1996
• 6: CONWAY, J. H. 1971. Regular Algebra and Finite Machines. Chapman and Hall, Ltd., London, UK.
• 7: COOK, S.A. 1978. Soundness and completeness of an axiom system for program verification. SIAM J. Comput. 7, 1 (Feb.), 70-90.
• 8: Patrick Coust, Methods and logics for proving programs, Handbook of theoretical computer science (vol. B): formal models and semantics, MIT Press, Cambridge, MA, 1991
• 9: FISCHER, M. J. AND LADNER, R. E. 1979. Propositional dynamic logic of regular programs. J. Comput. Syst. Sci. 18, 2, 194-211.
• 10: Joseph A. Goguen , Grant Malcolm, Algebraic Semantics of Imperative Programs, MIT Press, Cambridge, MA, 1996
• 11: HALPERN, J. Y. AND REIF, J. H. 1983. The propositional logic of deterministic, well-structured programs. Theor. Comput. Sci. 27, 127-165.
• 12: C. A. R. Hoare, An axiomatic basis for computer programming, Communications of the ACM, v.12 n.10, p.576-580, Oct. 1969 [doi>10.1145/363235.363259]
• 13: Kazuo Iwano , Kenneth Steiglitz, A semiring on convex polygons and zero-sum cycle problems, SIAM Journal on Computing, v.19 n.5, p.883-901, Oct. 1990 [doi>10.1137/0219061]
• 14: KLEENE, S. C. 1956. Representation of events in nerve nets and finite automata. In Automata Studies, C. E. Shannon and J. McCarthy, Eds. Princeton University Press, Princeton, NJ, 3-41.
• 15: Dexter Kozen, A completeness theorem for Kleene algebras and the algebra of regular events, Information and Computation, v.110 n.2, p.366-390, May 1, 1994
• 16: Dexter Kozen, Kleene algebra with tests, ACM Transactions on Programming Languages and Systems (TOPLAS), v.19 n.3, p.427-443, May 1997 [doi>10.1145/256167.256195]
• 17: Dexter Kozen , Frederick Smith, Kleene Algebra with Tests: Completeness and Decidability, Selected Papers from the10th International Workshop on Computer Science Logic, p.244-259, September 21-27, 1996
• 18: Michael G. Main , David L. Black, Semantic models for total correctness and fairness, Proceedings of the fifth international conference on Mathematical foundations of programming semantics, p.247-270, July 1990, New Orleans, Louisiana, United States
• 19: Ernest G. Manes , Michael A. Arbib, Algebraic approaches to program semantics, Springer-Verlag New York, Inc., New York, NY, 1986
• 20: Michael J. O'Donnell, Equational logic as a programming language, Massachusetts Institute of Technology, Cambridge, MA, 1985
• 21: V. R. Pratt, A practical decision method for propositional dynamic logic (Preliminary Report), Proceedings of the tenth annual ACM symposium on Theory of computing, p.326-337, May 01-03, 1978, San Diego, California, United States [doi>10.1145/800133.804362]
• 22: TAYLOR, W. 1979. Equational logic. Houston J. Math., i-83. Survey.

INDEX TERMS

Primary Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.2 Design Tools and Techniques
          Subjects: Structured programming**

Additional Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification
          Subjects: Correctness proofs
  D.3 PROGRAMMING LANGUAGES
      D.3.3 Language Constructs and Features
          Subjects: Control structures

  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.1 Specifying and Verifying and Reasoning about Programs
          Subjects: Pre- and post-conditions; Assertions; Logics of programs; Specification techniques; Mechanical verification; Invariants
      F.3.2 Semantics of Programming Languages
          Subjects: Algebraic approaches to semantics
      F.3.3 Studies of Program Constructs
          Subjects: Control primitives

  I. Computing Methodologies
  I.1 SYMBOLIC AND ALGEBRAIC MANIPULATION
      I.1.1 Expressions and Their Representation
          Subjects: Simplification of expressions
      I.1.3 Languages and Systems
          Subjects: Special-purpose algebraic systems
  I.2 ARTIFICIAL INTELLIGENCE
      I.2.2 Automatic Programming
          Subjects: Program verification; Program transformation; Program modification; Program synthesis

General Terms:
Design, Languages, Theory, Verification

Keywords:
Hoare logic, Kleene algebra, Kleene algebra with tests, dynamic logic, specification