Article

Free access

On effective axiomatizations of Hoare logics

Authors:

Edmund M. Clarke, Jr.,

Steven M. German,

Joseph Y. HalpernAuthors Info & Claims

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

Pages 309 - 321

https://doi.org/10.1145/582153.582186

Published: 25 January 1982 Publication History

PDF eReader

Abstract

For a wide class of programming languages P and expressive interpretations I, we show that there exist sound and relatively complete Hoare-like logics for both partial correctness and termination assertions. In fact, under mild assumptions on P and I, we show that the assertions true for P in I are uniformly decidable in the theory of I (Th(I)) iff the halting problem for P is decidable for finite interpretations. Moreover termination assertions are uniformly r.e. in Th(I) even if the halting problem for P is not decidable for finite interpretations. Since total correctness assertions coincide with termination assertions for deterministic programming languages, this last result unexpectedly suggests that the class of languages with good axiom systems for total correctness may be wider than for partial correctness.

References

[1]

{C176/79} Clarke, E.M. Programming language constructs for which it is impossible to obtain good Hoare axiom systems. JACM 26:1, January, 1979 Ph.D. Thesis, Cornell, 1976.

Digital Library

Google Scholar

[2]

{Co78} Cook, S.A. Soundness and completeness of an axiom system for program verification. SIAM Journal on Computing 7:1, pp. 70--90, February, 1978.

Crossref

Google Scholar

[3]

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

Digital Library

Google Scholar

[4]

{Ha79} Harel, D. First-Order Dynamic Logic. Lecture Notes in Computer Science, 68. Springer-Verlag, N.Y., 1979.

Digital Library

Google Scholar

[5]

{La80} Langmaack, H.A. Proof of a theorem of Lipton on Hoare Logic and Applications. Institut fur Informatik und Praktische Mathematik bericht 8003, June, 1980.

Google Scholar

[6]

{LO80} Langmaack, H.A. and E.R. Olderog. Present day Hoare-like systems for programming languages with procedures: Power, limits, and most likely extensions. In: Proceed, 7th Conf. Automata, Languages, and Programming, Nordwijkerhout 1980, Eds: J. W. de Bakker, J. van Leeuwen, LNCS 25, pp. 363--373, June, 1980.

Digital Library

Google Scholar

[7]

{Li77} Lipton, R.J. A necessary and sufficient condition for the existence of Hoare logics. In: 18th IEEE Symp. on Found. Comp. Science, pp. 1--6, October, 1977.

Digital Library

Google Scholar

[8]

{Me78} Meyer, A.R. Notes on Lipton's generalization of the theorems of Cook and Clarke on expressiveness. Privately circulated notes.

Google Scholar

[9]

{MH80} Meyer, A.R. and J.Y. Halpern. Axiomatic definitions of programming languages: a theoretical assessment. In: Proceed. 7th ACM Symp. on Principles of Programming Languages. pp. 202--212, January, 1980 (to appear in JACM).

Digital Library

Google Scholar

[10]

{Mi81} Mitchell, J.C. Axiomatic Definability and Completeness for Recursive Programs, S.M. Thesis. M.I.T., 1981.

Google Scholar

[11]

{Pr76} Pratt, V.R. Semantical Considerations of Floyd-Hoare Logic. In: 17th IEEE Symp. on Found. Comp. Science, pp. 109--121, October, 1976.

Google Scholar

[12]

{Sh67} Shoenfield, J. R. Mathematical logic. Addison Wesley, 1967.

Google Scholar

Cited By

View all

Langmaack H(2019)On termination problems for finitely interpreted ALGOL-like programsActa Informatica10.1007/BF0062528218:1(79-108)Online publication date: 2-Jan-2019
https://dl.acm.org/doi/10.1007/BF00625282
(2018)A necessary and sufficient condition in order that a Herbrand interpretation be expressive relative to recursive programsInformation and Control10.1016/S0019-9958(83)80006-056:3(212-219)Online publication date: 12-Dec-2018
https://dl.acm.org/doi/10.1016/S0019-9958%2883%2980006-0
Goerdt A(2005)A Hoare Calculus for functions defined by recursion on higher typesLogics of Programs10.1007/3-540-15648-8_9(106-117)Online publication date: 31-May-2005
https://doi.org/10.1007/3-540-15648-8_9
Show More Cited By

On effective axiomatizations of Hoare logics
1. Theory of computation

Recommendations

Intuitionistic Trilattice Logics

We take up a suggestion by Odintsov (2009, Studia Logica, 91, 407–428) and define intuitionistic variants of certain logics arising from the trilattice SIXTEEN₃ introduced in Shramko and Wansing (2005, Journal of Philosophical Logic, 34, 121–153 and ...
Undecidability of the Problem of Recognizing Axiomatizations of Superintuitionistic Propositional Calculi

We give a new proof of the following result (originally due to Linial and Post): it is undecidable whether a given calculus, that is a finite set of propositional formulas together with the rules of modus ponens and substitution, axiomatizes the ...
Optimal Axiomatizations of Finitely Valued Logics

We investigate the problem of finding optimal axiomatizations for operators and distribution quantifiers in finitely valued first-order logics. We show that the problem can be viewed as the minimization of certain propositional formulas. We outline a ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

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

January 1982

378 pages

ISBN:0897910656

DOI:10.1145/582153

Conference Chair:
Richard DeMillo

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]

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 25 January 1982

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Qualifiers

Article

Acceptance Rates

POPL '82 Paper Acceptance Rate 38 of 121 submissions, 31%;

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

13
Total Citations
View Citations
298
Total Downloads

Downloads (Last 12 months)42
Downloads (Last 6 weeks)9

Reflects downloads up to 11 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

View all

Langmaack H(2019)On termination problems for finitely interpreted ALGOL-like programsActa Informatica10.1007/BF0062528218:1(79-108)Online publication date: 2-Jan-2019
https://dl.acm.org/doi/10.1007/BF00625282
(2018)A necessary and sufficient condition in order that a Herbrand interpretation be expressive relative to recursive programsInformation and Control10.1016/S0019-9958(83)80006-056:3(212-219)Online publication date: 12-Dec-2018
https://dl.acm.org/doi/10.1016/S0019-9958%2883%2980006-0
Goerdt A(2005)A Hoare Calculus for functions defined by recursion on higher typesLogics of Programs10.1007/3-540-15648-8_9(106-117)Online publication date: 31-May-2005
https://doi.org/10.1007/3-540-15648-8_9
Josko B(2005)On expressive interpretations of a Hoare-logic for Clarke's language L4STACS 8410.1007/3-540-12920-0_7(73-84)Online publication date: 29-May-2005
https://doi.org/10.1007/3-540-12920-0_7
Olderog E(2005)Hoare's logic for programs with procedures — What has been achieved?Logics of Programs10.1007/3-540-12896-4_375(383-395)Online publication date: 31-May-2005
https://doi.org/10.1007/3-540-12896-4_375
Damm WJosko B(2005)A sound and relatively complete axiomatization of clarke's language L4Logics of Programs10.1007/3-540-12896-4_362(161-175)Online publication date: 31-May-2005
https://doi.org/10.1007/3-540-12896-4_362
Crasemann CLangmaack H(2005)Characterization of acceptable by algol-like programming languagesLogics of Programs10.1007/3-540-12896-4_360(129-146)Online publication date: 31-May-2005
https://doi.org/10.1007/3-540-12896-4_360
Langmaack H(2005)Aspects of programs with finite modesFoundations of Computation Theory10.1007/3-540-12689-9_108(241-254)Online publication date: 31-May-2005
https://doi.org/10.1007/3-540-12689-9_108
Stolboushkin A(1990)On the expressive power of program schemes with setsProceedings of the 5th Jerusalem Conference on Information Technology, 1990. 'Next Decade in Information Technology'10.1109/JCIT.1990.128315(447-455)Online publication date: 1990
https://doi.org/10.1109/JCIT.1990.128315
Loeckx JSieber KLoeckx JSieber K(1987)The Axiomatic Method of HoareThe Foundations of Program Verification10.1007/978-3-322-96753-4_8(149-173)Online publication date: 1987
https://doi.org/10.1007/978-3-322-96753-4_8
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.

Cited By

Recommendations

Intuitionistic Trilattice Logics

Undecidability of the Problem of Recognizing Axiomatizations of Superintuitionistic Propositional Calculi

Optimal Axiomatizations of Finitely Valued Logics