Towards fully abstract semantics for local variables

ABSTRACT

The Store Model of Halpern-Meyer-Trakhtenbrot is shown—after suitable repair—to be a fully abstract model for a limited fragment of ALGOL in which procedures do not take procedure parameters. A simple counter-example involving a parameter of program type shows that the model is not fully abstract in general. Previous proof systems for reasoning about procedures are typically sound for the HMT store model, so it follows that theorems about the counter-example are independent of such proof systems. Based on a generalization of standard cpo based models to structures called locally complete partial orders (lcpo's), improved models and stronger proof rules are developed to handle such examples.

REFERENCES

• 1: G. Berry, P. Curien, and J. L6vy. Full abstraction for sequential languages: the state of the page 0, Cambridge Univ. Press, 1985.
• 2: Edmund Melson Clarke, Jr., Programming Language Constructs for Which It Is Impossible To Obtain Good Hoare Axiom Systems, Journal of the ACM (JACM), v.26 n.1, p.129-147, Jan. 1979 [doi>10.1145/322108.322121]
• 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: W. Datum. The iO- and OI-hierarchies. Theoretical Computer Sci., 20:95-207, 1982.
• 5: W. Datum and E. Fehr. A schematological approach to the analysis of the procedure concept in ALGoL-languages. In 5i~h~ Coll. sur les Arbes en Algebre et en Programmation, pages 130- 134, Lille, 1980.
• 6: J. W. de Bakker, Mathematical Theory of Program Correctness, Prentice-Hall, Inc., Upper Saddle River, NJ, 1980
• 7: Steven M. German , Edmund M. Clarke , Joseph Y. Halpern, Reasoning About Procedures as Parameters, Proceedings of the Carnegie Mellon Workshop on Logic of Programs, p.206-220, June 06-08, 1983
• 8: A. Goerdt. Hoare logic for lambda-terms as basis of Itoare logic for imperative languages. In Syrup. Logic in Computer Sci., pages 293-299, IEEE, 1987.
• 9: Michael J. C. Gordon, The Denotational Description of Programming Languages: An Introduction, Springer-Verlag New York, Inc., Secaucus, NJ, 1979
• 10: Joseph Y. Halpern , Albert R. Meyer , B. A. Trakhtenbrot, The semantics of local storage, or what makes the free-list free?(Preliminary Report), Proceedings of the 11th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.245-257, January 15-18, 1984, Salt Lake City, Utah, United States [doi>10.1145/800017.800536]
• 11: Z. Manna and R. Waldinger. Problematic features of programming languages: a situationalcalculus approach. Acta Informatica, 16:371-426, 1981.
• 12: Robert Milne , C. Strachey, A Theory of Programming Language Semantics, Halsted Press, New York, NY, 1977
• 13: Ketan D. Mulmuley, Full abstraction and semantic equivalence, 1985
• 14: Michael J. O'Donnell, A critique of the foundations of Hoare style programming logics, Communications of the ACM, v.25 n.12, p.927-935, Dec 1982 [doi>10.1145/358728.358748]
• 15: Ernst-Rüdiger Olderog, A characterization of Hoare's logic for programs with Pascal-like procedures, Proceedings of the fifteenth annual ACM symposium on Theory of computing, p.320-329, December 1983 [doi>10.1145/800061.808761]
• 16: E. Olderog. Correctness of programs with PASCAL-like procedures without global variables. Theoretical Computer Sci., 30:49-90, 1984.
• 17: Ernst-Rüdiger Olderog, Hoare's Logic for Programs with Procedures - What Has Been Achieved?, Proceedings of the Carnegie Mellon Workshop on Logic of Programs, p.383-395, June 06-08, 1983
• 18: Frank Joseph Oles, A category-theoretic approach to the semantics of programming languages, 1982
• 19: F J Oles, Type algebras, functor categories and block structure, Algebraic methods in semantics, Cambridge University Press, New York, NY, 1986
• 20: G. D. Plotkin. LCF considered as a programming language. Theoretical Computer Sci., 5:223- 256, 1977.
• 21: John C. Reynolds, The Craft of Programming, Prentice Hall PTR, Upper Saddle River, NJ, 1981
• 22: J. C. Reynolds. The essence of ALGOL. In J. DeBakker and van Vliet, editors, Int'l. Symp. Algorithmic Languages, pages 345-372, IFIP, North-Holland, 1981.
• 23: J. C. Reynolds. Idealized ALGOL and its specification logic. In D. N6el, editor, Tools and Notions for Program Construction, pages 121-161, Cambridge Univ. Press, 1982.
• 24: Richard L. Schwartz, An Aximatic Treatment of Algol 68 Routines, Proceedings of the 6th Colloquium, on Automata, Languages and Programming, p.530-545, July 16-20, 1979
• 25: K. Sieber. A partial correctness logic for programs (in an ALGOL-like language).. In R. Parikh, editor, Logics of Programs, pages 320-342, Volume 193 of Lect. Notes in Computer Sci., Springer-Verlag, 1985.
• 26: Robert D. Tennent, Semantical Analysis of Specification Logic, Proceedings of the Conference on Logic of Programs, p.373-386, June 17-19, 1985
• 27: R. D. Tennent. Semantical analysis of specification logic. 1987. Submitted, 22 pp.
• 28: 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

INDEX TERMS

Primary Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES

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

          Nouns: ALGOL

General Terms:
Languages, Theory