Second-order mathematical theory of computation

Subscribe (Full Service)


	Search: The ACM Digital Library The Guide

	Feedback

Second-order mathematical theory of computation

Full text

Pdf (654 KB)

Source

Annual ACM Symposium on Theory of Computing archive
Proceedings of the second annual ACM symposium on Theory of computing table of contents

Northampton, Massachusetts, United States

Pages: 158 - 168

Year of Publication: 1970

Author

Zohar Manna

Computer Science Department, Stanford University

Sponsor

SIGACT: ACM Special Interest Group on Algorithms and Computation Theory

Publisher

ACM New York, NY, USA

Bibliometrics

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

Additional Information:

abstract 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/800161.805161 What is a DOI?

ABSTRACT

In this work we show that it is possible to formalize all properties regularly observed in (deterministic and non-deterministic) algorithms in second-order predicate calculus. Moreover, we show that for any given algorithm it suffices to know how to formalize its 'partial correctness' by a second-order formula in order to formalize all other properties by second-order formulas. This result is of special interest since 'partial correctness' has already been formalized in second-order predicate calculus for many classes of algorithms.

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	E. A. ASHCROFT, "Mathematical Logic Applied to the Semantics of Computer Programs",Ph.D. Thesis, to be submitted to Imperial College, London (1970).
	2	E. A. ASHCROFT and Z. MANNA, "Formalization of Properties of Parallel Programs", Computer Science Department, Stanford University, Artificial Intelligence Memo AIM-110 (February 1970).
	3	R. M. BURSTALL, "Formal Description of Program Structure and Semantics in First-Order Logic", in Machine Intelligence 5 (Eds. Meltzer and Michie), Edinburgh University Press, 79-98 (1970).
	4	D. C. COOPER, "Program Scheme Equivalences and Second-Order Logic", in Machine Intelligence 4 (Eds. Meltzer and Michie), Edinburgh University Press, 3-15 (1969).
	5	D. C. COOPER, "Program Schemes, Programs and Logic", Computation Services Department, University College of Swansea, Memo No. 6 (April 1969).
	6	R. W. FLOYD, "Assigning Meaning to Programs", in Proceedings of Symposia in Applied Mathematics, American Mathematical Society,Vol. 19, 19-32 (1967).
	7	Z. MANNA, "The Correctness of Programs", J. of Computer and System Sciences, Vol. 3, No. 2, 119-127 (1969).
	8	Zohar Manna, Properties of Programs and the First-Order Predicate Calculus, Journal of the ACM (JACM), v.16 n.2, p.244-255, April 1969 [doi>10.1145/321510.321516]
	9	Z. MANNA, "The Correctness of Non-deterministic Programs", Artificial Intelligence J., Vol. 1, No. 1 (1970).
	10	Zohar Manna , Amir Pnueli, Formalization of Properties of Functional Programs, Journal of the ACM (JACM), v.17 n.3, p.555-569, July 1970 [doi>10.1145/321592.321606]
	11	D. PARK, "Fixpoint Induction and Proofs of Program Properties", in Machine Intelligence 5 (Eds. Meltzer and Michie), Edinburgh University Press, 59-78 (1970).

CITED BY 6

	Vaughan R. Pratt, The competence/performance dichotomy in programming preliminary report, Proceedings of the 4th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.194-200, January 17-19, 1977, Los Angeles, California
	David Harel , Vaughan R. Pratt, Nondeterminism in logics of programs, Proceedings of the 5th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.203-213, January 23-25, 1978, Tucson, Arizona
	Bernard Elspas , Karl N. Levitt , Richard J. Waldinger , Abraham Waksman, An Assessment of Techniques for Proving Program Correctness, ACM Computing Surveys (CSUR), v.4 n.2, p.97-147, June 1972
	Mordechai Ben-Ari , Zohar Manna , Amir Pnueli, The temporal logic of branching time, Proceedings of the 8th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.164-176, January 26-28, 1981, Williamsburg, Virginia
	Laurian M. Chirica , David F. Martin, An approach to compiler correctness, ACM SIGPLAN Notices, v.10 n.6, p.96-103, June 1975
	Michal Armoni , Mordechai Ben-Ari, The concept of nondeterminism: its development and implications for teaching, ACM SIGCSE Bulletin, v.41 n.2, June 2009