Laws of programming

Subscribe (Full Service)


	Search: The ACM Digital Library The Guide

	Feedback

Laws of programming

Full text

Pdf (1.50 MB)

Source

Communications of the ACM archive
Volume 30 , Issue 8 (August 1987) table of contents

Pages: 672 - 686

Year of Publication: 1987

ISSN:0001-0782

Authors

C. A. R. Hoare	Univ. of Texas, Austin
I. J. Hayes	Univ. of Queensland, Australia
He Jifeng	Oxford Univ., Oxford, UK
C. C. Morgan	Oxford Univ., Oxford, UK
A. W. Roscoe	Oxford Univ., Oxford, UK
J. W. Sanders	Oxford Univ., Oxford, UK
I. H. Sorensen	Oxford Univ., Oxford, UK
J. M. Spivey	Oxford Univ., Oxford, UK
B. A. Sufrin	Oxford Univ., Oxford, UK

Publisher

ACM New York, NY, USA

Bibliometrics

Downloads (6 Weeks): 14, Downloads (12 Months): 92, Citation Count: 34

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

ABSTRACT

A complete set of algebraic laws is given for Dijkstra's nondeterministic sequential programming language. Iteration and recursion are explained in terms of Scott's domain theory as fixed points of continuous functionals. A calculus analogous to weakest preconditions is suggested as an aid to deriving programs from their specifications.

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	Roland C. Backhouse, Program construction and verification, Prentice-Hall, Inc., Upper Saddle River, NJ, 1986
	2	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]
	3	J. W. de Bakker, Mathematical Theory of Program Correctness, Prentice-Hall, Inc., Upper Saddle River, NJ, 1980
	4	Edsger Wybe Dijkstra, A Discipline of Programming, Prentice Hall PTR, Upper Saddle River, NJ, 1997
	5	David Gries, The Science of Programming, Springer-Verlag New York, Inc., Secaucus, NJ, 1987
	6	Eric C. R. Hehner, Predicative programming Part I, Communications of the ACM, v.27 n.2, p.134-143, Feb. 1984 [doi>10.1145/69610.357988]
	7	Hoare, C.A.R., and He, J. Weakest prespecification. Tech. Monogr. PRG-44, Programming Research Group, Oxford Univ., 1985.
	8	Igarishi, S. An axiomatic approach to equivalence problems of algorithms with applications. Rep., Computer Centre, Univ. of Tokyo, 1968.
	9	Cliff B. Jones, Software Development: A Rigorous Approach, Prentice Hall PTR, Upper Saddle River, NJ, 1980
	10	R. Kowalski, The relation between logic programming and logic specification, Proc. of a discussion meeting of the Royal Society of London on Mathematical logic and programming languages, p.11-27, June 1985, London, United Kingdom
	11	Roscoe, A.W. Laws of Occam programming. Tech. Monogr. PRG-53, Programming Research Group, Oxford Univ., 1986.
	12	Scott, D.S. Outline of a mathematical theory of computetion. Tech. Monogr. PRCX!, Programming Research Group, Oxford Univ., 1970.
	13	Tarski, A. On the calculus of relations. J. Symbolic Logic 6 (1941), 73-89.

CITED BY 35

	P. H. Welch, An OCCAM approach to transputer engineering, Proceedings of the third conference on Hypercube concurrent computers and applications: Architecture, software, computer systems, and general issues, p.138-147, January 19-20, 1988, Pasadena, California, United States
	Martin Odersky , Dan Rabin , Paul Hudak, Call by name, assignment, and the lambda calculus, Proceedings of the 20th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.43-56, March 1993, Charleston, South Carolina, United States
	E. J. Weyuker, The evaluation of program-based software test data adequacy criteria, Communications of the ACM, v.31 n.6, p.668-675, June 1988
	Lamia Labed Jilani , Jules Desharnais , Ali Mili, Defining and Applying Measures of Distance Between Specifications, IEEE Transactions on Software Engineering, v.27 n.8, p.673-703, August 2001
	P. A. Luker, Never mind the language, what about the paradigm?, ACM SIGCSE Bulletin, v.21 n.1, p.252-256, Feb. 1989
	C. A. R. Hoare, Algebra and models, ACM SIGSOFT Software Engineering Notes, v.18 n.5, p.1-8, Dec. 1993
	William G. Griswold , David Notkin, Automated assistance for program restructuring, ACM Transactions on Software Engineering and Methodology (TOSEM), v.2 n.3, p.228-269, July 1993
	William G. Griswold, Direct update of data flow representations for a meaning-preserving program restructuring tool, ACM SIGSOFT Software Engineering Notes, v.18 n.5, p.42-55, Dec. 1993
	J. A. Bergstra , T. B. Dinesh , J. Field , J. Heering, Toward a complete transformational toolkit for compilers, ACM Transactions on Programming Languages and Systems (TOPLAS), v.19 n.5, p.639-684, Sept. 1997
	R. Mili , M. Frappier , J. Desharnais , A. Mili, A calculus of program modifications, ACM SIGSOFT Software Engineering Notes, v.22 n.3, p.157-168, May 1997
	John Launchbury , Amr Sabry, Monadic state: axiomatization and type safety, ACM SIGPLAN Notices, v.32 n.8, p.227-238, Aug. 1997
	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
	Robin A. Nicholl , Tina M. Nicholl, Performing geometric transformations by program transformation, ACM Transactions on Graphics (TOG), v.9 n.1, p.28-40, Jan. 1990
	J. Field , J. Heering , T. B. Dinesh, Equations as a uniform framework for partial evaluation and abstract interpretation, ACM Computing Surveys (CSUR), v.30 n.3es, Sept. 1998
	Qin Shengchao , He Jifeng , Qiu Zongyan , Zhang Naixiao, An algebraic hardware/software partitioning algorithm, Journal of Computer Science and Technology, v.17 n.3, p.284-294, May 2002
	V. Cortellessa , D. Del Gobbo , M. Shereshevsky , J. Desharnais , A. Mili, Relational characterizations of system fault tolerance, Science of Computer Programming, v.56 n.3, p.343-361, May/June 2005
	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
	M. P. Ward, Pigs from sausages? Reengineering from assembler to C via FermaT transformations, Science of Computer Programming, v.52 n.1-3, p.213-255, August 2004
	Paulo Borba , Augusto Sampaio , Ana Cavalcanti , Márcio Cornélio, Algebraic reasoning for object-oriented programming, Science of Computer Programming, v.52 n.1-3, p.53-100, August 2004
	Jawed Siddiqi , Ian Morrey , Richard Hibberd , Graham Buckberry, Understanding and exploring formal specifications, Annals of Software Engineering, v.6 n.1-4, p.411-432, April 1999
	Leonardo Cole , Paulo Borba, Deriving refactorings for AspectJ, Proceedings of the 4th international conference on Aspect-oriented software development, p.123-134, March 14-18, 2005, Chicago, Illinois
	Joep L. W. Kessels, Calculational derivation of a counter with bounded response time and bounded power dissipation, Distributed Computing, v.8 n.3, p.143-149, March 1995
	Rohit Gheyi , Tiago Massoni, Formal refactorings for object models, Companion to the 20th annual ACM SIGPLAN conference on Object-oriented programming, systems, languages, and applications, October 16-20, 2005, San Diego, CA, USA
	Fairouz Tchier, Demonic fixed points, Acta Cybernetica, v.17 n.3, p.533-555, January 2006
	J. A. Bergstra , C. A. Middelburg, Splitting bisimulations and retrospective conditions, Information and Computation, v.204 n.7, p.1083-1138, July 2006
	Gary T. Leavens , Jean-Raymond Abrial , Don Batory , Michael Butler , Alessandro Coglio , Kathi Fisler , Eric Hehner , Cliff Jones , Dale Miller , Simon Peyton-Jones , Murali Sitaraman , Douglas R. Smith , Aaron Stump, Roadmap for enhanced languages and methods to aid verification, Proceedings of the 5th international conference on Generative programming and component engineering, October 22-26, 2006, Portland, Oregon, USA
	He Jifeng , Xiaoshan Li , Zhiming Liu, rCOS: a refinement calculus of object systems, Theoretical Computer Science, v.365 n.1, p.109-142, 10 November 2006
	Alban Ponse , Mark B. van der Zwaag, Belnap's logic and conditional composition, Theoretical Computer Science, v.388 n.1-3, p.319-336, December, 2007
	Dines Bjørner, Pinnacles of software engineering: 25 years of formal methods, Annals of Software Engineering, v.10 n.1-4, p.11-66, 2000
	Yingxu Wang, The Real-Time Process Algebra (RTPA), Annals of Software Engineering, v.14 n.1-4, p.235-274, December 2002
	Ali Mili, Desert Island Column: The Long Story of a Short Theorem, Automated Software Engineering, v.6 n.2, p.199-204, April 1999
	V. Dagdilelis , M. Satratzemi, Post's Machine: A Didactic Microworld as an Introduction to Formal Programming, Education and Information Technologies, v.6 n.2, p.123-141, June 2001
	David A. Naumann, A categorical model for higher order imperative programming, Mathematical Structures in Computer Science, v.8 n.4, p.351-399, August 1998
	Sanjay Misra , A. K. Misra, A proposed additional property to the Weyuker's existing properties, International Journal of Information Technology and Management, v.5 n.1, p.66-76, January 2006
	Benjamin H. Y. Koo , Willard L. Simmons , Edward F. Crawley, Algebra of systems: a metalanguage for model synthesis and evaluation, IEEE Transactions on Systems, Man, and Cybernetics, Part A: Systems and Humans, v.39 n.3, p.501-513, May 2009