article

Open access

Specifying the Semantics of while Programs: A Tutorial and Critique of a Paper by Hoare and Lauer

Editor: Susan L. Graham Authors:

Irene Greif,

Albert R. MeyerAuthors Info & Claims

ACM Transactions on Programming Languages and Systems (TOPLAS), Volume 3, Issue 4

Pages 484 - 507

https://doi.org/10.1145/357146.357151

Published: 01 October 1981 Publication History

PDF eReader

References

[1]

oEBAKKER, J.W. Mathematical Theory of Program Correctness. Prentice-Hall, Englewood Cliffs, N.J., 1980.

Crossref

Google Scholar

[2]

oEBAKKER, J.W. Recursive programs as predicate transformers. In Proc. IFIP Conf. Formal Specifications of Programming Constructs, St. Andrews, New Brunswick, 1977, pp. 7.1-7.15.

Google Scholar

[3]

DEBAKKER, J.W. Flow of control in the proof theory of structured programming. In 16th Ann. Syrup. Foundations of Computer Science. IEEE Computer Society, Long Beach, Calif., 1975, pp. 29-33.

Google Scholar

[4]

DEBAKKER, J.W., ANO MEERTENS, L.G.L.T. On the completeness of the inductive assertion method. J. Comput. Syst. Sci. 11, 3 (Dec. 1975), 323-357.

Google Scholar

[5]

DEROEVER, W.P. Dijkstra's predicate transformer, nondeterminism, recursion and termination. In Lecture Notes in Computer Science, vol. 45: Foundations of Computer Science, Springer- Verlag, New York, 1976, pp. 472-481.

Google Scholar

[6]

DIJgSTRA, E.W. A Discipline of Programming. Prentice-Hall, Englewood Cliffs, N.J., 1976.

Crossref

Google Scholar

[7]

D~JKSTRA, E.W. Guarded commands, nondeterminacy and formal derivation of programs. Commun. ACM 18, 8 (Aug. 1975), 453-457.

Crossref

Google Scholar

[8]

FLOYO, R.W. Assigning meaning to programs. In Proc. Symp. Applied Mathematics, vol. 19:{ Mathematical Aspects of Computer Science, J.T. Schwartz (Ed.). American Mathematical Society, Providence, R.I., 1967, pp. 19-32.

Google Scholar

[9]

GREIF, I., ANO MEYER, A. Specifying programming language semantics: A tutorial and critique of a paper by Hoare and Lauer. In Conf. Rec., 6th Ann. ACM Syrup. Principles of Programming Languages, San Antonio, Tex., Jan. 29-31, 1979, pp. 180-189.

Crossref

Google Scholar

[10]

HAREL, D. First-Order Dynamic Logic. Lecture Notes in Computer Science, G. Goos and J. Hartmanis (Eds.). Springer-Verlag, New York, 1978.

Crossref

Google Scholar

[11]

HAREL, D., MEYER, A.R., AND PRATT, V.R. Computability and completeness in logics of programs. In Conf. Ree., 9th Ann. ACM Symp. Theory of Computing, Boulder, Colo., May 2-4, 1977, pp. 261-268.

Crossref

Google Scholar

[12]

HAREL, D., AND PRATT, V.R. Nondeterminism in logics of programs (preliminary report). In Conf. Rec., 5th Ann. ACM Symp. Principles of Programming Languages, Tucson, Ariz., Jan. 23- 25, 1978, pp. 203-213.

Crossref

Google Scholar

[13]

HOARE, C.A.R. Some properties of predicate transformers. J. ACM25, 3 (July 1978), 461-480.

Crossref

Google Scholar

[14]

HOARE, C.A.R. An axiomatic basis for computer programming. Commun. ACM 12, 10 (Oct. 1969), 576-580, 583.

Crossref

Google Scholar

[15]

HOARE, C.A.R., AND LAUER, P. Consistent and complementary formal theories of the semantics of programming languages. Acta Inf. 3, 2 (May 1974), 135-153.

Google Scholar

[16]

HOARE, C.A.R., ANO WIRTH, N. An axiomatic definition of the programming language PASCAL. Acta Inf. 2, 4 (1973), 335-355.

Google Scholar

[17]

LAUER, P. Consistent Formal Theories of the Semantics of Programming Languages. Ph.D. dissertation, Faculty of Science, Queen's Univ. Belfast, 1971 (also Tech. Rep. 25.121, IBM Lab. Vienna, Vienna, Austria, 1971).

Google Scholar

[18]

MANNA, Z. Mathematical Theory of Computation. McGraw-Hill, New York, 1974.

Crossref

Google Scholar

[19]

MEYER, A.R., AND HALPERN, J.Y. Axiomatic definitions of programming languages: A theoretical assessment (preliminary report). In Conf. Rec., 7th Ann. ACM Symp. Principles of Programming Languages, Las Vegas, Nev., Jan. 28-30, 1980, pp. 203-212.

Crossref

Google Scholar

[20]

PRATT, V.R. Semantical considerations on Floyd-Hoare logic. In 17th Ann. Syrup. Foundations of Computer Science. IEEE Computer Society, Long Beach, Calif., 1976, pp. 109-121.

Google Scholar

[21]

RAULEFS, P. The connection between axiomatic and denotational semantics of programming languages. Interner Ber. 4/77, Inst. ffir Inforrnatik I. Univ. Karisruhe, Karlsruhe, W. Germany, 1977.

Google Scholar

[22]

SCHWARZ, g.s. Semantics of Partial Correctness Formalisms. Ph.D. dissertation, Dep. Systems and Information Sciences, Syracuse Univ., Syracuse, N.Y., 1974.

Crossref

Google Scholar

Cited By

View all

Apt KOlderog E(2021)Assessing the Success and Impact of Hoare’s LogicTheories of Programming10.1145/3477355.3477359(41-76)Online publication date: 4-Oct-2021
https://dl.acm.org/doi/10.1145/3477355.3477359
BERGER MHONDA KYOSHIDA N(2007)A logical analysis of aliasing in imperative higher-order functionsJournal of Functional Programming10.1017/S095679680700641717:4-5(473-546)Online publication date: 1-Jul-2007
https://dl.acm.org/doi/10.1017/S0956796807006417
Berger MHonda KYoshida N(2005)A logical analysis of aliasing in imperative higher-order functionsACM SIGPLAN Notices10.1145/1090189.108640140:9(280-293)Online publication date: 12-Sep-2005
https://dl.acm.org/doi/10.1145/1090189.1086401
Show More Cited By

Index Terms

Specifying the Semantics of while Programs: A Tutorial and Critique of a Paper by Hoare and Lauer

Recommendations

The axiomatic semantics of programs based on Hoare's logic

This paper is about the Floyd-Hoare Principle which says that the semantics of a programming language can be formally specified by axioms and rules of inference for proving the correctness of programs written in the language. We study the simple ...
Semantics for disjunctive logic programs
Stable semantics for disjunctive programs
Abstract
We introduce the stable model semantics fordisjunctive logic programs and deductive databases, which generalizes the stable model semantics, defined earlier for normal (i.e., non-disjunctive) programs. Depending on whether only total (2-valued) or ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Transactions on Programming Languages and Systems

ACM Transactions on Programming Languages and Systems Volume 3, Issue 4

Oct. 1981

184 pages

ISSN:0164-0925

EISSN:1558-4593

DOI:10.1145/357146

Editor:
Susan L. Graham

Issue’s Table of Contents

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 01 October 1981

Published in TOPLAS Volume 3, Issue 4

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

12
Total Citations
View Citations
689
Total Downloads

Downloads (Last 12 months)91
Downloads (Last 6 weeks)20

Reflects downloads up to 16 Jan 2025

Other Metrics

View Author Metrics

Citations

Cited By

View all

Apt KOlderog E(2021)Assessing the Success and Impact of Hoare’s LogicTheories of Programming10.1145/3477355.3477359(41-76)Online publication date: 4-Oct-2021
https://dl.acm.org/doi/10.1145/3477355.3477359
BERGER MHONDA KYOSHIDA N(2007)A logical analysis of aliasing in imperative higher-order functionsJournal of Functional Programming10.1017/S095679680700641717:4-5(473-546)Online publication date: 1-Jul-2007
https://dl.acm.org/doi/10.1017/S0956796807006417
Berger MHonda KYoshida N(2005)A logical analysis of aliasing in imperative higher-order functionsACM SIGPLAN Notices10.1145/1090189.108640140:9(280-293)Online publication date: 12-Sep-2005
https://dl.acm.org/doi/10.1145/1090189.1086401
Berger MHonda KYoshida NDanvy OPierce B(2005)A logical analysis of aliasing in imperative higher-order functionsProceedings of the tenth ACM SIGPLAN international conference on Functional programming10.1145/1086365.1086401(280-293)Online publication date: 28-Sep-2005
https://dl.acm.org/doi/10.1145/1086365.1086401
Dam MJensen F(2005)Compiler generation from relational semanticsESOP 8610.1007/3-540-16442-1_1(1-29)Online publication date: 29-May-2005
https://doi.org/10.1007/3-540-16442-1_1
COUSOT P(1990)Methods and Logics for Proving ProgramsFormal Models and Semantics10.1016/B978-0-444-88074-1.50020-2(841-993)Online publication date: 1990
https://doi.org/10.1016/B978-0-444-88074-1.50020-2
Zedan H(1990)Key references in distributed computer systems 1959–1989Distributed Computer Systems10.1016/B978-0-408-02938-4.50016-4(193-295)Online publication date: 1990
https://doi.org/10.1016/B978-0-408-02938-4.50016-4
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
Parikh R(1983)Some applications of topology to program semanticsMathematical Systems Theory10.1007/BF0174457316:1(111-131)Online publication date: Dec-1983
https://doi.org/10.1007/BF01744573
Meyer AHalpern J(1982)Axiomatic Definitions of Programming LanguagesJournal of the ACM10.1145/322307.32232429:2(555-576)Online publication date: 1-Apr-1982
https://dl.acm.org/doi/10.1145/322307.322324
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

The axiomatic semantics of programs based on Hoare's logic

Semantics for disjunctive logic programs

Stable semantics for disjunctive programs

Comments

Information

Published In

Publisher

Publication History

Permissions

Check for updates

Qualifiers

Contributors

Other Metrics

Bibliometrics

Article Metrics

Other Metrics

Citations

Cited By

View options

PDF

eReader

Login options

Full Access

Figures

Other

Share

Share this Publication link

Share on social media

Affiliations