Axiomatic Definitions of Programming Languages

Subscribe (Full Service)


	Search: The ACM Digital Library The Guide

	Feedback

Axiomatic Definitions of Programming Languages: A Theoretical Assessment

Full text

Pdf (1.18 MB)

Source

Journal of the ACM (JACM) archive
Volume 29 , Issue 2 (April 1982) table of contents

Pages: 555 - 576

Year of Publication: 1982

ISSN:0004-5411

Authors

Albert R. Meyer	Laboratory for Computer Science, 545 Technology Square, Massachusetts, Institute of Technology, Cambridge, MA
Joseph Y. Halpern	Laboratory for Computer Science, 545 Technology Square, Massachusetts, Institute of Technology, Cambridge, MA and Harvard University, Cambridge, Massachusetts

Publisher

ACM New York, NY, USA

Bibliometrics

Downloads (6 Weeks): 1, Downloads (12 Months): 22, Citation Count: 5

Additional Information:

references cited by index terms collaborative colleagues peer to peer

Tools and Actions:	Request Permissions Review this Article Save this Article to a Binder Display Formats: BibTeX EndNote ACM Ref

DOI Bookmark:	Use this link to bookmark this Article: http://doi.acm.org/10.1145/322307.322324 What is a DOI?

REFERENCES

Note: OCR errors may be found in this Reference List extracted from the full text article. ACM has opted to expose the complete List rather than only correct and linked 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
	2	BERGSI~A, J.A., TIURYN, J, AND TUCKER, J V Correctness theories and program eqmvalence Preprint, SUcht,ng Mathemattsch Centrum, Amsterdam, 1979
	3	BLtKLE, A Survey of Input-Output Semantics and Program Vertfication. Institute of Computer Soence, Pohsh Academy of Sciences, Warsaw, 1979.
	4	Edmund Melson Clarke, Jr., Programming Language Constructs for Which It Is Impossible To Obtain Good Hoare Axiom Systems, Journal of the ACM (JACM), v.26 n.1, p.129-147, Jan. 1979 [doi>10.1145/322108.322121]
	5	CooK, S A Soundness and completeness of an axtom system for program verification. SIAM ~ Comput 7, 1 (Feb. 1978), 70-90.
	6	CRAIG, W., AND VAUGHT, R L. Fimte axiomauzabihty using addmonal predicates. J. Symb. Logic 23, 3 (1958), 289-308
	7	Edsger W. Dijkstra, Guarded commands, nondeterminacy and formal derivation of programs, Communications of the ACM, v.18 n.8, p.453-457, Aug. 1975 [doi>10.1145/360933.360975]
	8	Edsger Wybe Dijkstra, A Discipline of Programming, Prentice Hall PTR, Upper Saddle River, NJ, 1997
	9	ENDERTON, H.B. A Mathematical lntroductwn to Logw. Academic Press, New York, 1972.
	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
	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
	12	GALLIER, J.H Nondetermlmstlc flowchart programs w~th recurslve procedures: Semantics and correctness I. Theor Comput. Sct 13, 3 (1981), 193-224.
	13	GALLIER, J H Non deterministlc flowchart programs with recursive procedures: Semantics and correctness II. Theor. Comput. ScL 13, 4 (1981), 239-270
	14	Irene Greif , Albert R. Meyer, Specifying the Semantics of while Programs: A Tutorial and Critique of a Paper by Hoare and Lauer, ACM Transactions on Programming Languages and Systems (TOPLAS), v.3 n.4, p.484-507, Oct. 1981 [doi>10.1145/357146.357151]
	15	Joseph Y. Halpern , Albert R. Meyer, Axiomatic definitions of programming languages, II, Proceedings of the 8th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.139-148, January 26-28, 1981, Williamsburg, Virginia [doi>10.1145/567532.567548]
	16	David Harel, First-Order Dynamic Logic, Springer-Verlag New York, Inc., Secaucus, NJ, 1979
	17	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]
	18	C. A. R. Hoare, Some Properties of Predicate Transformers, Journal of the ACM (JACM), v.25 n.3, p.461-480, July 1978 [doi>10.1145/322077.322088]
	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.
	20	HOARE, C A R., AND WIRTH, N. An axaomatlc defmmon of the programming language PASCAL Acta lnf 2 (1973), 335-355.
	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
	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
	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.
	24	Michael Machtey , Paul Young, An Introduction to the General Theory of Algorithms, Elsevier Science Inc., New York, NY, 1978
	25	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]
	26	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]
	27	Michael J. O'Donnell, Computing in Systems Described by Equations, Springer-Verlag New York, Inc., Secaucus, NJ, 1977
	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
	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.
	30	Richard L. Schwartz, An Aximatic Treatment of Algol 68 Routines, Proceedings of the 6th Colloquium, on Automata, Languages and Programming, p.530-545, July 16-20, 1979

CITED BY 5

	CORPORATE Tech Correspondence, Technical correspondence, Communications of the ACM, v.28 n.5, p.534-538, May 1985
	Edmund M. Clarke, Jr. , Steven M. German , Joseph Y. Halpern, Effective Axiomatizations of Hoare Logics, Journal of the ACM (JACM), v.30 n.3, p.612-636, July 1983
	Daniel Leivant, Inductive Completeness of Logics of Programs, Electronic Notes in Theoretical Computer Science (ENTCS), 228, p.101-112, January, 2009
	Daniel Leivant, Logical and mathematical reasoning about imperative programs: preliminary report, Proceedings of the 12th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.132-140, January 14-16, 1985, New Orleans, Louisiana, United States
	David Peleg, Concurrent dynamic logic, Journal of the ACM (JACM), v.34 n.2, p.450-479, April 1987