Article

Free access

Axiomatic definitions of programming languages: a theoretical assessment (preliminary report)

Authors:

Albert R. Meyer,

Joseph Y. HalpernAuthors Info & Claims

POPL '80: Proceedings of the 7th ACM SIGPLAN-SIGACT symposium on Principles of programming languages

Pages 203 - 212

https://doi.org/10.1145/567446.567466

Published: 28 January 1980 Publication History

Abstract

A precise definition is given of how partial correctness or termination assertions serve to specify the semantics of classes of program schemes. Assertions involving only formulas of first order predicate calculus are proved capable of specifying program scheme semantics, and effective axiom systems for deriving such assertions are described. Such axiomatic specifications are possible despite the limited expressive power of predicate calculus.

References

[1]

Apt, K. R., J. A. Bergstra, L. G. L. T. Meertens. Recursive Assertions Are Not Enough - Or Are They? Theoretical Computer Science, in vol. 8, pp. 73-87, 1979.

[2]

Bergstra, J. A., J. Tiuryn, and J. V. Tucker. Correctness Theories and Program Equivalence. Preprint. Stichting Mathematisch Centrum, Amsterdam, 1979.

[3]

Cook, S. A. Soundness and Completeness of an Axiom System for Program Verification. SIAM Journal on Computing, vol. 7, no. 1. February, 1978.

[4]

Dijkstra, E. W. Guarded Commands, Nondeterminacy and Formal Derivation of Programs. Comm. of the A.C.M. vol 18, no. 8, 1975.

Digital Library

[5]

Dijkstra, E. W. A Discipline of Programming. Prentice-Hall, 1976.

Digital Library

[6]

Floyd, R. W. Assigning Meaning to Programs. In Mathematical Aspects of Computer Science. Proceedings of Symposium in Applied Mathematics (ed. J. T. Schwartz). (pp. 19-33) American Math. Society, Providence, Rhode Island, 1967.

[7]

Friedman, H. Algorithmic Procedures, Generalized Turing Algorithms, and Elementary Recursion Theory. In Logic colloquiuum, 1969 (ed. R. O. Gandy and C. M. E. Yates) (pp. 316-389). North Holland, Amsterdam, 1971.

[8]

Greif, I. and A. R. Meyer. Specifying the Semantics of While-Programs. M.I.T., Laboratory for Computer Science, TM-130. M.I.T., Cambridge, Mass. 02139, April, 1979.

[9]

Harel, D. Logics of Programs: Axiomatics and Descriptive Power. M.I.T., Laboratory for Computer Science, TR-200. M.I.T., Cambridge, Mass. 02139. May, 1978.

Digital Library

[10]

Harel, D., A. R. Meyer, and V. R. Pratt. Computability and Completeness in Logics of Programs. Proceedings of Ninth Annual A.C.M. Symposium on Theory of Computing. Boulder, Colorado. May, 1977.

Digital Library

[11]

Hoare, C. A. R. and P. Lauer. Consistent and Complementary Formal Theories of the Semantics of Programming Languages. Acta Informatica 3, pp 135-155, 1974.

Digital Library

[12]

Hoare, C. A. R. and N. Wirth. An Axiomatic Definition of the Programming Language PASCAL. Acta Informatica 2, pp. 335-355, 1973.

Digital Library

[13]

Janssen, T. M. V. and P. van Emde Boas. The Expressive Power of Intensional Logic in the Semantics of Programming Languages. Preprint. Stichting Mathematisch Centrum, Amsterdam, May, 1977.

[14]

Kleene, S. C. Two Papers on the Predicate Calculus. Memoirs of the American Math. Soc., No. 10. (pp. 27-66). American Math. Society Providence, Rhode Island, 1952.

[15]

London, Ralph L. Program Verification In Research Directions in Software Technology. ed. Peter Wegner. (pp. 302-315). M.I.T. Press, Cambridge, Mass., 1978.

[16]

Machtey, M. and P. Young. An Introduction to the General Theory of Algorithms. North Holland, 1978.

Digital Library

[17]

Pratt, V. R. Semantical Considerations of Floyd-Hoare Logic. 17th Annual IEEE Symposium on the Foundations of Computer Science. pp. 109-121, October, 1976.

[18]

Schwartz, R. An Axiomatic Semantic Definition of Algol 68. UCLA-ENG-7838; UCLA-34P214-75, University of California at Los Angeles, Los Angeles, Calif. 1978.

Cited By

Dodig Crnkovic GBurgin M(2012)Unconventional Algorithms: Complementarity of Axiomatics and ConstructionEntropy10.3390/e1411206614:11(2066-2080)Online publication date: 25-Oct-2012
https://doi.org/10.3390/e14112066
Tiuryn J(2005)A survey of the logic of effective definitionsLogic of Programs10.1007/3-540-11160-3_7(198-245)Online publication date: 30-May-2005
https://doi.org/10.1007/3-540-11160-3_7
Moriconi MSchwartz R(2005)Automatic construction of verification condition generators from hoare logicsAutomata, Languages and Programming10.1007/3-540-10843-2_30(363-377)Online publication date: 25-May-2005
https://doi.org/10.1007/3-540-10843-2_30
Show More Cited By

Axiomatic definitions of programming languages: a theoretical assessment (preliminary report)
1. Theory of computation

Recommendations

Higher-order logic programming languages with constraints: a semantics
TLCA'07: Proceedings of the 8th international conference on Typed lambda calculi and applications

A Kripke Semantics is defined for a higher-order logic programming language with constraints, based on Church's Theory of Types and a generic constraint formalism.

Our syntactic formal system, hoHH(C) (higher-order hereditary Harrop formulas with ...
Formal Logic Definitions for Interchange Languages
Proceedings of the International Conference on Intelligent Computer Mathematics - Volume 9150

System integration often requires standardized interchange languages, via which systems can exchange mathematical knowledge. Major examples are the MathML-based markup languages and TPTP. However, these languages standardize only the syntax of the ...
A logic of nonmonotone inductive definitions

Well-known principles of induction include monotone induction and different sorts of nonmonotone induction such as inflationary induction, induction over well-founded sets and iterated induction. In this work, we define a logic formalizing induction ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

POPL '80: Proceedings of the 7th ACM SIGPLAN-SIGACT symposium on Principles of programming languages

January 1980

261 pages

ISBN:0897910117

DOI:10.1145/567446

Conference Chairs:
Paul Abrahams
Courant Institute, New York, NY
,
Richard Lipton
University of California at Berkeley, Berkeley, CA
,
Program Chair:
Stephen Bourne
Bell Laboratories, Murray Hill, NJ

Copyright © 1980 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Sponsors

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 28 January 1980

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Qualifiers

Article

Acceptance Rates

Overall Acceptance Rate 824 of 4,130 submissions, 20%

Upcoming Conference

POPL '25

Sponsor:
sigplan

The 52nd Annual ACM SIGPLAN Symposium on Principles of Programming Languages

January 19 - 25, 2025

Denver , CO , USA

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

9
Total Citations
View Citations
337
Total Downloads

Downloads (Last 12 months)75
Downloads (Last 6 weeks)12

Reflects downloads up to 14 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

Dodig Crnkovic GBurgin M(2012)Unconventional Algorithms: Complementarity of Axiomatics and ConstructionEntropy10.3390/e1411206614:11(2066-2080)Online publication date: 25-Oct-2012
https://doi.org/10.3390/e14112066
Tiuryn J(2005)A survey of the logic of effective definitionsLogic of Programs10.1007/3-540-11160-3_7(198-245)Online publication date: 30-May-2005
https://doi.org/10.1007/3-540-11160-3_7
Moriconi MSchwartz R(2005)Automatic construction of verification condition generators from hoare logicsAutomata, Languages and Programming10.1007/3-540-10843-2_30(363-377)Online publication date: 25-May-2005
https://doi.org/10.1007/3-540-10843-2_30
Bergstra JTucker J(1984)The axiomatic semantics of programs based on Hoare's logicActa Informatica10.1007/BF0026425221:3(293-320)Online publication date: 1-Oct-1984
https://dl.acm.org/doi/10.1007/BF00264252
Meyer AMitchell JDeMillo R(1982)Axiomatic definability and completeness for recursive programsProceedings of the 9th ACM SIGPLAN-SIGACT symposium on Principles of programming languages10.1145/582153.582188(337-346)Online publication date: 25-Jan-1982
https://dl.acm.org/doi/10.1145/582153.582188
Clarke EGerman SHalpern JDeMillo R(1982)On effective axiomatizations of Hoare logicsProceedings of the 9th ACM SIGPLAN-SIGACT symposium on Principles of programming languages10.1145/582153.582186(309-321)Online publication date: 25-Jan-1982
https://dl.acm.org/doi/10.1145/582153.582186
Parikh R(1982)Some applications of topology to program semanticsLogics of Programs10.1007/BFb0025791(375-386)Online publication date: 1982
https://doi.org/10.1007/BFb0025791
Halpern JMeyer AWhite JLipton RGoldberg P(1981)Axiomatic definitions of programming languages, IIProceedings of the 8th ACM SIGPLAN-SIGACT symposium on Principles of programming languages10.1145/567532.567548(139-148)Online publication date: 26-Jan-1981
https://dl.acm.org/doi/10.1145/567532.567548
Salwicki A(1980)Axioms of algorithmic logic univocally determine semantics of programsMathematical Foundations of Computer Science 198010.1007/BFb0022532(552-561)Online publication date: 1980
https://doi.org/10.1007/BFb0022532

View Options

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

Media

Figures

Other

Tables

View Table of Contents