Browse Prior Art Database

An Early Program Proof by Alan Turing

IP.com Disclosure Number: IPCOM000129447D
Original Publication Date: 1984-Apr-01
Included in the Prior Art Database: 2005-Oct-06
Document File: 6 page(s) / 27K

Publishing Venue

Software Patent Institute

Related People

F. L. MORRIS: AUTHOR [+3]

Abstract

The paper reproduces, with typographical corrections and comments, a 1949 paper by Alan Turing that foreshadows much subsequent work in program proving.

This text was extracted from a PDF file.
This is the abbreviated version, containing approximately 19% of the total text.

Page 1 of 6

THIS DOCUMENT IS AN APPROXIMATE REPRESENTATION OF THE ORIGINAL.

Copyright ©; 1984 by the American Federation of Information Processing Societies, Inc. Used with permission.

An Early Program Proof by Alan Turing

F. L. MORRIS

C. B. JONES

  (Image Omitted: © 1984 by the American Federation of Information Processing societies, Inc Permission to copy without fee all or part of this material is granted provided that the copies are not made or distributed for direct commercial advantage, the AFIPS copyright notice and the title of the publication and its date appear, and notice is given that the copying is by permission of the American Federation of Information Processing Societies, Inc. To copy otherwise, or to republish, requires specific permission. Authors' Addresses: F. L. Morris, School of Computer and Information Science, 313 Link Hall, Syracuse university' Syracuse, NY 13210. C. B. Jones, Department of Computer Science, The university, Manchester Ml3 9PL, England. © 1984

AFIPS 0164-1239/84/020139-143

An Early Program Proof by Alan Turing

F. L. MORRIS

C. B. JONES .00/00)

The paper reproduces, with typographical corrections and comments, a 1949 paper by Alan Turing that foreshadows much subsequent work in program proving.

Categories and Subject Descriptors: D. 2.4 [Software Engineering] -- correctness proofs; .3.1 [Logics and Meanings of Programs] -- assertions; K. 2 [History of Computing] -- software General Terms: Verification Additional Key Words and Phrases: A. M. Turing

Introduction

The standard references for work on program proofs attribute the early statement of direction to John McCarthy (e.g., McCarthy 1963); the first workable methods to Peter Naur (1966) and Robert Floyd (1967); and the provision of more formal systems to C. A. R. Hoare (1969) and Edsger Dijkstra (1976). The early papers of some of the computing pioneers, however, show an awareness of the need for proofs of program correctness and even present workable methods (e.g., Goldstine and von Neumann 1947; Turing 1949).

The 1949 paper by Alan M. Turing is remarkable in many respects. The three (foolscap) pages of text contain an excellent motivation by analogy, a proof of a program with two nested loops, and an indication of a general proof method very like that of Floyd. Unfortunately, the paper is made extremely difficult to read by the large number of transcription errors. For example, all instances of the factorial sign (Turing used |n) have been omitted in the commentary, and ten other identifiers are written incorrectly. It would appear to be worth correcting these errors and commenting on the proof from the viewpoint of subsequent work on program proofs.

IEEE Computer Society, Apr 01, 1984 Page 1 IEEE Annals of the History of Computing Volume 6 Number 2, Pages 139-143

Page 2 of 6

An Early Program Proof by Alan Turing

Turing delivered this paper in June 1949, at the inaugural conference of the EDSAC, the computer at Cambridge University built under the dire...