Predicative programming Part I

Subscribe (Full Service)


	Search: The ACM Digital Library The Guide

	Feedback

Predicative programming Part I

Full text

Pdf (754 KB)

Source

Communications of the ACM archive
Volume 27 , Issue 2 (February 1984) table of contents

Pages: 134 - 143

Year of Publication: 1984

ISSN:0001-0782

Author

Eric C. R. Hehner

Univ. of Toronto, Toronto, Ont., Canada

Publisher

ACM New York, NY, USA

Bibliometrics

Downloads (6 Weeks): 3, Downloads (12 Months): 28, Citation Count: 14

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

ABSTRACT

Programs are given a new semantics with the merit that a specification written as a first-order predicate can be refined, step by step, to a program via the rules of Predicate Calculus. The semantics allows a free mixture of predicate and programming notations, and manipulation of programs.

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.

	0	Ashcroft, E.A. and Wadge, W.W. LUCID--A formal system for writing and proving programs, Siam J. Comp. 5 (1976), 336-354.
	1	John Backus, Can programming be liberated from the von Neumann style?: a functional style and its algebra of programs, Communications of the ACM, v.21 n.8, p.613-641, Aug. 1978 [doi>10.1145/359576.359579]
	2	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]
	3	Edsger Wybe Dijkstra, A Discipline of Programming, Prentice Hall PTR, Upper Saddle River, NJ, 1997
	4	M. H. Van Emden , R. A. Kowalski, The Semantics of Predicate Logic as a Programming Language, Journal of the ACM (JACM), v.23 n.4, p.733-742, Oct. 1976 [doi>10.1145/321978.321991]
	5	Floyd, R.W. Assigning meaning to programs. Math. Aspects of Cornput. Sci. 19, (1967), 19-32.
	6	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]
	7	Hoare, C.A.R. ls there a mathematical basis for computer programming? NAG Newsletter 2 (Sept. 1981), 6-14.
	8	Cliff B. Jones, Software Development: A Rigorous Approach, Prentice Hall PTR, Upper Saddle River, NJ, 1980
	9	Lassez, J.-L., Nguyen, V.L., Sonenburg, E.A. Fixed-point theorems and semantics: A folk tale. Inf. Proc. Let. 14, 3 (May 16, 1982), 112- 116.
	10	David Lorge Parnas, A generalized control structure and its formal definition, Communications of the ACM, v.26 n.8, p.572-581, Aug. 1983 [doi>10.1145/358161.358168]
	11	Scott, D.S. Outline of a mathematical theory of computation. Proc. 4th Annual Princeton Conf. Inf. Sci. Syst., Department of Electrical Engineering, Princeton University, Princeton, NJ, 1970 and Tech. Rpt. PRG-2, Programming Research Group, Oxford University, 1970.

CITED BY 14

	C. A. R. Hoare , I. J. Hayes , He Jifeng , C. C. Morgan , A. W. Roscoe , J. W. Sanders , I. H. Sorensen , J. M. Spivey , B. A. Sufrin, Laws of programming, Communications of the ACM, v.30 n.8, p.672-686, Aug. 1987
	Greg Nelson, A generalization of Dijkstra's calculus, ACM Transactions on Programming Languages and Systems (TOPLAS), v.11 n.4, p.517-561, Oct. 1989
	J. Zwiers , W. Roever, Predicates are predicate transformers: a unified compositional theory for concurrency, Proceedings of the eighth annual ACM Symposium on Principles of distributed computing, p.265-279, June 1989, Edmonton, Alberta, Canada
	Ali Mili , Jules Desharnais , Jean Raynomd Gagné, Formal models of stepwise refinements of programs, ACM Computing Surveys (CSUR), v.18 n.3, p.231-276, Sept. 1986
	Hans-Juergen Boehm, Side effects and aliasing can have simple axiomatic descriptions, ACM Transactions on Programming Languages and Systems (TOPLAS), v.7 n.4, p.637-655, Oct. 1985
	Johan Agat, Transforming out timing leaks, Proceedings of the 27th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.40-53, January 19-21, 2000, Boston, MA, USA
	Simon S. Lam , A. Udaya Shankar, A Relational Notation for State Transition Systems, IEEE Transactions on Software Engineering, v.16 n.7, p.755-775, July 1990
	CORPORATE Tech Correspondence, Technical correspondence, Communications of the ACM, v.28 n.5, p.534-538, May 1985
	CORPORATE Tech Correspondence, Technical correspondence, Communications of the ACM, v.28 n.5, p.534-538, May 1985
	Mark Saaltink, Relational semantics, ACM SIGSOFT Software Engineering Notes, v.10 n.4, August 1985
	Dennis K. Peters , David Lorge Parnas, Using Test Oracles Generated from Program Documentation, IEEE Transactions on Software Engineering, v.24 n.3, p.161-173, March 1998
	David Lorge Parnas , Jan Madey , Michal Iglewski, Precise Documentation of Well-Structured Programs, IEEE Transactions on Software Engineering, v.20 n.12, p.948-976, December 1994
	Fairouz Tchier, Demonic fixed points, Acta Cybernetica, v.17 n.3, p.533-555, January 2006
	David Lorge Parnas, Document based rational software development, Knowledge-Based Systems, v.22 n.3, p.132-141, April, 2009