Is Sometimes Ever Better Than Always?

Subscribe (Full Service)


	Search: The ACM Digital Library The Guide

	Feedback

Is Sometimes Ever Better Than Always?

Full text

Pdf (476 KB)

Source

ACM Transactions on Programming Languages and Systems (TOPLAS) archive
Volume 1 , Issue 2 (October 1979) table of contents

Pages: 258 - 265

Year of Publication: 1979

ISSN:0164-0925

Author

David Gries

Computer Science Department, Upson Hall, Cornell University, Ithaca, NY

Publisher

ACM New York, NY, USA

Bibliometrics

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

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

ABSTRACT

The “intermittent assertion” method for proving programs correct is explained and compared with the conventional method. Simple conventional proofs of iterative algorithms that compute recursively defined functions, including Ackermann's function, are given.

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 little induction. Proc. IFIP Congress 1974, Amsterdam, The Netherlands, pp. 308-312.
	2	Edsger Wybe Dijkstra, A Discipline of Programming, Prentice Hall PTR, Upper Saddle River, NJ, 1997
	3	GRIES, D. The Schorr-Waite graph marking algorithm. To appear in Acta Informatica.
	4	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]
	5	Donald E. Knuth, The art of computer programming, volume 1 (3rd ed.): fundamental algorithms, Addison Wesley Longman Publishing Co., Inc., Redwood City, CA, 1997
	6	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]
	7	TOPOR, R.W. A simple proof of the Schorr-Waite garbage collection algorithm. To appear in Acta Informatica.

CITED BY 4

	H. J. Boom, A Weaker Precondition for Loops, ACM Transactions on Programming Languages and Systems (TOPLAS), v.4 n.4, p.668-677, Oct. 1982
	Ali Mili, A case for teaching program verification: Its importance in the CS curriculum, ACM SIGCSE Bulletin, v.15 n.1, p.2-6, February 1983
	Douglas D. Dunlop , Victor R. Basili, Generalizing specifications for uniformly implemented loops, ACM Transactions on Programming Languages and Systems (TOPLAS), v.7 n.1, p.137-158, Jan. 1985
	Ali Mili , Jules Desharnais, A system for classifying program verification methods: Assigning meanings to program verification methods, Proceedings of the 7th international conference on Software engineering, p.499-509, March 26-29, 1984, Orlando, Florida, United States