Some Properties of Predicate Transformers

Subscribe (Full Service)


	Search: The ACM Digital Library The Guide

	Feedback

Some Properties of Predicate Transformers

Full text

Pdf (1.06 MB)

Source

Journal of the ACM (JACM) archive
Volume 25 , Issue 3 (July 1978) table of contents

Pages: 461 - 480

Year of Publication: 1978

ISSN:0004-5411

Author

C. A. R. Hoare

Oxford University Computing Laboratory, Programming Research Group, 45 Banbury Road, Oxford OX2 6PE, England and Queen's University, Belfast, Northern Ireland

Publisher

ACM New York, NY, USA

Bibliometrics

Downloads (6 Weeks): 2, Downloads (12 Months): 42, Citation Count: 12

Additional Information:

references cited by index terms collaborative colleagues peer to peer

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/322077.322088 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	BURSTALL, R~ M Program proving as hand simulation with a httle induction Information Processing 74, North-Holland, Amsterdam, 1974, pp 308-312
	2	oE BAKKER, J W Semantics and termmauon ofnondetermlmstlc programs Proc Third Int Colloqumm on Automata Languages and Programming, S Mlchaelson and R Mdner, Eds, Edinburgh U Press, Edinburgh, Scotland, July 1976, pp 435-477
	3	DE BAKKER, J W, AND DE ROEVER, W P A calculus for recurswe program schemes In Automata Languages and Programming, M Nlvat, Ed, North-Holland, Amsterdam, 1973, pp 167-196
	4	DE ROEVER, W P Dljkstra's predicate transformer, non-determinism, recurslon and termination Sprmger Lecture Notes m Computer Science 45 Mathematical Foundations of Computer Science, 1976, pp 472-481
	5	DIJKSTRA, E W Cooperating sequential processes In Programming Languages, F Genuys, Ed,/~cademlc Press, New York, p 196
	6	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]
	7	DIJKSTRA, E W A Dtsctphne of Programming Prentice-Hall, Englewood Chffs, N J, 1976,
	8	EGLI, H A mathematical model for nondetermlmstlc computations Zurich ETH, 1975
	9	Robert W. Floyd, Nondeterministic Algorithms, Journal of the ACM (JACM), v.14 n.4, p.636-644, Oct. 1967 [doi>10.1145/321420.321422]
	10	HOARE, C A R, AND LAUER, P E Consistent and complementary formal theories of the semantics of programming languages Acta Informauca 3 (1974), 135-153.
	11	LAUER, P E Consistent formal theories of the semantics of programming languages Ph D Th, Queen's U, Belfast, N Ireland, Tech Rep TR 25 121, IBM Lab, Vienna, Nov 1971.
	12	Zohar Manna , Richard Waldinger, Is “sometime” sometimes better than “always”?: intermittent assertions in proving program correctness, Communications of the ACM, v.21 n.2, p.159-172, Feb. 1978 [doi>10.1145/359340.359353]
	13	RUSSELL, B Introductwn to Mathematical Phdosophy Allen & Unwm, 1919
	14	SCOTT, D., AND STRACBEY, C Toward a mathemaucal semanucs for computer languages. Oxford U. PRG6, Oxford, Aug 1971

CITED BY 12

	Ravi Sethi, A case study in specifying the semantics of a programming language, Proceedings of the 7th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.117-130, January 28-30, 1980, Las Vegas, Nevada
	I. Greif , A. Meyer, Specifying programming language semantics: a tutorial and critique of a paper by Hoare and Lauer, Proceedings of the 6th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.180-189, January 29-31, 1979, San Antonio, Texas
	Michael Johnson , David Naumann , John Power, Category Theoretic Models of Data Refinement, Electronic Notes in Theoretical Computer Science (ENTCS), 225, p.21-38, January, 2009
	Irene Greif , Albert R. Meyer, Specifying the Semantics of while Programs: A Tutorial and Critique of a Paper by Hoare and Lauer, ACM Transactions on Programming Languages and Systems (TOPLAS), v.3 n.4, p.484-507, Oct. 1981
	Patrick Cousot , Radhia Cousot, Systematic design of program analysis frameworks, Proceedings of the 6th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.269-282, January 29-31, 1979, San Antonio, Texas
	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
	George S. Avrunin , Jack C. Wileden, Describing and analyzing distributed software system designs, ACM Transactions on Programming Languages and Systems (TOPLAS), v.7 n.3, p.380-403, July 1985
	Albert R. Meyer , Joseph Y. Halpern, Axiomatic Definitions of Programming Languages: A Theoretical Assessment, Journal of the ACM (JACM), v.29 n.2, p.555-576, April 1982
	Bruno Blanchet, Escape analysis: correctness proof, implementation and experimental results, Proceedings of the 25th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.25-37, January 19-21, 1998, San Diego, California, United States
	David Harel, Recursion in logics of programs, Proceedings of the 6th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.81-92, January 29-31, 1979, San Antonio, Texas
	Mikkel Nygaard , Glynn Winskel, Domain theory for concurrency, Theoretical Computer Science, v.316 n.1-3, p.153-190, 28 May 2004
	Patrick Cousot, Constructive design of a hierarchy of semantics of a transition system by abstract interpretation, Theoretical Computer Science, v.277 n.1-2, p.47-103, April 28, 2002