Subscribe
Issue No.02 - April-June (2003 vol.25)
pp: 26-49
Cliff B. Jones , University of Newcastle-upon-Tyne
ABSTRACT
<p>This article traces the history-up to around 1990-of research on reasoning about programs. The main focus is on sequential imperative programs but some comments are made on concurrency. The main thesis is that the idea of reasoning about programs has been around since they were first written; the search has been to find tractable methods.</p>
CITATION
Cliff B. Jones, "The Early Search for Tractable Ways of Reasoning about Programs", IEEE Annals of the History of Computing, vol.25, no. 2, pp. 26-49, April-June 2003, doi:10.1109/MAHC.2003.1203057
REFERENCES
 1. This article is not a true history; for one thing, I am not a historian. My biases and a selective knowledge make the current text open to criticism. At best, this article will provide a source for subsequent historical research. One topic that is largely ignored here is that of numerical analysis. 2. A.M. Turing, "On Computable Numbers, with an Application to the Entscheidungsproblem," Proc. London Mathematical Soc., Series 2, vol. 42, pp. 230-265, 1936. Correction published ibid., vol. 43, pp. 544-546, 1937. Reprinted in M. Davis,The Undecidable,Raven Press, 1965, pp. 115-154. 3. Normally, just Tony Hoare, but references show all initials. 4. Brian Randell has pointed out that a concern with correctness was already present in the pre-electronic phase: Charles Babbage (1791-1871) wrote about the "Verification of the Formulae Placed on the [Operation] Cards." See B. Randell, The Origins of Digital Computers: Selected Papers, Springer-Verlag, 2nd ed., 1975, pp. 45-47. Konrad Zuse'sPlankalkulis one of the earliest programming languages (see K. Zuse,Der Computer: Mein Lebenswerk,Springer-Verlag, 1984); Heinz Zemanek has kindly checked with Zuse and confirms that the concern was shared but that there were no specific provisions for correctness arguments. 5. H.H. Goldstine and J. von Neumann, "Planning and Coding of Problems for an Electronic Computing Instrument," 1947, part II, vol. 1 of a report prepared for US Army Ordnance Dept.; republished as pp. 80-151 ofJohn von Neumann: Collected Works,vol. V,Design of Computers, Theory of Automata and Numerical Analysis,A.H. Taub, ed., Pergamon Press, 1963. 6. A.H. Taub ed. John von Neumann: Collected Works, vol. V, Design of Computers, Theory of Automata and Numerical Analysis, Pergamon Press, 1963, pp. 81-82. 7. Ibid., p. 83. 8. Ibid., p. 92. 9. Ibid., p. 98. 10. Ibid., p. 100. 11. Ibid., pp. 84 and 92. 12. A.M. Turing, "Checking a Large Routine," Report of a Conference on High Speed Automatic Calculating Machines, Univ. Mathematical Laboratory, Cambridge, UK, June 1949, pp. 67-69. The printed text of Turing's paper contains so many transcription errors that it took considerable effort to decipher. For a corrected version that is also related to later work, see F.L. Morris and C.B. Jones, "An Early Program Proof by Alan Turing,"Annals of the History of Computing,vol. 6, no. 2, Apr. 1984, pp. 139-143. 13. A. Hodges, Alan Turing, The Enigma.New York: Simon and Schuster, 1983. 14. J.A.N. Lee pointed out that John McCarthy said of the design of inter alia Algol 60: "It was stated that everyone was a gentleman and no one would propose something that he didn't know how to implement."See R.L. Wexelblat, ed., History of Programming Languages, Academic Press, 1981. 15. J. McCarthy, "A Basis for a Mathematical Theory for Computation," Computer Programming and Formal Systems, P. Braffort and D. Hirschberg, eds., North-Holland, 1963, pp. 33-70. 16. J. McCarthy, "Recursive Functions of Symbolic Expressions and their Computation by Machine," Comm. ACM, vol. 3, no. 4, Apr. 1960, pp. 184-195. 17. J. McCarthy, "Towards a Mathematical Science of Computation," Proc. Information Processing '62, C.M. Popplewell, ed., North-Holland, 1963, pp. 21-28. 18. Edsger Wybe Dijkstra described in his Turing Award lecture (E.W. Dijkstra, "The Humble Programmer,"Comm. ACM, vol. 15, no. 10, 1972, pp. 453-457) how his decision to work in computing was influenced by van Wijngaarden. 19. A. van Wijngaarden, "Numerical Analysis as an Independent Science," BIT, vol. 6, no. 1, 1966, pp. 66-81. (Text of 1964 talk.) 20. As mentioned, little is said here about the problems on numerical analysis. In fact, most early research on reasoning about programs was confined to discrete data—a notable exception is found in T.E. Hull, W.H. Enright, and A.E. Sedgwick, "The Correctness of Numerical Algorithms," ACM SIGPLAN Notices, vol. 7, no. 1, Jan. 1972, pp. 66-73. 21. P. Naur, "Proof of Algorithms by General Snapshots," BIT, vol. 6, no. 4, 1966, pp. 310-316. 22. R.W. Floyd, "Assigning Meanings to Programs," Proc. Symp. in Applied Mathematics, Vol.19: Mathematical Aspects of Computer Science, Am. Mathematical Soc., 1967, pp. 19-32. 23. Naur was to develop his ideas, together with others on action clusters (see P. Naur, "Programming by Action Clusters," BIT, vol. 9, no. 3, 1969, pp. 250-258) and to fit them into his thoughtful but too little known book P. Naur,Concise Survey of Computer Methods,Studentlitteratur, 1974. 24. This is presumably the reason that Maurice Wilkes argues (M.V. Wilkes, Memoirs of a Computer Pioneer, MIT Press, 1985) that Turing (see Ref. 12) did not anticipate Floyd"s contribution: "Turing did use the word 'assertion' and he did point out the separate need to show the execution of the program would terminate. What was missing was the concept of loop invariant." 25. S. Gorn,"Common Programming Language Task: Final Report," Contract No. DA-36-039-SC-75047, DA Proj. No. 3-28-01-201, PR and C No. 58-ELC/D-4457, Part I, Section 5: "On The Logical Design of Formal Mixed Languages," 1959. 26. C.A.R. Hoare, "An Axiomatic Basis for Computer Programming," Comm. ACM, 1969. 27. T.B. Steel, Formal Language Description Languages for Computer Programming,North-Holland, 1966. 28. K.R. Apt, "Ten Years of Hoare's Logic: A Survey—Part I," ACM Trans. Programming Languages and Systems, vol. 3, no. 4, 1981, pp. 431-483. 29. C.A.R. Hoare, "Procedures and Parameters: An Axiomatic Approach," Symposium on Semantics of Algorithmic Languages, LNM 188, E. Engeler, ed., Springer-Verlag, 1971, pp. 102-116. 30. M. Clint and C.A.R. Hoare, "Program Proving: Jumps and Functions," Acta Informatica, vol. 1, 1972, pp. 214-224. 31. E.A. Ashcroft, M. Clint, and C.A.R. Hoare, remarks on, "Program Proving: Jumps and Functions," Acta Informatica, vol. 6, no. 3, 1976, pp. 317-318. 32. W.-P. de Roever, "Recursion and Parameter Mechanisms: An Axiomatic Approach", Automata Languages and Programming, LNCS 14, J. Loeckx, ed., Springer-Verlag, 1974, andCall-by-Value versus Call-by-Name: A Proof Theoretic Comparison,tech. report IW 23/76, Mathematical Center, Amsterdam, Sept. 1976. 33. C.A.R. Hoare and N. Wirth, "An Axiomatic Definition of the Programming Language Pascal," Acta Informatica, vol. 2, no. 4, 1973, pp. 335-355. 34. It has often been argued that this goal was overambitious. In Hoare's presentation at the April 1969 meeting of IFIP Working Group WG 2.2 in Vienna, he responded to the challenge—that it had taken millennia of arithmetic before Peano's axioms were formalized—that he had not been on that task! 35. R.L. London et al., "Proof Rules for the Programming Language Euclid," Acta Informatica, vol. 10, no. 1, 1978, pp. 1-26. 36. D.I. Good et al., Report on the Language, version 2.0, tech. report ICSCA-CMP-10, Univ. of Texas at Austin, Sept. 1978. 37. E.W. Dijkstra, Goto Statement Considered Harmful Comm. ACM, vol. 11, no. 3, pp. 147-148, Mar. 1968. 38. O.-J. Dahl, E.W. Dijkstra, and C.A.R. Hoare eds. Structured Programming, Academic Press, 1972. 39. E.W. Dijkstra, "A Constructive Approach to the Problem of Program Correctness," BIT, vol. 8, no. 3, 1968, pp. 174-186. Also, E.W. Dijkstra,A Short Introduction to the Art of Programming,Technisch Hogeschool Eindhoven (Eindhoven University of Technology), EWD-316, 1971. 40. N. Wirth, Systematic Programming: An Introduction, Prentice Hall, 1973. Also, N. Wirth,Algorithms + Data Structures = Programs,Prentice Hall, 1976. 41. , A detailed technical assessment that focuses on the questions of consistency and completeness is given in Ref. 28 and in K.R. Apt, "Ten Years of Hoare's Logic: A Survey—Part II: Nondeterminism," Theoretical Computer Science, vol. 28, 1984, pp. 83-109. Another important study is J. de Bakker,Mathematical Theory of Program Correctness,Prentice Hall, 1980. 42. E.W. Dijkstra, A Discipline of Programming.Englewood Cliffs, N.J.: Prentice Hall, 1976. 43. D. Gries, The Science of Programming.New York, Heidelberg, Berlin: Springer-Verlag, 1981. 44. R.C. Backhouse, Program Construction and Verification, Prentice Hall, 1986. 45. Z. Manna, Termination of Algorithms, doctoral dissertation, Dept. of Computer Science, Carnegie Mellon Univ., Apr. 1968. 46. C.B. Jones, Formal Development of Programs, tech. report 12.117, IBM Laboratory, Apr. 1973. 47. C.B. Jones, Software Development, A Rigorous Approach, Prentice Hall, 1980. 48. Aczel (private communication) writes of the specifications: "It is familiar that this specification does not explicitly express all that we have in mind…a more flexible and powerful approach has been advocated by Cliff Jones in his bookSoftware Development: A Rigorous Approach…His rules appear elaborate and unmemorable compared with the original rules for partial correctness of Hoare." 49. C.B. Jones, Systematic Software Development Using VDM.Englewood Cliffs, N.J.: Prentice Hall, 1986. 50. E.C.R. Hehner, The Logic of Programming, Prentice Hall, 1984. 51. J. Coenen, W.-P. de Roever, and J. Zwiers, "Assertional Data Reification Proofs: Survey and Perspective," 4th Refinement Workshop, J.M. Morris and R. Shaw, eds., Springer-Verlag, 1991, pp. 97-114. 52. A. Tarlecki, "A Language of Specified Programs," Science of Computer Programming, vol. 5, no. 1, 1985, pp. 59-81. 53. This led to some embarrassment for me when, at a seminar in Newcastle-upon-Tyne in 1982, Hoare gave a talk that accepted postconditions of two states but used thex,x′convention; I might have been pleased had I not been waiting to give my own talk with the first set of slides using the hook notation. 54. H. Barringer, J.H. Cheng, and C.B. Jones, "A Logic Covering Undefinedness in Program Proofs," Acta Informatica, vol. 21, no. 3, 1984, pp. 251-269. 55. Normally known as David Park. To avoid confusion, all references show only one initial. D. Park, "Fixpoint Induction and Proofs of Program Properties," Machine Intelligence 5, B. Meltzer and D. Michie, eds., Edinburgh Univ. Press, 1969, pp. 59-78. 56. R.M. Burstall, "Proving Properties of Programs by Structural Induction," Computer J., vol. 12, no. 1, 1969, pp. 41-48. 57. C.A.R. Hoare, Comm. ACM, vol. 4, no. 7, July 1961, pp. 321-322. 58. C. A. R. Hoare, "Proof of a Program: FIND," Comm. ACM, vol. 14, p. 39, Jan. 1971. 59. Further applications are in M. Foley and C.A.R. Hoare, "Proof of a Recursive Program: Quicksort," Computer J., vol. 14, no. 4, Nov. 1971, pp. 391-395, and in C.A.R. Hoare, "Proof of a Structured Program: 'The Sieve of Eratosthenes'," Computer J., vol. 15, no. 4, Nov. 1972, pp. 321-325. 60. E.W. Dijkstra, "Guarded Commands, Nondeterminacy, and Formal Derivation of Programs," Comm. ACM, vol. 18, no. 8, pp. 453-457, Aug 1975. 61. Not only did the Blanchland (Oct. 1973) meeting of IFIP W.G. 2.3 have a part to play in the development (see Mike Woodger"s nice history inProgramming Methodology: A Collection of Articles by Members of IFIP W.G. 2.3,D. Gries, ed., Springer-Verlag, 1978, pp. 1-5), but the firm rejection of arguments presented in an unnecessarily operational way has remained a hallmark of these gatherings. 62. E. Dijkstra and C. Scholten, Predicate Calculus and Program Semantics. Springer-Verlag, 1989. 63. C. Morgan, Programming from Specifications, Prentice Hall, 1990. 64. P. Lucas, Two Constructive Realizations of the Block Concept and their Equivalence, tech. report TR 25.085, IBM Laboratory, June 1968. 65. C.B. Jones, A Technique for Showing that Two Functions Preserve a Relation between their Domains, tech. report LR 25.3.067, IBM Laboratory, Apr. 1970. 66. For example, see R. Milner, The Difficulty of Verifying a Program with Unnatural Data Representation, tech. report 3, Computation Services Dept., Univ. College of Swansea, Jan. 1969; A Formal Notion of Simulation between Programs,tech. report 14, Dept. of Computer Science, Univ. College of Swansea, Oct. 1970; andProgram Simulation: An Extended Formal Notion,tech. report 17, Dept. of Computer Science, Univ. College of Swansea, Apr. 1971. 67. R. Milner, An Algebraic Definition of Simulation between Programs, tech. report CS-205, Computer Science Dept., Stanford Univ., Feb. 1971. 68. C.A.R. Hoare, "Proof of Correctness of Data Representations," Acta Informatica, vol. 1, no. 4, 1972, pp. 271-281. 69. Robin Milner also pointed out (private communication, Feb. 1992) that his submission to theJ. ACMon this topic was thought by the referees to be too obvious to warrant publication. Milner rightly comments that "things don't have to be difficult to be useful!" 70. C. Strachey, "Systems Analysis and Programming," Scientific Am., vol. 215, no. 3, Sept. 1966, pp. 112-124. 71. C.B. Jones, Software Development, A Rigorous Approach, Prentice Hall, 1980. 72. C.B. Jones, "Implementation Bias in Constructive Specification of Abstract Objects," unpublished manuscript, Sept. 1977. 73. T. Nipkow, "Non-deterministic Data Types: Models and Implementations," Acta Informatica, vol. 22, no. 6, 1986, pp. 629-661. 74. J. He, C.A.R. Hoare, and J.W. Sanders, “Data Refinement Refined,” Proc. ESOP'86 European Symp. Programming, G. Goos and H. Hartmants, eds., pp. 187–196, Mar. 1986. 75. J.V. Guttag, The Specification and Application to Programming of Abstract Data Types, CSRG-59, doctoral dissertation, Univ. of Toronto, Computer Systems Research Group, Sept. 1975. 76. S.N. Zilles, Abstract Specifications for Data Types, tech. report 11, MIT progress report, 1974. 77. J.A. Goguen et al., Initial Algebra Semantics, tech. report RC 5243, IBM, 30 Jan. 1975. 78. F.L. Morris, "Advice on Stucturing Compilers and Proving them Correct," ACM Symp. Principles of Programming Languages, ACM Press, 1973, pp. 144-152, and J.H. Morris, "Types are not Sets,"ACM Symp. Principles of Programming Languages,ACM Press, 1973, pp. 120-124. 79. For a useful historical sketch, see J.A. Goguen et al., "Initial Algebra Semantics and Continuous Algebras," J. ACM, vol. 24, no. 1, 1977, pp. 68-95. 80. P. Lucas, "On the Semantics of Programming Languages and Software Devices," R. Rustin, Formal Semantics of Programming Languages, Prentice Hall, 1972, pp. 41-57. 81. H. Beki$\breve c$ and K. Walk, "Formalization of Storage Properties," Symp. Semantics of Algorithmic Languages, LNM 188, E. Engeler, ed., Springer-Verlag, 1971, pp. 28-61. 82. C.B. Jones, "Formal Development of Correct Algorithms: An Example Based on Earley's Recogniser", ACM SIGPLAN Notices, vol. 7, no. 1, Jan. 1972, pp. 150-169. 83. Text books in this area include H. Ehrig and B. Mahr, Fundamentals of Algebraic Specification 1: Equations and Initial Semantics, European Assoc. for Theoretical Computer Science (EATCS) Monographs on Theoretical Computer Science, Springer-Verlag, 1985, and H. Ehrig and B. Mahr,Fundamentals of Algebraic Specification 2: Module Specifications and Constraints,EATCS Monographs on Theoretical Computer Science, Springer-Verlag, 1990. 84. D. Bjørner and C.B. Jones eds. The Vienna Development Method: The Meta-Language, LNCS 61, Springer-Verlag, 1978. 85. More recent publications are D. Bjø, rner and C.B. Jones, Formal Specification and Software Development, Prentice Hall, 1982; C.B. Jones,Systematic Software Development Using VDM,Prentice Hall, 1986; and C.B. Jones, "VDM Proof Obligations and their Justification,"VDM'87—A Formal Definition at Work,LNCS 252, D. Bjørner et al., eds, Springer-Verlag, 1987, pp. 260-286. 86. J.-R. Abrial and S.A. Schuman, "Non-deterministic System Specification," Semantics of Concurrent Computation: Proceedings, LNCS 70, G. Kahn, ed., Springer-Verlag, 1979, pp. 34-50; also J.-R. Abrial, S.A. Schuman, and B. Meyer, "Specification language,"On the Construction of Programs,R.M. McKeag and A.M. Macnaghten, eds., Cambridge Univ. Press, 1980, pp. 343-410. 87. A reference that has not been located is Abrial's paper that was presented at the conference whose proceedings are published as Mathematical Studies of Information Processing, LNC75, E.K. Blum, M. Paul, and S. Takasu, eds., Springer-Verlag, 1979.