Term transformers: A new approach to state

ABSTRACT

We present a new approach to adding state and state-changing commands to a term language. As a formal semantics it can be seen as a generalization of predicate transformer semantics, but beyond that it brings additional opportunities for specifying and verifying programs. It is based on a construct called a phrase, which is a term of the form C ▹ t, where C stands for a command and t stands for a term of any type. If R is boolean, C ▹ R is closely related to the weakest precondition wp(C,R). The new theory draws together functional and imperative programming in a simple way. In particular, imperative procedures and functions are seen to be governed by the same laws as classical functions. We get new techniques for reasoning about programs, including the ability to dispense with logical variables and their attendant complexities. The theory covers both programming and specification languages, and supports unbounded demonic and angelic nondeterminacy in both commands and terms.

REFERENCES

• 1: Ralph-Johan J. Back , Abo Akademi , J. Von Wright , F. B. Schneider , D. Gries, Refinement Calculus: A Systematic Introduction, Springer-Verlag New York, Inc., Secaucus, NJ, 1998
• 2: Back, R.-J. R. 1980. Correctness preserving program refinements: Proof theory and applications. Tract 131, Mathematisch Centrum, Amsterdam.
• 3: R. J. R. Back , J. von Wright, Duality in specification languages: a lattice-theoretical approach, Acta Informatica, v.27 n.7, p.583-625, 1990
• 4: Roland Backhouse, Program Construction: Calculating Implementations from Specifications, John Wiley & Sons, Inc., New York, NY, 2003
• 5: Bijlsma, L. and Nederpelt, R. 1998. Dijkstra-Scholten predicate calculus: Concepts and misconceptions. Acta Inf. 35, 1007--1036.
• 6: Sascha Böhme , K. Rustan Leino , Burkhart Wolff, HOL-Boogie -- An Interactive Prover for the Boogie Program-Verifier, Proceedings of the 21st International Conference on Theorem Proving in Higher Order Logics, August 18-21, 2008, Montreal, P.Q., Canada [doi>10.1007/978-3-540-71067-7_15]
• 7: H. J. Boom, A Weaker Precondition for Loops, ACM Transactions on Programming Languages and Systems (TOPLAS), v.4 n.4, p.668-677, Oct. 1982 [doi>10.1145/69622.357189]
• 8: Raymond Boute, Functional declarative language design and predicate calculus: a practical approach, ACM Transactions on Programming Languages and Systems (TOPLAS), v.27 n.5, p.988-1047, September 2005 [doi>10.1145/1086642.1086647]
• 9: Bunkenburg, A. 1997. Expression refinement. Ph.D. thesis, Computing Science Department, University of Glasgow.
• 10: Edward Cohen, Programming in the 1990s: an introduction to the calculation of programs, Springer-Verlag New York, Inc., New York, NY, 1990
• 11: David Detlefs , Greg Nelson , James B. Saxe, Simplify: a theorem prover for program checking, Journal of the ACM (JACM), v.52 n.3, p.365-473, May 2005 [doi>10.1145/1066100.1066102]
• 12: Edsger Wybe Dijkstra, A Discipline of Programming, Prentice Hall PTR, Upper Saddle River, NJ, 1997
• 13: Edsger W. Dijkstra, Selected writings on computing: a personal perspective, Springer-Verlag New York, Inc., New York, NY, 1982
• 14: Edsger W. Dijkstra , Carel S. Scholten, Predicate calculus and program semantics, Springer-Verlag New York, Inc., New York, NY, 1990
• 15: E W Dijkstra , A J M van Gasteren, A simple fixpoint argument without the restriction to continuity, Acta Informatica, v.23 n.1, p.1-7, April 1986 [doi>10.1007/BF00268074]
• 16: Robert W. Floyd, Nondeterministic Algorithms, Journal of the ACM (JACM), v.14 n.4, p.636-644, Oct. 1967 [doi>10.1145/321420.321422]
• 17: Paul Gardiner , Carroll Morgan, Data refinement of predicate transformers, Theoretical Computer Science, v.87 n.1, p.143-162, Sept. 16, 1991 [doi>10.1016/0304-3975(91)90029-2]
• 18: David Gries, The Science of Programming, Springer-Verlag New York, Inc., Secaucus, NJ, 1987
• 19: David Gries , Fred B. Schneider, A logical approach to discrete math, Springer-Verlag New York, Inc., New York, NY, 1993
• 20: Eric C.R. Hehner, The logic of programming, Prentice-Hall, Inc., Upper Saddle River, NJ, 1984
• 21: Eric C. R. Hehner, A practical theory of programming, Springer-Verlag New York, Inc., New York, NY, 1993
• 22: Hitchcock, P. and Park, D. 1972. Induction rules and termination proofs. In IRIA Conference on Automata, Languages, and Programming Theory. North-Holland, Amsterdam, 225--251.
• 23: 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]
• 24: Anne Kaldewaij, Programming: the derivation of algorithms, Prentice-Hall, Inc., Upper Saddle River, NJ, 1990
• 25: Kleymann, T. 1999. Hoare logic and auxiliary variables. Formal Aspects Comput. 11, 5, 541--566.
• 26: John Launchbury , Simon L. Peyton Jones, Lazy functional state threads, Proceedings of the ACM SIGPLAN 1994 conference on Programming language design and implementation, p.24-35, June 20-24, 1994, Orlando, Florida, United States
• 27: E. Moggi, Computational lambda-calculus and monads, Proceedings of the Fourth Annual Symposium on Logic in computer science, p.14-23, June 1989, Pacific Grove, California, United States
• 28: C. Morgan, Auxiliary variables in data refinement, Information Processing Letters, v.29 n.6, p.293-296, Dec. 8, 1988 [doi>10.1016/0020-0190(88)90227-X]
• 29: Carroll Morgan, Programming from specifications (2nd ed.), Prentice Hall International (UK) Ltd., Hertfordshire, UK, 1994
• 30: Joseph M. Morris, A theoretical basis for stepwise refinement and the programming calculus, Science of Computer Programming, v.9 n.3, p.287-306, December 1, 1987 [doi>10.1016/0167-6423(87)90011-6]
• 31: Joseph M. Morris , Malcolm Tyrrell, Dual unbounded nondeterminacy, recursion, and fixpoints, Acta Informatica, v.44 n.5, p.323-344, August 2007 [doi>10.1007/s00236-007-0049-9]
• 32: Joseph M. Morris , Malcolm Tyrrell, Dually nondeterministic functions, ACM Transactions on Programming Languages and Systems (TOPLAS), v.30 n.6, p.1-34, October 2008 [doi>10.1145/1391956.1391961]
• 33: David A. Naumann, Calculating sharp adaptation rules, Information Processing Letters, v.77 n.2-4, p.201-208, Feb. 1, 2001 [doi>10.1016/S0020-0190(00)00215-5]
• 34: David A. Naumann, Ideal models for pointwise relational and state-free imperative programming, Proceedings of the 3rd ACM SIGPLAN international conference on Principles and practice of declarative programming, p.4-15, September 05-07, 2001, Florence, Italy [doi>10.1145/773184.773186]
• 35: David A. Naumann, Predicate transformer semantics of a higher-order imperative language with record subtyping, Science of Computer Programming, v.41 n.1, p.1-51, September 2001 [doi>10.1016/S0167-6423(00)00005-8]
• 36: Greg Nelson, A generalization of Dijkstra's calculus, ACM Transactions on Programming Languages and Systems (TOPLAS), v.11 n.4, p.517-561, Oct. 1989 [doi>10.1145/69558.69559]
• 37: Nelson, G. 1992. Some generalizations and applications of Dijkstra's guarded commands. In Programming and Mathematical Methods, M. Broy, Ed. NATO ASI Series F: Computer and Systems Sciences, vol. 88. Springer-Verlag, New York.
• 38: Helmut A. Partsch, Specification and transformation of programs: a formal approach to software development, Springer-Verlag New York, Inc., New York, NY, 1990
• 39: Pierik, C. and de Boer, F. S. 2004. Modularity and the rule of adaptation. In Algebraic Methodology and Software Technology, 10th International Conference, C. Rattray, et al., Eds. Lecture Notes in Computer Science, vol. 3116. Springer-Verlag, New York, 394--408.
• 40: J. M. Spivey, Understanding Z: a specification language and its formal semantics, Cambridge University Press, New York, NY, 1988
• 41: Tarski, A. 1955. A lattice-theoretical fixpoint theorem and its applications. Pacific J. Math. 5, 285--309.
• 42: Tunnicliffe, W. R. 1985. The free completely distributive lattice over a poset. Algebra Universalis 21, 133--135.
• 43: J. von Wright, The lattice of data refinement, Acta Informatica, v.31 n.2, p.105-135, Feb. 1994 [doi>10.1007/BF01192157]
• 44: Philip Wadler, The essence of functional programming, Proceedings of the 19th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.1-14, January 19-22, 1992, Albuquerque, New Mexico, United States [doi>10.1145/143165.143169]
• 45: Jim Woodcock , Martin Loomes, Software engineering mathematics, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1990

INDEX TERMS

Primary Classification:
  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.1 Specifying and Verifying and Reasoning about Programs
          Subjects: Logics of programs

Additional Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification
          Subjects: Correctness proofs; Formal methods

General Terms:
Design, Theory, Verification

Keywords:
Nondeterminacy, nondeterminism, predicate transformers, procedures, refinement calculus, state