A fully abstract semantics and a proof system for an algol-like language with sharing

  • Stephen D. Brookes
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 239)


In this paper we discuss the semantics of a simple block-structured programming language which allows sharing or aliasing. Sharing, which arises naturally in procedural languages which permit certain forms of parameter passing, has typically been regarded as problematical for the semantic treatment of a language. Difficulties have been encountered in both denotational and axiomatic treatments of sharing in the literature. Nevertheless, we find that it is possible to define a clean and elegant formal semantics for sharing. The key to our success is the choice of semantic model; we show that conventional approaches based on locations are less than satisfactory for the purposes of reasoning about partial correctness, and that in a well defined sense locations are unnecessary.

We begin by defining a denotational semantics for our programming language. The semantic model is not based on locations, but instead uses an abstract sharing relation on identifiers to represent the notion of aliasing, and uses an abstract state with a stack-like structure to capture the semantics of blocks and accurately model the scope rules. The semantics is shown to be fully abstract with respect to partial correctness properties, in contrast to conventional location-based models. This means that the semantics identifies terms if and only if they induce identical partial correctness behaviour in all program contexts. This property usually fails for location-based semantics because in such models it is possible to distinguish between terms on the basis of their effect on individual locations, which has no bearing on partial correctness.

We believe that axiomatic reasoning about program behaviour should be based directly on a semantic model specifically tailored for that purpose; full abstraction with respect to an appropriate behavioural notion is a formal criterion against which to judge the suitability of a semantics. The structure of a semantic model should be used directly to suggest the structure of an assertion language for expressing program properties. With this in mind, we build a Hoare-style (syntax-directed) proof system for partial correctness properties of our programming language, and we prove soundness and relative completeness of this system. The proof system is built up in a hierarchical manner which reflects the syntactic and semantic structure of the programming language. We first design a proof system for declarations, and then use it in building proof rules for commands. We claim that our proof rules are conceptually simpler to understand than other rules proposed in the literature for aliasing, without losing any expressive power. We show, for example, that it is possible to define a “generic” inference rule for blocks which is uniformly applicable to3 blocks headed by different forms of declaration. The important point here is that, unlike most of the proof systems for these constructs in the literature, we do not have to design a separate rule for blocks for each possible form of declaration. This results in greater flexibility and adaptability in our proof system. We demonstrate that some well known rules from the literature for blocks can be derived in our system.


Semantic Model Proof System Sequential Composition Sharing Relation Semantic Function 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

7. References

  1. [1]
    Apt, K. R., Ten Years of Hoare's Logic: A survey-Part 1, ACM TOPLAS, Vol. 3 pp 431–483 (1981).Google Scholar
  2. [2]
    de Bakker, J. W., Mathematical Theory of Program Correctness, Prentice-Hall 1980.Google Scholar
  3. [3]
    Cartwright, R., and Oppen, D., The Logic of Aliasing, Acta Informatica 15, pp 365–384 (1981).Google Scholar
  4. [4]
    Cartwright, R., and Oppen, D., Unrestricted Procedure Calls in Hoare's Logic, Proc. 5th ACM Symposium on Principles of Programming Languages, ACM New York.Google Scholar
  5. [5]
    Clarke, E. M., Programming language constructs for which it is impossible to obtain good Hoare axioms, JACM 26 pp 129–147 (1979).Google Scholar
  6. [6]
    Cook, S., Soundness and completeness of an axiom system for program verification, SIAM J. Comput. 7, pp 70–90 (1978).Google Scholar
  7. [7]
    Donahue, James, Locations Considered Unnecessary, Acta Informatica 8, pp 221–242 (1977).Google Scholar
  8. [8]
    Gordon, M., The Denotational Description of Programming Languages, Springer Verlag 1978.Google Scholar
  9. [9]
    Gries, D., The Multiple Assignment Statement, IEEE Trans. Software Engrg, SE-4, pp 89–93 (1978).Google Scholar
  10. [10]
    Gries, D., and Levin, G., Assignment and procedure call proof rules, ACM TOPLAS 2, pp 564–579 (1980).Google Scholar
  11. [11]
    Halpern, J., A Good Hoare Axiom System for an Algol-like language, Proc. POPL 1984.Google Scholar
  12. [12]
    Halpern, J., Meyer, A., and Trakhtenbrot, B., The Semantics of Local Storage, or What Makes the Free-list Free?, Proc. POPL 1984.Google Scholar
  13. [13]
    Halpern, J., Meyer, A., and Trakhtenbrot, B., From Denotational to Operational and Axiomatic Semantics for ALGOL-like languages: An Overview, Proc. 1983 Workshop on Logics of Programs, Springer Verlag LNCS 164 (1984).Google Scholar
  14. [14]
    Hoare, C. A. R., An Axiomatic Basis for Computer Programming, CACM 12, pp 576–580 (1969).Google Scholar
  15. [15]
    Hoare, C. A. R., Procedures and parameters: An axiomatic approach, in: Symposium on Semantics of Algorithmic Languages, Springer Verlag LNCS 188 (1971).Google Scholar
  16. [16]
    Jones, C. B., Yet Another Proof of the Correctness of Block Implementation, IBM Laboratory, Vienna (August 1970).Google Scholar
  17. [17]
    Landin, P. J., A Correspondence between Algol 60 and Church's lambda notation, CACM 8, 89–101 and 158–165 (1965).Google Scholar
  18. [18]
    Langmaack, H., On Termination Problems for Finitely Interpreted ALGOL-like Programs, Acta Informatica 18, pp 79–108 (1972).Google Scholar
  19. [19]
    Milne, R., and Strachey, C., A Theory of Programming Language Semantics, Chapman and Hall 1976.Google Scholar
  20. [20]
    Milner, R., Fully Abstract Models of Typed λ-calculi, Theoretical Computer Science (1977).Google Scholar
  21. [21]
    Mosses, P. D., The Mathematical Semantics of ALGOL 60, Technical Monograph PRG-12, Oxford University Computing Laboratory, Programming Research Group (1974).Google Scholar
  22. [22]
    Olderog, E-R., Correctness of Programs with Pascal-like Procedures without Global Variables, Theoretical Computer Science 30 (1984) 49–90.Google Scholar
  23. [23]
    Olderog, E-R., Sound and Complete Hoare-like Calculi Based on Copy Rules, Acta Informatica 16, pp 161–197 (1981).Google Scholar
  24. [24]
    Oles, F. J., A Category-theoretic Approach to the Semantics of ALGOL-like Languages, Ph. D. thesis, Syracuse University (August 1982).Google Scholar
  25. [25]
    Plotkin, G. D., LCF Considered as a Programming Language, Theoretical Computer Science 5, pp 223–255 (1977).Google Scholar
  26. [26]
    Plotkin, G. D., and Hennessy, M. C. B., Full Abstraction for a Simple Parallel Programming Language, Proc. MFCS 1979, Springer LNCS 74, pp 108–120 (1979).Google Scholar
  27. [27]
    Reynolds, J., The Craft of Programming, Prentice-Hall 1981.Google Scholar
  28. [28]
    Reynolds, J., Idealized Algol and its specification logic, Technical Report 1-81, Dept. of Computer and Information Science, Syracuse University (July 1981).Google Scholar
  29. [29]
    Reynolds, J., Syntactic control of interference, Proceedings of the 5th ACM Symposium on Principles of Programming Languages, ACM New York, pp 39–46 (1978).Google Scholar
  30. [30]
    Stoy, J. E., Denotational Semantics, MIT Press 1977.Google Scholar
  31. [31]
    Strachey, C., Towards a formal semantics, in: Formal Language Description Languages for Computer Programming, ed. T. B. Steel, Jr., North-Holland, Amsterdam (1966).Google Scholar
  32. [32]
    Tennent, R. D., Semantics of interference control, Theoretical Computer Science 27 (1983) 293–310.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1986

Authors and Affiliations

  • Stephen D. Brookes
    • 1
  1. 1.Computer Science DepartmentCarnegie-Mellon UniversityPittsburgh

Personalised recommendations