This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
The Early Search for Tractable Ways of Reasoning about Programs
April-June 2003 (vol. 25 no. 2)
pp. 26-49
Cliff B. Jones, University of Newcastle-upon-Tyne

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.

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.
87. A reference that has not been located is Abrial's paper that was presented at the conference whose proceedings are published asMathematical Studies of Information Processing,LNC75, E.K. Blum, M. Paul, and S. Takasu, eds., Springer-Verlag, 1979.
88. J. M. Spivey,The Z Notation: A Reference Manual. Englewood Cliffs, NJ: Prentice-Hall, 1989.
89. D.I. Good and W.D. Young, "Mathematical Methods for Digital Systems Development," VDM'91—Formal Software Development Methods, Vol. 2: Tutorials, LNCS 552, S. Prehn and W.J. Toetenel, eds., Springer-Verlag, 1991, pp. 406-430.
90. R.M. Burstall and J.A. Goguen, "An Informal Introduction to Specifications Using CLEAR," The Correctness Problem in Computer Science, Int'l Lecture Series in Computer Science, R.S. Boyer and J.S. Moore, eds., Academic Press, 1981, pp. 185-214.
91. Richard A. DeMillo, Richard J. Lipton, and Alan J. Perlis, "Social Processes and Proofs of Theorems and Programs," Comm. ACM, vol. 22, p. 271, May 1979.
92. O-J. Dahl, "Can Program Proving Be Made Practical?" EEC-Crest Course on Programming Foundations, M. Amirchahy and D. Néel, eds., IRIA, 1978, pp. 57-114. Also printed as tech. report 33, Inst. of Informatics, Univ. of Oslo. See also C.B. Jones, "Constructing a Theory of a Data Structure as an Aid to Program Development,"Acta Informatica,vol. 11, no. 2, 1979, pp. 119-137, and more recently, J.V. Guttag, J.J. Horning, and J.M. Wing,Larch in Five Easy Pieces,tech. report 5, Digital Equipment Corp. Science Research Center, July 1985, and B. Mueller, "Formal Derivation of Pointer Algorithms,"Informatik und Mathematik,M. Broy, ed., Springer-Verlag, 1991, pp. 419-440.
93. James H. Fetzer, "Program Verification: The Very Idea," Comm. ACM, vol. 31, p. 1,057, Sept. 1988.
94. E.W. Dijkstra, "Cooperating Sequential Processes," Programming Languages, F. Genuys, ed., Academic Press, 1968, pp. 43-112.
95. C.A.R. Hoare, "Towards a Theory of Parallel Programming," Operating System Techniques, C.A.R. Hoare and R. Perrot, eds., Academic Press, 1972, pp. 61-71.
96. C.A.R. Hoare, "Monitors, An Operating System Structuring Concept," Comm. ACM, vol. 17, no. 10, Oct. 1974, pp. 549-557.
97. C.A.R. Hoare, "Communicating Sequential Processes," Comm. ACM, vol. 21, no. 8, Aug. 1978, pp. 666-677. For a more recent description of CSP, see C.A.R. Hoare,Communicating Sequential Processes,Prentice Hall, 1985.
98. P. Brinch Hansen, "Distributed Processes: A Concurrent Programming Concept," Comm. ACM, vol. 21, no. 11, Nov. 1978, pp. 934-941.
99. R. Milner, Communication and Concurrency, Prentice-Hall, Englewood Cliffs, N.J., 1989.
100. D. Park, "Concurrency and Automata on Infinite Sequences," Theoretical Computer Science, 5th GI-Conference, LNCS 104, Springer-Verlag, 1981, pp. 167-183.
101. E.A. Ashcroft and Z. Manna, "Formalization of Properties of Parallel Programs," Machine Intelligence 6, B. Meltzer and D. Michie, eds., Edinburgh Univ. Press, 1971, pp. 17-41.
102. S.S. Owicki, Axiomatic Proof Techniques for Parallel Programs, doctoral dissertation, Dept. of Computer Science, Cornell Univ., 1975. Published as tech. report 75-251.
103. S.S. Owicki and D. Gries, "An Axiomatic Proof Technique for Parallel Programs," Acta Informatica, vol. 6, no. 4, 1976, pp. 319-340. A related method is described in L. Lamport, "Proving the Correctness of Multiprocess Programs,"IEEE Trans. Software Eng., vol. 3, no. 2, Mar. 1977, pp. 125-143.
104. N. Francez and A. Pnueli, "A Proof Method for Cyclic Programs," Acta Informatica, vol. 9, no. 2, 1978, pp. 133-157.
105. C.B. Jones, Development Methods for Computer Programs including a Notion of Interference, doctoral dissertation, Oxford Univ., June 1981. Printed as Technical Monograph No. PRG-25. These ideas are in C.B. Jones, "Specification and Design of (Parallel) Programs," Information Processing 83,R.E.A. Mason, ed., North-Holland, 1983, pp. 321-332, and in K. Stølen,Development of Parallel Programs on Shared Data-Structures,doctoral dissertation, Dept. of Computer Science, Manchester Univ., 1990 (also published as tech. report UMCS-91-1-1).
106. J. Misra and K.M. Chandy, "Proofs of Networks of Processes," IEEE Trans. Software Eng., vol. 7, no. 4, July 1981, pp. 417-426.
107. W.-P. de Roever, "The Quest for Compositionality: A Survey of Assertion-Based Proof Systems for Concurrent Programs: Part I: Concurrency Based on Shared Variables," E.J. Neuhold and G. Chroust, Formal Models in Programming, Proc. Working Conf. The Role of Abstract Models in Information Processing,North-Holland, 1985, pp. 181-205.
108. See also J. Hooman and W.-P. de Roever, "The Quest Goes On: A Survey of Proof Systems for Partial Correctness of CSP," Current Trends in Concurrency, LNC224, J"S. de Bakker, W.-P. de Roever, and G. Rozenberg, eds., Springer-Verlag, 1986, and J. Zwiers, Compositionality, Concurrency and Partial Correctness: Proof Theories for Networks of Processes, and their Relationship, doctoral dissertation, Technical Univ. Eindhoven, 1988. Available as LNCS 321, Springer-Verlag.
108. See also J. Hooman and W.-P. de Roever, "The Quest Goes On: A Survey of Proof Systems for Partial Correctness of CSP,"Current Trends in Concurrency,LNC224, J"S. de Bakker, W.-P. de Roever, and G. Rozenberg, eds., Springer-Verlag, 1986, and J. Zwiers,Compositionality, Concurrency and Partial Correctness: Proof Theories for Networks of Processes, and their Relationship,doctoral dissertation, Technical Univ. Eindhoven, 1988. Available as LNCS 321, Springer-Verlag.
109. A. Pnueli, "The Temporal Semantics of Concurrent Programs," Theoretical Computer Science, vol. 13, 1981, pp. 45-60.
110. H. Barringer, R. Kuiper, and A. Pnueli, "Now You Can Compose Temporal Logic Specifications," Proc. 16th ACM STOC, pp. 51-63, ACM Press, 1984.
111. L. Lamport, A Temporal Logic of Actions, tech. report 57, DEC, SRC, 1990. See also "The 'Hoare Logic' of Concurrent Programs," Acta Informatica, vol. 14, no. 1, 1980, pp. 21-37, and "Control Predicates are Better than Dummy Variables for Reasoning About Program Control,"ACM Trans. Programming Languages and Systems,vol. 10, no. 2, Apr. 1988, pp. 267-281.
112. H.C. Lauer, Correctness in Operating Systems, doctoral dissertation, Dept. of Computer Science, Carnegie Mellon Univ., 1972.
113. K.M. Chandy and J. Misra, Parallel Program Design—A Foundation. Addison-Wesley, 1988.
114. C.A. Petri, Kommunikation mit Automaten, [Communication with Automation] doctoral dissertation, Univ. of Darmstadt, 1962; alsoNichtsequentielle prozesse,tech. report ISF-76-6, GMD, 1976, and its translation,Non-sequential processes,tech. report ISF-77-05, GMD, 1977. A useful overview is contained in G. Rozenberg,Advances in Petri-nets,LNCS 188, Springer-Verlag, 1985.
115. H. Zemanek, "Semiotics and Programming Languages," Comm. ACM, vol. 9, no. 3, Mar. 1966, pp. 139-143.
116. P. Naur, “Revised Report on the Algorithmic Language ALGOL 60,” Comm. ACM, vol. 6, no. 1, pp. 1-17, 1963.
117. For an early view, see S. Gorn, "Specification Languages for Mechanical Languages and their Processors—A Baker's Dozen," Comm. ACM, vol. 4, no. 12, Dec. 1961, pp. 532-542.
118. J. McCarthy, "A Formal Description of a Subset of ALGOL," Formal Language Description Languages for Computer Programming, T.B. Steel, ed., North-Holland, 1966, pp. 1-12.
119. For background on the IBM Laboratory in Vienna, see P. Lucas, "Formal Semantics of Programming Languages: VDL," IBM J. Research and Development, vol. 25, no. 5, Sept. 1981, pp. 549-561.
120. Which might have been called "NPL" had the UK National Physical Laboratory not pointed out that they had a prior claim on the acronym; see History of Programming Languages, R.L. Wexelblat, ed., Academic Press, 1981, pp. 551-600.
121. Secondary material includes P. Lucas and K. Walk, On The Formal Description of PL/I, vol. 6, Part 3 of Annual Review in Automatic Programming, Pergamon Press, 1969.
122. J. McCarthy and J. Painter, Correctness of a Compiler for Arithmetic Expressions, tech. report CS38, Computer Science Dept., Stanford Univ., Apr. 1966. See alsoProc. Symp. in Applied Mathematics, Vol.19: Mathematical Aspects of Computer Science,American Mathematical Soc., 1967, pp. 33-41.
123. P.J. Landin, "The Mechanical Evaluation of Expressions," Computer J., vol. 6, no. 4, 1964, pp. 308-320, and "A Correspondence between ALGOL-60 and Church's Lambda-Notation,"Comm. ACM,vol. 8, no. 2, Feb. 1965, pp. 89-101, 158-165.
124. D. Scott, "A Construction of a Model for thelCalculus," manuscript, Nov. 1969; "Models for thelCalculus," manuscript—draft, Dec. 1969; "A Simplified Construction forlCalculus Models," manuscript, Apr. 1973;Outline of a Mathematical Theory of Computation,tech. report PRG-2, Oxford Univ. Computing Laboratory, Programming Research Group, Nov. 1970; andData Types as Lattices,tech. report PRG-5, Oxford Univ. Programming Research Group, Sept. 1976.
125. C. Strachey and D. Scott, "Mathematical Semantics for Two Simple Languages," paper read at Princeton Univ., Aug. 1970.
126. J. Stoy, Denotational Semantics, the Scott-Strachey Approach to Programming Language Theory, MIT Press, 1977.
127. H. Beki$ \breve c $ et al., A Formal Definition of a PL/I Subset, tech. report 25.139, IBM Laboratory, Dec. 1974.
128. H. Beki$ \breve c $, Programming Languages and Their Definition, LNCS 177, Springer-Verlag, 1984.
129. P. Naur, "Formalization in Program Development," BIT, vol. 22, no. 4, 1982, pp. 437-453.
130. G.D. Plotkin, A Structural Approach to Operational Semantics, tech. report DAIMI FN-19, Aarhus Univ., 1981.
131. For example, S. Igarashi, An Axiomatic Approach to the Equivalence Problems of Algorithms with Applications, doctoral dissertation, Univ. of Tokyo, 1964.
132. C.A.R. Hoare et al., “Laws of Programming,” Comm. the ACM, vol. 30, no. 8, pp. 672–686, 1987.
133. John W. Backus, "Can Programming be Liberated From the von Neumann Style? A Functional Style and Its Algebra of Programs," Communications of the ACM, vol. 21, pp. 613-641, 1978.
134. R. Kowalski, "Algorithm = Logic + Control," Comm. ACM, vol. 22, July 1979.
135. For a recent survey, see J.A. Robinson, "Logic and Logic Programming," Comm. ACM, vol. 35, no. 3, Mar. 1992, pp. 40-65.
136. G. Kahn and D. MacQueen, "Coroutines and Networks of Parallel Processes," Information Processing 77, B. Gilchrist, ed., 1977, pp. 993-998.
137. D.B. MacQueen, Models for Distributed Computing, tech. report 351, INRIA, Apr. 1979.
138. Inmos, occam 2: Reference Manual, Prentice Hall, 1988.
139. O.-J. Dahl, B. Myhrhaug, and K. Nygaard, SIMULA 67 Common Base Language, tech. report S-2, Norwegian Computing Center, 1968.
140. A. Goldberg and D. Robson, Smalltalk 80: The Language and Its Implementation.Reading, Mass.: Addison Wesley, 1983.
141. B. Meyer,Object-Oriented Software Construction. Englewood Cliffs, NJ: Prentice-Hall, 1988.
142. P. America, "Issues in the Design of a Parallel Object-Oriented Language," Formal Aspects of Computing, vol. 1, no. 4, 1989, pp. 366-411.

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
Usage of this product signifies your acceptance of the Terms of Use.