A Complete and Consistent Hoare Axiomatics for a Simple Programming Language

Subscribe (Full Service)


	Search: The ACM Digital Library The Guide

	Feedback

A Complete and Consistent Hoare Axiomatics for a Simple Programming Language

Full text

Pdf (612 KB)

Source

Journal of the ACM (JACM) archive
Volume 26 , Issue 1 (January 1979) table of contents

Pages: 119 - 128

Year of Publication: 1979

ISSN:0004-5411

Authors

John C. Cherniavsky	Department of Computer Science, State University of New York at Stony Brook, Stony Brook, NY
Samuel N. Kamin	Department of Computer Science, State University of New York at Stony Brook, Stony Brook, NY

Publisher

ACM New York, NY, USA

Bibliometrics

Downloads (6 Weeks): 1, Downloads (12 Months): 21, Citation Count: 2

Additional Information:

references cited by index terms collaborative colleagues

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/322108.322120 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	CrlERNIAVSKY, J.C Simple programs realize exactly Presberger formulas SlAM J. Comping, 5, 4 (1976), 666-677
	2	Edmund Melson Clarke, Jr., Programming language constructs for which it is impossible to obtain good hoare-like axiom systems, Proceedings of the 4th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.10-20, January 17-19, 1977, Los Angeles, California [doi>10.1145/512950.512952]
	3	Robert L. Constable , Allan B. Borodin, Subrecursive Programming Languages, Part I: efficiency and program structure, Journal of the ACM (JACM), v.19 n.3, p.526-568, July 1972 [doi>10.1145/321707.321721]
	4	COOK, S.A Soundness and completeness of an axiom system for program venficauon TR 95, Dept of Comptr So, U of Toronto, Toronto, Canada, June 1976
	5	COOPER, D C Theorem-provmg m arithmetic without muluphcatton Machine Intelhgence 7, B Meltzer and D Mlchle, Eds, Wiley, New York, 1972, pp 91-99
	6	ENDERTON, H.B A Mathematical Introduction to Logw Academic Press, New York, 1972
	7	HOARE, C A R, AND WIRTH, N An axtomauc defimuon of the programming language PASCAL Acta Informauca 2 (1973), 335-355
	8	Neil D. Jones , Steven S. Muchnick, Even Simple Programs Are Hard To Analyze, Journal of the ACM (JACM), v.24 n.2, p.338-350, April 1977 [doi>10.1145/322003.322016]
	9	Zohar Manna, Introduction to Mathematical Theory of Computation, McGraw-Hill, Inc., New York, NY, 1974
	10	Elliott Mendelson, Introduction to mathematical logic (3rd ed.), Wadsworth Publ. Co., Belmont, CA, 1987
	11	Albert R. Meyer , Dennis M. Ritchie, The complexity of loop programs, Proceedings of the 1967 22nd national conference, p.465-469, January 1967, Washington, D.C., United States [doi>10.1145/800196.806014]
	12	PATERSON, M S Eqmvalence problems m a model ofcomputauon Ph D Dtss, U of Cambridge, Cambridge, England, 1967

CITED BY 2

	Eitan M. Gurari , Oscar H. Ibarra, The Complexity of the Equivalence Problem for Simple Programs, Journal of the ACM (JACM), v.28 n.3, p.535-560, July 1981
	Eitan M. Gurari, Decidable problems for powerful programs, Journal of the ACM (JACM), v.32 n.2, p.466-483, April 1985