Axiomatic definitions of programming languages, II

ABSTRACT

Sufficient conditions are given for partial correctness assertions to determine the input-output semantics of quite general classes of programming languages. This determination cannot be unique unless states which are indistinguishable by predicates in the assertions are identified. Even when indistinguishable states are identified, partial correctness assertions may not suffice to determine program semantics.

REFERENCES

• 1: {A} Apt, K. R. Ten Years of Hoare's Logic, A survey, Part I, 5thScandinavian Logic Symposium, Jan. 1979, Aalborg, Denmark; revised manuscript September, 1979, 49pp.
• 2: {BTT} Bergstra, J. A., J. Tiuryn, and J. V. Tucker. Correctness Theories and Program Equivalence, Preprint, Stichting Mathematisch Centrum, Amsterdam, 1979.
• 3: {C} Cook, S. A. Soundness and Completeness of an axiom system for program verification, SIAM J. Computing, 7,1(1978), 70-90.
• 4: I. Greif , A. Meyer, Specifying programming language semantics: a tutorial and critique of a paper by Hoare and Lauer, Proceedings of the 6th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.180-189, January 29-31, 1979, San Antonio, Texas [doi>10.1145/567752.567769]
• 5: D. Harel , A. R. Meyer , V. R. Pratt, Computability and completeness in logics of programs (Preliminary Report), Proceedings of the ninth annual ACM symposium on Theory of computing, p.261-268, May 04-04, 1977, Boulder, Colorado, United States [doi>10.1145/800105.803416]
• 6: Albert R. Meyer , Joseph Y. Halpern, Axiomatic definitions of programming languages: a theoretical assessment (preliminary report), Proceedings of the 7th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.203-212, January 28-30, 1980, Las Vegas, Nevada [doi>10.1145/567446.567466]
• 7: Albert R. Meyer , Karl Winklmann, On the expressive power of Dynamic Logic (Preliminary Report), Proceedings of the eleventh annual ACM symposium on Theory of computing, p.167-175, April 30-May 02, 1979, Atlanta, Georgia, United States [doi>10.1145/800135.804410]