Substructural logic and partial correctness

ABSTRACT

We formulate a noncommutative sequent calculus for partial correctness that subsumes propositional Hoare Logic. Partial correctness assertions are represented by intuitionistic linear implication. We prove soundness and completeness over relational and trace models. As a corollary, we obtain a complete sequent calculus for inclusion and equivalence of regular expressions.

REFERENCES

• 1: Artemov, S. 2001. Explicit provability and constructive semantics. Bull. Symb. Logic 7, 1 (Mar.), 1--36.
• 2: Boffa, M. 1990. Une remarque sur les systèmes complets d'identités rationnelles. Informat. Théoret. Appl./Theoret. Informat. Appl. 24, 4, 419--423.
• 3: Boffa, M. 1995. Une condition impliquant toutes les identités rationnelles. Informat. Théoret. Appl./Theoret. Informat. Appl. 29, 6, 515--518.
• 4: Conway, J. H. 1971. Regular Algebra and Finite Machines. Chapman and Hall, London, England.
• 5: Fischer, M. J. and Ladner, R. E. 1979. Propositional dynamic logic of regular programs. J. Comput. Syst. Sci. 18, 2, 194--211.
• 6: Jean-Yves Girard, Linear logic, Theoretical Computer Science, v.50 n.1, p.1-102, Jan. 30, 1987 [doi>10.1016/0304-3975(87)90045-4]
• 7: Gödel, K. 1933. Eine Interpretation des intuitionistischen Aussagenkalküls. Ergebnisse eines mathematischen Kolloquiums 4, 39--40. (Reprinted in: S. Feferman, Ed., Collected Works of Kurt Gödel, vol. 1, Oxford University Press, New York, 1986.)
• 8: David Harel , Jerzy Tiuryn , Dexter Kozen, Dynamic Logic, MIT Press, Cambridge, MA, 2000
• 9: P. T. Johnstone, Notes on logic and set theory, Cambridge University Press, New York, NY, 1987
• 10: Kaplan, D. M. 1969. Regular expressions and the equivalence of programs. J. Comput. Syst. Sci. 3, 361--386.
• 11: Dexter Kozen, On action algebras, Logic and information flow, MIT Press, Cambridge, MA, 1994
• 12: 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]
• 13: Dexter Kozen, On Hoare logic and Kleene algebra with tests, ACM Transactions on Computational Logic (TOCL), v.1 n.1, p.60-76, July 2000 [doi>10.1145/343369.343378]
• 14: Dexter Kozen, Automata on Guarded Strings and Applications, Cornell University, Ithaca, NY, 2001
• 15: Dexter Kozen , Maria-Christina Patron, Certification of Compiler Optimizations Using Kleene Algebra with Tests, Proceedings of the First International Conference on Computational Logic, p.568-582, July 01, 2000
• 16: 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
• 17: Kozen, D. and Tiuryn, J. 2001. On the completeness of propositional Hoare logic. Inf. Sci. 139, 3--4, 187--195.
• 18: Kripke, S. 1963. Semantic analysis of modal logic. Z. Math. Logik Grundlagen Math. 9, 67--96.
• 19: Kripke, S. 1965. Semantical analysis of intuitionistic logic I. In Formal Systems and Recursive Functions, J. N. Crossley and M. A. E. Dummett, Eds. North-Holland, Amsterdam, The Netherlands, 92--130.
• 20: Daniel Krob, Complete systems of B -rational identities, Theoretical Computer Science, v.89 n.2, p.207-343, Oct. 28, 1991 [doi>10.1016/0304-3975(91)90395-I]
• 21: Vaughan Pratt, Action logic and pure induction, Proceedings of the European workshop on Logics in AI, p.97-120, March 1991, Amsterdam, The Netherlands
• 22: Restall, G. 2000. An Introduction to Substructural Logics. Routledge.
• 23: Troelstra, A. S. 1992. Lectures on Linear Logic. CSLI Lecture Notes, vol. 29. Center for the Study of Language and Information.
• 24: Yetter, D. N. 1990. Quantales and (noncommutative) linear logic. J. Symbol. Logic 55, 41--64.

INDEX TERMS

Primary Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.2 Design Tools and Techniques

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: Assertions; Logics of programs; Specification techniques; Mechanical verification; Pre- and post-conditions; 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 transformation; Program synthesis; Program modification; Program verification

General Terms:
Theory, Verification

Keywords:
Dynamic logic, Hoare logic, Kleene algebra, Kleene algebra with tests, linear logic, sequent calculus, specification, substructural logic