Predicative programming Part II

Subscribe (Full Service)


	Search: The ACM Digital Library The Guide

	Feedback

Predicative programming Part II

Full text

Pdf (650 KB)

Source

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

Pages: 144 - 151

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): 2, Downloads (12 Months): 16, Citation Count: 7

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.357990 What is a DOI?

ABSTRACT

Part I of this two-part paper presented a new semantics of programs. Each program is considered to be a predicate, in a restricted notation, that specifies the observable behavior of a computer executing the program. We considered a variety of notations, including assignment, composition (semicolon), deterministic choice (if), nondeterministic choice, definition (nonrecursive and recursive), and variable declaration. We did not consider any input or output notations, or concurrency; that is the subject of Part II. We assume the reader is familiar with Part I, so that we can build on ideas presented there.

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	J. Dean Brock , William B. Ackerman, Scenarios: A Model of Non-Determinate Computation, Proceedings of the International Colloquium on Formalization of Programming Concepts, p.252-259, April 19-25, 1981
	1	Hehner, E.C.R., and Hoare, C.A.R. A more complete model of communicating processes. Theor. Comput. Sci. 26 (1983), 105-120.
	2	C. A. R. Hoare, Communicating sequential processes, Communications of the ACM, v.21 n.8, p.666-677, Aug. 1978 [doi>10.1145/359576.359585]
	3	Hoare, C.A.R. A calculus of total correctness for communicating processes. Sci. Comput. Program. 1 (1981), 49-72.
	4	Hoare, C.A.R. Specifications, programs, and implementations. Technical Monograph PRG-29, Oxford University Computing Laboratory (Programming Research Group), June 1982.
	5	Kahn, G., MacQueen, D.B. Coroutines and networks of parallel processes In: Information Processing 77. Proceedings of IFIP Congress 77, Elsevier North-Holland, Inc., New York, 1977, 993-998.
	6	Lengauer, C. and Hehner, E.C.R. A methodology for programming with concurrency: An informal presentation. Sci. Comput. Program. 2 (1982) 1-18.

CITED BY 7

	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
	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 , Lawrence C. Paulson, Should your specification language be typed, ACM Transactions on Programming Languages and Systems (TOPLAS), v.21 n.3, p.502-526, May 1999
	Manfred Broy, Declarative specification and declarative programming, Proceedings of the 6th international workshop on Software specification and design, October 25-26, 1991, Como, Italy
	Stefan Ratschan, Convergent approximate solving of first-order constraints by approximate quantifiers, ACM Transactions on Computational Logic (TOCL), v.5 n.2, p.264-281, April 2004
	C. A. R. Hoare, Assertions: A Personal Perspective, IEEE Annals of the History of Computing, v.25 n.2, p.14-25, April 2003
	Martin Fränzle , Christian Herde, HySAT: An efficient proof engine for bounded model checking of hybrid systems, Formal Methods in System Design, v.30 n.3, p.179-198, June 2007