article

Free access

Axiomatic Definitions of Programming Languages: A Theoretical Assessment

Authors:

Albert R. Meyer,

Joseph Y. HalpernAuthors Info & Claims

Journal of the ACM (JACM), Volume 29, Issue 2

Pages 555 - 576

https://doi.org/10.1145/322307.322324

Published: 01 April 1982 Publication History

PDF eReader

References

[1]

APT, K.R., BERGSTRA, J A, AND MEERTEN$, L.G.L.T RecursLve asseruons are not enoughmor are they Theor. Comput Scl. 8 (1979), 73-87

Google Scholar

[2]

BERGSI~A, J.A., TIURYN, J, AND TUCKER, J V Correctness theories and program eqmvalence Preprint, SUcht,ng Mathemattsch Centrum, Amsterdam, 1979

Google Scholar

[3]

BLtKLE, A Survey of Input-Output Semantics and Program Vertfication. Institute of Computer Soence, Pohsh Academy of Sciences, Warsaw, 1979.

Google Scholar

[4]

CLARKE, E M. JR,Programming language constructs for which it is tmpossible to obtain good Hoare axaom systems. J ACM 26, 1 (Jan. 1979), 129-147

Crossref

Google Scholar

[5]

CooK, S A Soundness and completeness of an axtom system for program verification. SIAM ~ Comput 7, 1 (Feb. 1978), 70-90.

Google Scholar

[6]

CRAIG, W., AND VAUGHT, R L. Fimte axiomauzabihty using addmonal predicates. J. Symb. Logic 23, 3 (1958), 289-308

Google Scholar

[7]

DIJKSTRA, E.W. Guarded commands, nondeterminacy and formal derivation of programs Commun.,4CM 18, 8 (Aug. 1975), 453-457.

Crossref

Google Scholar

[8]

DIJKSTRA, E W A Disctphne of Programming Prentice-Hall, Englewood Cliffs, N.J., 1976.

Crossref

Google Scholar

[9]

ENDERTON, H.B. A Mathematical lntroductwn to Logw. Academic Press, New York, 1972.

Google Scholar

[10]

FLOYD, R W. Assigning meamng to programs }n Mathematical Aspects of Computer Science Proc Symposium in dpphed Mathemaucs, J T Schwartz, Ed., Ameneart Mathematical Society, Provtdenee, R I., 1967, pp. 19-33

Google Scholar

[11]

FRIEDMAN, H. Algorithmic procedures, generahzed Tunng algorithms, and elementary recurslon theory. In Logic Colloqutum, 1969, R.O Gandy and C M.E Yates, Eds, North Holland, Amsterdam, 1971, pp. 316--389

Google Scholar

[12]

GALLIER, J.H Nondetermlmstlc flowchart programs w~th recurslve procedures: Semantics and correctness I. Theor Comput. Sct 13, 3 (1981), 193-224.

Google Scholar

[13]

GALLIER, J H Non deterministlc flowchart programs with recursive procedures: Semantics and correctness II. Theor. Comput. ScL 13, 4 (1981), 239-270

Google Scholar

[14]

GRIEF, I, AND MEYER, A R. Specifying the semanucs of while-programs. A tutorial and critique of a paper by Hoare and Lauer. ACM Trans. Prog. Long, Syst. 3, 4 (Oct. 1981), 484-507.

Crossref

Google Scholar

[15]

HALPERN, J Y., AND MEYER, A R. Axaomatzc definitions of programming languages II. Proc 8th Arm. Syrup on the Principles of Programming Languages, Williamsburg, Va, January 1981, pp 139- 148

Crossref

Google Scholar

[16]

HAP.EL, D.First.Order Dynamic Logic Lecture Notes in Computer Sc, ence, 68, Springer-Verlag, New York, 1979.

Crossref

Google Scholar

[17]

HAm, D, MEYEr, A.R, AND PRATT, V.R Computabdtty and completeness in log,cs of programs: Preliminary report. Proc 9th Ann. ACM Symp. on Theory of Computing, Boulder, Colo., May 1977, pp 261-268, Revised version- Tech. Pep., MIT LCS TM-97, M.I.T, Cambridge, Mass., Feb. 1978

Crossref

Google Scholar

[18]

HOaRE, C.A.R Some properties of predicate transformers. J ACM 25, 3 (July 1978), 461-480

Crossref

Google Scholar

[19]

HOARE, C.A R., AND LAUER, P.Consistem and complementary formal theories of the semantics of programming languages Acta I. 3 (1974), 135-155.

Google Scholar

[20]

HOARE, C A R., AND WIRTH, N. An axaomatlc defmmon of the programming language PASCAL Acta lnf 2 (1973), 335-355.

Google Scholar

[21]

JAIqSSEt~, T.M V., ANn VAN EroDE BOAS, P.The expressive power of mtensional logic in the semantics of programming languages. Preprmt, Stichting Mathematisch Centrum, Amsterdam, May 1977

Google Scholar

[22]

KLEEr;~ S.C.Two Papers on the Predicate Calculus. Memoirs of the Amencan Mathematical Society, 10, American Mathematical Society, Providence, R.I, 1952, pp 27-66

Google Scholar

[23]

LONDON, R L. Program verification In Research D~rections in Software Technology, Peter Wegner, Ed, M I T. Press, Cambridge, Mass., 1978, pp. 302-315.

Google Scholar

[24]

MAchtey, M., AND YOUNC, P An IntroducUon to the General Theory of Algorithms. North Holland, Amsterdam, 1978.

Crossref

Google Scholar

[25]

MEYER, A.R, AND HALPERN, I.Y. Axiomatic defimtlons of programming languages" A theoreucal assessment Proc 7th Ann Symp. on Principles of Programming Languages, Las Vegas, Nev, Jan. 1980, pp. 203-212.

Crossref

Google Scholar

[26]

MEYER, A R, AND WINKLMANN, K. On the expressive power of dynamic loglc Proc 1 l th Arm Conf on Theory of Computing, Atlanta, Ga., May 1979, pp 167-175.

Crossref

Google Scholar

[27]

O'DONNELL, M J Computing :n Systems Descrtbed by Equations, Lecture Notes m Computer Science 58, Springer-Verlag, 1977

Crossref

Google Scholar

[28]

Pv, Arr, V R.Semantical considerations of Floyd-Hoare logic. 17th Ann. IEEE Syrup on the Foundations of Computer Science, Houston, Tex, Oct 1976, pp 109-121

Google Scholar

[29]

SCHWARTZ) R.L. An axiomatic semantic defimtton of Algol 68. Tech. Rep. UCLA-ENG-7838, UCLA-34P214-75, Univ. of California at Los Angeles, Los Angeles, Cahf. 1978.

Google Scholar

[30]

SCHWARTZ, R.L. An axiomatic treatment of ALGOL 68 routines. In Automata, Languages and Programming, Sixth Colloqutum, Lecture Notes ha Computer Science 71, H.A Maurer, Ed., Springer- Verlag, N.Y., 1979, pp. 530--545.

Crossref

Google Scholar

Cited By

View all

KHALED MSZÉKELY GLEFEVER KFRIEND M(2019)DISTANCES BETWEEN FORMAL THEORIESThe Review of Symbolic Logic10.1017/S175502031900055813:3(633-654)Online publication date: 4-Oct-2019
https://doi.org/10.1017/S1755020319000558
Platzer A(2015)Differential Game LogicACM Transactions on Computational Logic10.1145/281782417:1(1-51)Online publication date: 14-Nov-2015
https://dl.acm.org/doi/10.1145/2817824
Apt KBouveresse JFeferman SGaifman HGirard JHodges WKrivine JLascar DMcAloon KNivat MSabbagh G(2014)European Summer Meeting of the Association for Symbolic Logic, Paris, 1985The Journal of Symbolic Logic10.2307/227389352:01(295-349)Online publication date: 12-Mar-2014
https://doi.org/10.2307/2273893
Show More Cited By

Index Terms

Axiomatic Definitions of Programming Languages: A Theoretical Assessment
1. Software and its engineering
  1. Software notations and tools
    1. Formal language definitions
      1. Semantics
2. Theory of computation
  1. Logic
  2. Semantics and reasoning
    1. Program reasoning
    2. Program semantics

Recommendations

Axiomatic definitions of programming languages: a theoretical assessment (preliminary report)
POPL '80: Proceedings of the 7th ACM SIGPLAN-SIGACT symposium on Principles of programming languages

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 ...
Derivation of axiomatic definitions of programming languages from algorithmic definitions
Proceedings of ACM conference on Proving assertions about programs

Language definitions by abstract interpreters are appropriate to the design and development of a language. Axiomatic definitions are more appropriate to proving program properties and verification of compilers. The proof methods of Manna and Ashcroft ...
Derivation of axiomatic definitions of programming languages from algorithmic definitions
Proceedings of ACM conference on Proving assertions about programs

Language definitions by abstract interpreters are appropriate to the design and development of a language. Axiomatic definitions are more appropriate to proving program properties and verification of compilers. The proof methods of Manna and Ashcroft ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

Journal of the ACM Volume 29, Issue 2

April 1982

330 pages

ISSN:0004-5411

EISSN:1557-735X

DOI:10.1145/322307

Issue’s Table of Contents

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 01 April 1982

Published in JACM Volume 29, Issue 2

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

24
Total Citations
View Citations
643
Total Downloads

Downloads (Last 12 months)47
Downloads (Last 6 weeks)5

Reflects downloads up to 16 Jan 2025

Other Metrics

View Author Metrics

Citations

Cited By

View all

KHALED MSZÉKELY GLEFEVER KFRIEND M(2019)DISTANCES BETWEEN FORMAL THEORIESThe Review of Symbolic Logic10.1017/S175502031900055813:3(633-654)Online publication date: 4-Oct-2019
https://doi.org/10.1017/S1755020319000558
Platzer A(2015)Differential Game LogicACM Transactions on Computational Logic10.1145/281782417:1(1-51)Online publication date: 14-Nov-2015
https://dl.acm.org/doi/10.1145/2817824
Apt KBouveresse JFeferman SGaifman HGirard JHodges WKrivine JLascar DMcAloon KNivat MSabbagh G(2014)European Summer Meeting of the Association for Symbolic Logic, Paris, 1985The Journal of Symbolic Logic10.2307/227389352:01(295-349)Online publication date: 12-Mar-2014
https://doi.org/10.2307/2273893
Leivant D(2009)Inductive Completeness of Logics of ProgramsElectronic Notes in Theoretical Computer Science (ENTCS)10.1016/j.entcs.2008.12.119228(101-112)Online publication date: 1-Jan-2009
https://dl.acm.org/doi/10.1016/j.entcs.2008.12.119
Leivant D(2008)Reasoning in dynamic logic about program terminationPillars of computer science10.5555/1805839.1805862(441-456)Online publication date: 1-Jan-2008
https://dl.acm.org/doi/10.5555/1805839.1805862
Leivant D(2008)Reasoning in Dynamic Logic about Program TerminationPillars of Computer Science10.1007/978-3-540-78127-1_23(441-456)Online publication date: 2008
https://doi.org/10.1007/978-3-540-78127-1_23
Honsell FMiculan M(2005)A natural deduction approach to dynamic logicTypes for Proofs and Programs10.1007/3-540-61780-9_69(165-182)Online publication date: 7-Jun-2005
https://doi.org/10.1007/3-540-61780-9_69
Weispfenning V(2005)Diamond formulas in the dynamic logic of recursively enumerable programs8th International Conference on Automated Deduction10.1007/3-540-16780-3_120(564-571)Online publication date: 31-May-2005
https://doi.org/10.1007/3-540-16780-3_120
Leviant D(2005)Partial-correctness theories as first-order theoriesLogics of Programs10.1007/3-540-15648-8_15(190-195)Online publication date: 31-May-2005
https://doi.org/10.1007/3-540-15648-8_15
Leivant D(2004)Proving termination assertions in dynamic logicsProceedings of the 19th Annual IEEE Symposium on Logic in Computer Science, 2004.10.1109/LICS.2004.1319603(89-98)Online publication date: 2004
https://doi.org/10.1109/LICS.2004.1319603
Show More Cited By

View Options

View options

PDF

View or Download as a PDF file.

PDF

eReader

View online with eReader.

eReader

Login options

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

References

Cited By

Index Terms

Recommendations