A New Incompleteness Result for Hoare's System

Subscribe (Full Service)


	Search: The ACM Digital Library The Guide

	Feedback

A New Incompleteness Result for Hoare's System

Full text

Pdf (432 KB)

Source

Journal of the ACM (JACM) archive
Volume 25 , Issue 1 (January 1978) table of contents

Pages: 168 - 175

Year of Publication: 1978

ISSN:0004-5411

Author

Mitchell Wand

Computer Science Department, Indiana University, 101 Lindley Hall, Bloomington, IN

Publisher

ACM New York, NY, USA

Bibliometrics

Downloads (6 Weeks): 1, Downloads (12 Months): 24, Citation Count: 7

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/322047.322062 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	BETH, E W Formal Methods D Reldel, Dordrecht-Holland, 1962.
	2	Robert S. Boyer , J. Strother Moore, Proving Theorems about LISP Functions, Journal of the ACM (JACM), v.22 n.1, p.129-144, Jan. 1975 [doi>10.1145/321864.321875]
	3	COOK, S A Axiomattc and interpretive semantics for an ALGOL fragment Tech Rep 79, Dept. Comptr. Sci, U of Toronto, Toronto, Ont, Feb 1975
	4	DEBAKKER, J W , AND MEERTENS, L G L T On the completeness of the inductive assertion method J Comptr Syst Scl 11 (1975), 323-357
	5	Maarten M. Fokkinga, Inductive assertion patters for recursive procedures, Programming Symposium, Proceedings Colloque sur la Programmation, p.221-233, April 09-11, 1974
	6	HF.WITT, C W , AND SMITH, B Towards a programming apprentice IEEE Trans on Software Eng SE- 1 (1975), 25-45.
	7	C. A. R. Hoare, An axiomatic basis for computer programming, Communications of the ACM, v.12 n.10, p.576-580, Oct. 1969 [doi>10.1145/363235.363259]
	8	C. A. R. Hoare, Proof of a program: FIND, Communications of the ACM, v.14 n.1, p.39-45, Jan. 1971 [doi>10.1145/362452.362489]
	9	HOARE, C A R, AND LAUER, P Consistent and complementary formal theories of the semanucs of programming languages Acta Informattca 3 (1974), 135-153
	10	Ralph L. London, A view of program verification, Proceedings of the international conference on Reliable software, p.534-545, April 21-23, 1975, Los Angeles, California
	11	LYONS, T, AND BaUNO, J An interactive system for program verification Courant Computer Sctence Symposmm 4 Algorahm Spect/icatlon, R Rustm, Ed , 1971, pp 117-141
	12	Zohar Manna, Introduction to Mathematical Theory of Computation, McGraw-Hill, Inc., New York, NY, 1974
	13	PRATT, V Semantical considerations on Floyd-Hoare log,c Proc IEEE Syrup on Foundations of Comptr Scl., 1976, pp. 109-121.
	14	SHOENFIELD, J R. Mathemattcal Logtc Addison-Wesley, Reading, Mass., 1967
	15	Norihisa Suzuki, Verifying programs by algebraic and logical reduction, Proceedings of the international conference on Reliable software, p.473-481, April 21-23, 1975, Los Angeles, California

CITED BY 7

	Krzysztof R. Apt, Ten Years of Hoare's Logic: A Survey—Part I, ACM Transactions on Programming Languages and Systems (TOPLAS), v.3 n.4, p.431-483, Oct. 1981
	L. Colussi, Recursion As an Effective Step in Program Development, ACM Transactions on Programming Languages and Systems (TOPLAS), v.6 n.1, p.55-67, Jan. 1984
	D. Leivant , T. Fernando, Skinny and fleshy failures of relative completeness, Proceedings of the 14th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.246-252, January 21-23, 1987, Munich, West Germany
	Daniel Leivant , Tim Fernando, Meager and replete failures of relative completeness, Journal of the ACM (JACM), v.35 n.4, p.953-964, Oct. 1988
	Stephen L. Bloom , Zoltán Ésik, Floyd-Hoare logic in iteration theories, Journal of the ACM (JACM), v.38 n.4, p.887-934, Oct. 1991
	S. Antoy , J. Gannon, Using Term Rewriting to Verify Software, IEEE Transactions on Software Engineering, v.20 n.4, p.259-274, April 1994
	Sandip Ray , Warren A. Hunt, Jr. , John Matthews , J. Strother Moore, A Mechanical Analysis of Program Verification Strategies, Journal of Automated Reasoning, v.40 n.4, p.245-269, May 2008