Ten Years of Hoare's Logic: A Survey

Subscribe (Full Service)


	Search: The ACM Digital Library The Guide

	Feedback

Ten Years of Hoare's Logic: A Survey—Part I

Full text

Pdf (2.98 MB)

Source

ACM Transactions on Programming Languages and Systems (TOPLAS) archive
Volume 3 , Issue 4 (October 1981) table of contents

Pages: 431 - 483

Year of Publication: 1981

ISSN:0164-0925

Author

Krzysztof R. Apt

LITP, Université Paris 7, 2, place Jussieu, 75221 Paris, France

Publisher

ACM New York, NY, USA

Bibliometrics

Downloads (6 Weeks): 34, Downloads (12 Months): 291, Citation Count: 43

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/357146.357150 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. A sound complete Hoare-like system for a fragment of PASCAL. Rep. IW 97/78, Mathematisch Centrum, Amsterdam, 1978.
	2	APT, K.R., BERGSTRA, J.A., AND MEr. RTENS, L.G.L.T. Recursive assertions are not enough--Or are they? Theor. Comput. Sci. 8 (1979), 73-87.
	3	Krzysztof R. Apt , J. W. de Bakker, Semantics and Proof Theory of Pascal Procedures, Proceedings of the Fourth Colloquium on Automata, Languages and Programming, p.30-44, July 18-22, 1977
	4	ArT, K.R., AND DE BAKKER, J.W. Exercises in denotational semantics. In Lecture Notes in Computer Science, vol. 45: Proc. 5th Syrup. Mathematical Foundations of Computer Science. Springer-Verlag, New York, 1976, pp. 1-11.
	5	BERGSTRA, J.A., AND TUCKER, J.V. Some natural structures which fail to possess a sound and decidable Hoare-like logic for their while-programs. Theor. Comput. Sci., to appear; earlier version appeared as Rep. IW 136/80, Mathematisch Centrum, Amsterdam, 1980.
	6	BERCSTRA, J.A., AND TUCKER, J.V. Expressiveness and the completeness of Hoare's logic. Rep. IW 149/80, Mathematisch Centrum, Amsterdam, 1980.
	7	Robert Cartwright , Derek Oppen, Unrestricted procedure calls in Hoare's logic, Proceedings of the 5th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.131-140, January 23-25, 1978, Tucson, Arizona [doi>10.1145/512760.512774]
	8	CLARKE, E.M., JR. Proving correctness of coroutines without history variables. Acta Inf. 13 (1980), pp. 169-188.
	9	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]
	10	CLARKE, E.M., JR. Program invariants as fixed points. In Proc. 18th IEEE Symp. Foundations of Computer Science, 1977, pp. 18-29.
	10a	Edmund Melson Clarke, Jr., Completeness and incompleteness theorems for hoare-like axiom systems., 1976
	11	CLINT, M. Program proving: Coroutines. Acta Inf. 2 (1973), 50-63.
	12	GLINT, M., AND HOARE, C.A.R. Program proving: Jumps and functions. Acta Inf. 1 (1971), 214-224.
	13	COOK, S.A. Soundness and completeness of an axiom system for program verification. SIAM J. Comput. 7, i (1978), 70-90.
	14	J. W. de Bakker, Mathematical Theory of Program Correctness, Prentice-Hall, Inc., Upper Saddle River, NJ, 1980
	15	Dr~ BAKKER, J.W. Correctness proofs for assignment statements. Rep. IW 55/76, Mathematisch Centrum, Amsterdam, 1976.
	16	Edsger Wybe Dijkstra, A Discipline of Programming, Prentice Hall PTR, Upper Saddle River, NJ, 1997
	17	James Edward Donahue, Complementary Definitions of Programming Language Semantics, Springer-Verlag New York, Inc., Secaucus, NJ, 1976
	18	FLOYO, R.W. Assigning meanings to programs. In Proc. AMS Syrup. Applied Mathematics, vol. 19. American Mathematical Society, Providence, R.I., 1967, pp. 19-31.
	19	GORELICK, G.A. A complete axiomatic system for proving assertions about recursive and nonrecursive programs. Tech. Rep. 75, Dep. Computer Science, Univ. Toronto, 1975.
	20	GRIr~S, D. The multiple assignment statement. IEEE Trans. Softw. Eng. SE-4 (March 1978), 89-93.
	21	David Gries , Gary Levin, Assignment and Procedure Call Proof Rules, ACM Transactions on Programming Languages and Systems (TOPLAS), v.2 n.4, p.564-579, Oct. 1980 [doi>10.1145/357114.357119]
	22	HARr~L, D. Proving the correctness of regular deterministic programs: A unifying survey using dynamic logic. Theor. Comput. Sci. 12 (1980), 61-81.
	23	David Harel, First-Order Dynamic Logic, Springer-Verlag New York, Inc., Secaucus, NJ, 1979
	24	HAREL, D., PNUELI, A., AND STAVI, J. Completeness issues for inductive assertions and Hoare's method. Tech. Rep., Dep. Computer Science, Univ. Tel Aviv, Israel, 1976.
	25	HOARE, C.A.R. Proof of correctness of data representations. Acta Inf. I (1972), 271-281.
	26	HOARE, C.A.R. Procedures and parameters: An axiomatic approach. In Lecture Notes in Mathematics, vol. 188: Semantics of Algorithmic Languages. Springer-Verlag, New York, 1971, pp. 102-116.
	27	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]
	28	HOARE, C.A.R., AND WIRTH, N. An axiomatic definition of the programming language PASCAL. Acta Inf. 2 (1973), 335-355.
	29	ICARASHI, S., LONDON, R.L., AND LUCKHAM, D.C. Automatic program verification i: A logical basis and its implementation. Acta Inf. 4 (1975), 145-182.
	30	T. M. V. Janssen , Peter van Emde Boas, On the Proper Treatment or Referencing, Dereferencing and Assignment, Proceedings of the Fourth Colloquium on Automata, Languages and Programming, p.282-300, July 18-22, 1977
	31	Peter Kandzia, On the Most Recent Property of Algol-Like Programs, Proceedings of the 2nd Colloquium on Automata, Languages and Programming, p.97-111, July 29-August 02, 1974
	32	LANCMAACX, H. A proof of a theorem of Lipton on Hoare Logic and applications. Ber. 8003, Inst. Inf. Prakt. Math., Univ. Kiel, W. Germany, 1980.
	33	Hans Langmaack, On a theory of decision problems in programming languages, Proceedings of the International Conference on Mathematical Studies of Information Processing, p.538-558, August 23-26, 1978
	34	LANGMAACK, H. On termination problems for finitely interpreted ALGOL-like programs. Ber. 7904, Inst. Inf. Prakt. Math., Univ. Kiel, W. Germany, 1980.
	35	LANGMAACK, H. On correct procedure parameter transmission in higher programming languages. Acta Inf. 2 (1973), 110-142.
	36	Hans Langmaack , Ernst-Rüdiger Olderog, Present-Day Hoare-Like Systems for Programming Languages with Procedures: Power, Limits and most Likely Expressions, Proceedings of the 7th Colloquium on Automata, Languages and Programming, p.363-373, July 14-18, 1980
	37	LAUER, P.E. Consistent formal theories of the semantics of programming languages. Tech. Rep. TR.25.121, IBM Lab. Vienna, Austria, 1971.
	38	LIPTON, R.J. A necessary and sufficient condition for the existence of Hoare Logics. In Proc. 18th IEEE Symp. Foundations of Computer Science, 1977, pp. 1-6.
	39	LOMAZOVA, I.A. O slo~,nosti induktivnyh uslovii dlja verifikacii arifmetiSeskih programm (On the complexity of inductive assertions for the verification of arithmetical programs). In Materialy Wsesojuznoi Nau5noi Studen~eskoi Konferencii, Matematika, Novosibirsk State Uni{z., Novosibirsk, U.S.S.R., 1978, pp. 85-94.
	40	LONDON, R.L., GUTTA~, J.V., HORNING, J.J., LAMPSON, B.W., MITCHELL, J.G., AND POPEK, G.J. Proof rules for the programming language Euclid. Acta Inf. 10 (1978), 1-26.
	41	Clement L. McGowan, The “most recent” error: Its causes and correction, Proceedings of ACM conference on Proving assertions about programs, p.191-202, January 06-07, 1972, Las Cruces, New Mexico, United States
	42	MANNA, Z., AND PNUELI, A. Axiomatic approach to total correctness of programs. Acta Inf. 3 (1974), 253-263.
	43	Albert R. Meyer , Rohit Parikh, Definability in Dynamic Logic, Proceedings of the twelfth annual ACM symposium on Theory of computing, p.1-7, April 28-30, 1980, Los Angeles, California, United States [doi>10.1145/800141.804646]
	44	OLDEROG, E.R. General equivalence of expressivity definitions using strongest postconditions resp. weakest preconditions. Ber. 8007, Inst. Inf. Prakt. Math., Univ. Kiel, West Germany, 1980.
	45	OLDEROO, E.R. Sound and complete Hoare-like calculi based on copy rules. Ber. 7905, Inst. Inf. Prakt. Math., Univ. Kiel, West Germany, 1980; also Acta Inf., to appear.
	46	Derek C. Oppen , Stephen A. Cook, Proving assertions about programs that manipulate data structures, Proceedings of seventh annual ACM symposium on Theory of computing, p.107-116, May 05-07, 1975, Albuquerque, New Mexico, United States [doi>10.1145/800116.803758]
	47	OW~CKI, S., AND GRIES, D. An axiomatic proof technique for parallel programs I. Acta Inf. 6 (1976), 319-340.
	48	PRATT, V.R. Semantical considerations on Floyd-Hoare logic. Proc. 17th IEEE Symp. Foundations of Computer Science, 1976, pp. 109-121.
	49	PRESBURGER, M. Uber die VoUst~indigkeit eines gewissen Systems der Arithmetic ganzer Zahlen, in welchen die Addition als einzige Operation hervortritt. In C.R. ler Congr. de Math~maticiens de Pays Slavs, 1929.
	50	SCOTT, D., AND DE BAKKER, J.W. A theory of programs: Notes of an IBM Vienna seminar, 1969. Unpublished.
	51	SHOENFIELD, J.R. Mathematical Logic. Addison-Wesley, Reading, Mass., 1967.
	52	SOKOgOWSKi, S. Axioms for total correctness. Acta inf. 9 (1977), 61-72.
	53	SOKOr. OWSKI, S. Total correctness for procedures. In Lecture Notes in Computer Science, vol. 53: Proc. 6th Symp. Mathematical Foundations of Computer Science. Springer-Verlag, New York, 1977, pp. 475-483.
	54	Mitchell Wand, A New Incompleteness Result for Hoare's System, Journal of the ACM (JACM), v.25 n.1, p.168-175, Jan. 1978 [doi>10.1145/322047.322062]
	55	Niklaus Wirth , C. A. R. Hoare, A contribution to the development of ALGOL, Communications of the ACM, v.9 n.6, p.413-432, June 1966 [doi>10.1145/365696.365702]

CITED BY 43

	J. Widom , D. Gries , F. B. Schneider, Completeness and incompleteness of trace-based network proof systems, Proceedings of the 14th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.27-38, January 21-23, 1987, Munich, West Germany
	A. Udaya Shankar, An introduction to assertional reasoning for concurrent systems, ACM Computing Surveys (CSUR), v.25 n.3, p.225-262, Sept. 1993
	F. S. deBoer, A Hoare logic for dynamic networks of asychronously communicating deterministic processes, Theoretical Computer Science, v.274 n.1-2, p.3-41, March 6, 2002
	Andreas Blass , Yuri Gurevich, Inadequacy of computable loop invariants, ACM Transactions on Computational Logic (TOCL), v.2 n.1, p.1-11, Jan. 2001
	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
	Bart Jacobs , Joachim van den Berg , Marieke Huisman , Martijn van Berkum , U. Hensel , H. Tews, Reasoning about Java classes: preliminary report, ACM SIGPLAN Notices, v.33 n.10, p.329-340, Oct. 1998
	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
	Newcomb Greenleaf, Algorithms and proofs: mathematics in the computing curriculum, ACM SIGCSE Bulletin, v.21 n.1, p.268-272, Feb. 1989
	W. Richards Adrion , Martha A. Branstad , John C. Cherniavsky, Validation, Verification, and Testing of Computer Software, ACM Computing Surveys (CSUR), v.14 n.2, p.159-192, June 1982
	Leslie Lamport, The temporal logic of actions, ACM Transactions on Programming Languages and Systems (TOPLAS), v.16 n.3, p.872-923, May 1994
	Leslie Lamport, win and sin: predicate transformers for concurrency, ACM Transactions on Programming Languages and Systems (TOPLAS), v.12 n.3, p.396-428, July 1990
	Yongmei Liu, A hoare-style proof system for robot programs, Eighteenth national conference on Artificial intelligence, p.74-79, July 28-August 01, 2002, Edmonton, Alberta, Canada
	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
	W. Damm, A Microprogramming Logic, IEEE Transactions on Software Engineering, v.14 n.5, p.559-574, May 1988
	Jennifer Widom , David Gries , Fred B. Schneider, Trace-based network proof systems: expressiveness and completeness, ACM Transactions on Programming Languages and Systems (TOPLAS), v.14 n.3, p.396-416, July 1992
	Laurian M. Chirica , David F. Martin, Toward compiler implementation correctness proofs, ACM Transactions on Programming Languages and Systems (TOPLAS), v.8 n.2, p.185-214, April 1986
	Anders Møller , Michael I. Schwartzbach, The pointer assertion logic engine, ACM SIGPLAN Notices, v.36 n.5, p.221-231, May 2001
	M. Felder , D. Mandrioli , A. Morzenti, Proving Properties of Real-Time Systems Through Logical Specifications and Petri Net Models, IEEE Transactions on Software Engineering, v.20 n.2, p.127-141, February 1994
	K. R. Apt , G. D. Plotkin, Countable nondeterminism and random assignment, Journal of the ACM (JACM), v.33 n.4, p.724-767, Oct. 1986
	Ernie Cohen , Dexter Kozen, A note on the complexity of propositional Hoare logic, ACM Transactions on Computational Logic (TOCL), v.1 n.1, p.171-174, July 2000
	Saddek Bensalem , Yassine Lakhnech, Automatic Generation of Invariants, Formal Methods in System Design, v.15 n.1, p.75-92, July 1999
	J. Kljaich, Jr. , B. T. Smith , A. S. Wojcik, Formal Verification of Fault Tolerance Using Theorem-Proving Techniques, IEEE Transactions on Computers, v.38 n.3, p.366-376, March 1989
	Werner Damm, An axiomatization of low-level parallelism in microarchitectures, ACM SIGMICRO Newsletter, v.15 n.4, p.314-323, Dec. 1984
	Cliff B. Jones, The Early Search for Tractable Ways of Reasoning about Programs, IEEE Annals of the History of Computing, v.25 n.2, p.26-49, April 2003
	Sigurd Meldal, A complete axiomatic semantics of spawning, Distributed Computing, v.5 n.3, p.159-174, December 1991
	Shiyong Lu , Arthur Bernstein , Philip Lewis, Correct Execution of Transactions at Different Isolation Levels, IEEE Transactions on Knowledge and Data Engineering, v.16 n.9, p.1070-1081, September 2004
	Martin Berger , Kohei Honda , Nobuko Yoshida, A logical analysis of aliasing in imperative higher-order functions, ACM SIGPLAN Notices, v.40 n.9, September 2005
	Ernst-Rüdiger Olderog, A characterization of Hoare's logic for programs with Pascal-like procedures, Proceedings of the fifteenth annual ACM symposium on Theory of computing, p.320-329, December 1983
	Kohei Honda, From process logic to program logic, ACM SIGPLAN Notices, v.39 n.9, September 2004
	Cees Pierik , Frank S. de Boer, A proof outline logic for object-oriented programming, Theoretical Computer Science, v.343 n.3, p.413-442, 17 October 2005
	Xinyu Feng , Zhong Shao , Alexander Vaynberg , Sen Xiang , Zhaozhong Ni, Modular verification of assembly code with stack-based control abstractions, ACM SIGPLAN Notices, v.41 n.6, June 2006
	MARTIN BERGER , KOHEI HONDA , NOBUKO YOSHIDA, A logical analysis of aliasing in imperative higher-order functions, Journal of Functional Programming, v.17 n.4-5, p.473-546, July 2007
	Arthur Charlesworth, Comprehending software correctness implies comprehending an intelligence-related limitation, ACM Transactions on Computational Logic (TOCL), v.7 n.3, p.590-612, July 2006
	Ward Douglas Maurer, Generalized structured programs and loop trees, Science of Computer Programming, v.67 n.2-3, p.223-246, July, 2007
	Andrew Ireland , Jamie Stark, Combining Proof Plans with Partial Order Planning for Imperative Program Synthesis, Automated Software Engineering, v.13 n.1, p.65-105, January 2006
	Van Nguyen , David Gries , Susan Owicki, A model and temporal proof system for networks of processes, Proceedings of the 12th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.121-131, January 14-16, 1985, New Orleans, Louisiana, United States
	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
	Leslie Lamport , Fred B. Schneider, Constraints: a uniform approach to aliasing and typing, Proceedings of the 12th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.205-216, January 14-16, 1985, New Orleans, Louisiana, United States
	Bernhard Reus , Jan Schwinghammer, Denotational semantics for a program logic of objects, Mathematical Structures in Computer Science, v.16 n.2, p.313-358, April 2006
	Johan Dovland , Einar Broch Johnsen , Olaf Owe, Observable Behavior of Dynamic Systems: Component Reasoning for Concurrent Objects, Electronic Notes in Theoretical Computer Science (ENTCS), v.203 n.3, p.19-34, May, 2008
	Erika Ábrahám , Frank S. de Boer , Willem-Paul de Roever , Martin Steffen, A Deductive Proof System for Multithreaded Java with Exceptions, Fundamenta Informaticae, v.82 n.4, p.391-463, February 2008
	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
	F. S. de Boer, A shared-variable concurrency analysis of multi-threaded object-oriented programs, Theoretical Computer Science, v.410 n.2-3, p.128-141, February, 2009