Constraints: a uniform approach to aliasing and typing

ABSTRACT

A constraint is a relation among program variables that is maintained throughout execution. Type declarations and a very general form of aliasing can be expressed as constraints. A proof system based upon the interpretation of Hoare triples as temporal logic formulas is given for reasoning about programs with constraints. The proof system is shown to be sound and relatively complete, and example program proofs are given.

REFERENCES

• 1: Krzysztof R. Apt, Ten Years of Hoare's Logic: A Survey—Part I, ACM Transactions on Programming Languages and Systems (TOPLAS), v.3 n.4, p.431-483, Oct. 1981 [doi>10.1145/357146.357150]
• 2: Alan Borning, The Programming Language Aspects of ThingLab, a Constraint-Oriented Simulation Laboratory, ACM Transactions on Programming Languages and Systems (TOPLAS), v.3 n.4, p.353-387, Oct. 1981 [doi>10.1145/357146.357147]
• 3: [3] Stephen D. Brooks. A Fully Abstract Semantics And A Proof System For An ALGOL-like Language With Sharing. Preliminary Draft, Carnegie-Mellon University, Feb. 1984.
• 4: [4] R. Cartwright and D. Oppen. The Logic of Aliasing. Acta Informatica 15, (1981) 365-384.
• 5: J. W. de Bakker, Mathematical Theory of Program Correctness, Prentice-Hall, Inc., Upper Saddle River, NJ, 1980
• 6: Boris A. Trakhtenbrot , Joseph Y. Halpern , Albert R. Meyer, From Denotational to Operational and Axiomatic Semantics for ALGOL-like Languages: an Overview, Proceedings of the Carnegie Mellon Workshop on Logic of Programs, p.474-500, June 06-08, 1983
• 7: David Gries , Gary Levin, Assignment and Procedure Call Proof Rules, ACM Transactions on Programming Languages and Systems (TOPLAS), v.2 n.4, p.564-579, Oct. 1980 [doi>10.1145/357114.357119]
• 8: 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]
• 9: [9] C. A. R. Hoare. Procedures and Parameters: An Axiomatic Approach. Symposium on Semantics of Algorithmic Languages, Lecture Notes in Computer Science, Volume 88, Springer-Verlag, New York, 1971.
• 10: C. A. R. Hoare, Communicating sequential processes, Communications of the ACM, v.21 n.8, p.666-677, Aug. 1978 [doi>10.1145/359576.359585]
• 11: [11] C. A. R. Hoare and N. Wirth. An Axiomatic definition of the programming language Pascal. Acta Informatica 2 (1973), 335-355.
• 12: [12] L. Lamport. The "Hoare Logic" of Concurrent Programs. Acta Informatica 14 (1980), 21-37.
• 13: Leslie Lamport, Specifying Concurrent Program Modules, ACM Transactions on Programming Languages and Systems (TOPLAS), v.5 n.2, p.190-222, April 1983 [doi>10.1145/69624.357207]
• 14: Leslie Lamport , Fred B. Schneider, The ``Hoare Logic'' of CSP, and All That, ACM Transactions on Programming Languages and Systems (TOPLAS), v.6 n.2, p.281-296, April 1984 [doi>10.1145/2993.357247]
• 15: [15] L. Lamport and F. B. Schneider. Fully Compositional Generalized Hoare Logic. In preparation.
• 16: Susan Owicki , Leslie Lamport, Proving Liveness Properties of Concurrent Programs, ACM Transactions on Programming Languages and Systems (TOPLAS), v.4 n.3, p.455-495, July 1982 [doi>10.1145/357172.357178]
• 17: John C. Reynolds, The Craft of Programming, Prentice Hall PTR, Upper Saddle River, NJ, 1981
• 18: Richard D. Schlichting , Fred B. Schneider, Using message passing for distributed programming: proof rules and disciplines, ACM Transactions on Programming Languages and Systems (TOPLAS), v.6 n.3, p.402-431, July 1984 [doi>10.1145/579.583]
• 19: [19] R. M. Stallman and G. J. Sussman. Forward Reasoning and Dependency-Directed Backtracking in a System for Computer-Aided Circuit Analysis. Ariticial Intelligence 9, 1977, 135-196.
• 20: Guy Lewis Steele, Jr. , Gerald Jay Sussman, Constraints, Proceedings of the international conference on APL: part 1, p.208-225, May 30-June 01, 1979, New York, New York, United States
• 21: [21] G. J. Sussman, and R. M. Stallman. Heuristic Techniques in Computer-Aided Circuit Analysis. IEEE Transactions on Circuits and Systems CAS-22, 11 (November 1975).
• 22: [22] I. E. Sutherland. SKETCHPAD: A Man-Machine Graphical Communication System. M.I.T. Lincoln Laboratory Technical Report 296, (January 1963).

INDEX TERMS

Primary Classification:
  F. Theory of Computation
  F.4 MATHEMATICAL LOGIC AND FORMAL LANGUAGES
      F.4.1 Mathematical Logic
          Subjects: Logic and constraint programming

Additional Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.1 Formal Definitions and Theory
          Subjects: Semantics

  F. Theory of Computation
  F.1 COMPUTATION BY ABSTRACT DEVICES
      F.1.3 Complexity Measures and Classes
          Subjects: Reducibility and completeness

General Terms:
Design, Languages, Performance, Theory, Verification