This Article 
 Bibliographic References 
 Add to: 
Assertions: A Personal Perspective
April-June 2003 (vol. 25 no. 2)
pp. 14-25
C.A.R. Hoare, Microsoft Research

Assertions are Boolean formulas placed in program text at places where their evaluation will always be true. If the assertions are strong enough, they express everything that the programmers on either side of an interface need to know about the program on the other side, even before the code is written. Indeed, assertions can serve as the basis of a formal proof of the correctness of a complete program.

1. Elliott Brothers, Elliott 803 Programming Manual, London Ltd., 1960.
2. D. Shell, "A High-Speed Sorting Procedure," Comm. ACM, vol. 2, no. 7, July 1959, pp. 30-32.
3. P. Naur ed. "Report on the Algorithmic Language Algol 60," Comm. ACM, vol. 3, no. 5, May 1960, pp. 299-314.
4. N. Chomsky, Syntactic Structures, Mouton&Co., 1957.
5. J.W. Backus,, "The Syntax and the Semantics of the Proposed International Algebraic Language of the Zurich ACM-GAMM [Assoc. for Computing Machinery-German association for Applied Mathematics and Mechanics] Conference," Proc. Int'l Congress for Information Processing, 1959, pp. 125-132.
6. C.A.R. Hoare, "Report on the Elliott Algol Translator," Computer J., vol. 5, no. 4, Jan. 1963, pp. 345-348.
7. T.B. SteelJr. ed. Formal Language Description Languages for Computer Programming,North Holland, 1966.
8. J.V. Garwick, "The Definition of Programming Languages by their Compilers," Formal Language Description Languages for Computer Programming,North Holland, 1966.
9. W.V.O. Quine, Mathematical Logic, revised ed., Harvard Univ. Press, 1955.
10. S. Igarashi, An Axiomatic Approach to Equivalence Problems of Algorithms with Applications, doctoral dissertation, Tokyo Univ., 1964.
11. P. Lucas et al., Informal Introduction to the Abstract Syntax and Interpretation of PL/I, ULD version II, IBM TR 25.03, IBM, 1968.
12. R.W. Floyd, "Assigning Meanings to Programs," Proc. Am. Soc. Symp. Applied Mathematics, vol. 19, 1967, pp. 19-31.
13. C.A.R. Hoare, "An Axiomatic Basis for Computer Programming," Comm. ACM, 1969.
14. C.A.R. Hoare, "Procedures and Parameters: An Axiomatic Approach," Symp. Semantics of Algorithmic Languages, LNM 188, E. Engeler, ed., Springer-Verlag, 1971, pp. 102-116.
15. C.A.R. Hoare and M. Foley, "Proof of a Recursive Program: Quicksort," Computer J., vol. 14, no. 4, Nov. 1971, pp. 391-395.
16. C.A.R. Hoare, "Towards a Theory of Parallel Programming," Operating Systems Techniques, Academic Press, 1972, pp. 61-71.
17. C.A.R. Hoare and M. Clint, "Program Proving: Jumps and Functions," Acta Informatica, vol. 1, 1972, pp. 214-224.
18. C.A.R. Hoare, "A Note on the For Statement," BIT, vol. 12, no. 3, 1972, pp. 334-341.
19. 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.
20. R.L. London et al., "Proof Rules for the Programming Language EUCLID," Acta Informatica, vol. 10, 1978, pp. 1-26.
21. B. Meyer, Object-Oriented Software Construction, 2nd ed., Prentice Hall, Upper Saddle River, N.J., 1997.
22. E.W. Dijkstra, Goto Statement Considered Harmful Comm. ACM, vol. 11, no. 3, pp. 147-148, Mar. 1968.
23. S.C. Johnson, "Lint: A C Program Checker," UNIX 4.2 Programming Manual, Univ. of California, Berkeley, 1984.
24. W.R. Bush, J.D. Pincus, and D.J. Sielaff, "A Static Analyser for Finding Dynamic Programming Errors," Software Practice and Experience, vol. 30, no. 7, June 2000, pp. 775-802.
25. E.W. Dijkstra, "A Constructive Approach to the Problem of Program Correctness," BIT, vol. 8, 1968, pp. 174-186.
26. E.W. Dijkstra, A Discipline of Programming.Englewood Cliffs, N.J.: Prentice Hall, 1976.
27. C. Morgan, Programming from Specifications, Prentice Hall, 1990.
28. O-J. Dahl et al., SIMULA 67 Common Base Language, Norwegian Computer Center, 1967.
29. O-J. Dahl and C.A.R. Hoare, "Hierarchical Program Structures," Structured Programming, Academic Press, 1972, pp. 175-220.
30. C.A.R. Hoare, "A Structured Paging System," Computer J., vol. 16, no. 3, Aug. 1973, pp. 209-215, 1973.
31. C.A.R. Hoare, "Proof of Correctness of Data Representations," Acta Informatica, vol. 1, no. 4, 1972, pp. 271-281.
32. E.W. Dijkstra, "Cooperating Sequential Processes," Programming Languages, F. Genuys, ed., Academic Press, 1968.
33. P. Brinch Hansen, "Structured Multiprogramming," Comm. ACM, vol. 15, no. 7, July 1972, pp. 574-578.
34. C.A.R. Hoare, "Monitors, An Operating System Structuring Concept," Comm. ACM, vol. 17, no. 10, Oct. 1974, pp. 549-557.
35. P. Brinch Hansen, "The Programming Language Concurrent Pascal," IEEE Trans. Soft. Eng., vol. 1, no. 2, June 1975, pp. 199-207.
36. J. Gosling, B. Joy, and G. Steele, The Java Language Specification, Addison-Wesley, Reading, Mass., 1996.
37. C.A.R. Hoare, "The Structure of an Operating System," Language Hierarchies and Interfaces, LNCS 46, F.L. Bauer and K. Samelson, eds., Springer, 1976, pp. 242-265.
38. J. Welsh and D. Bustard, Concurrent Program Structures, Prentice Hall, 1988.
39. E.W. Dijkstra, "Guarded Commands, Nondeterminacy, and Formal Derivation of Programs," Comm. ACM, vol. 18, no. 8, pp. 453-457, Aug 1975.
40. C.A.R. Hoare,“Communicating sequential processes,” Comm. of the ACM, vol. 21, no. 8, pp. 666-677, Aug. 1978.
41. J. Stoy, Denotational Semantics, the Scott-Strachey Approach to Programming Language Theory, MIT Press, 1977.
42. S. Brookes and A.W. Roscoe, "An Improved Failures Model for CSP," Proc. Pittsburgh Seminar on Concurrency, LNCS 197, S.D. Brookes, A.W. Roscoe, and G. Winskel., eds., Springer, 1985.
43. C.A.R. Hoare, Communicating Sequential Processes, Prentice Hall, Englewood Cliffs, N.J., 1985.
44. Inmos, Transputer Reference Manual, Prentice Hall, 1988.
45. C.A.R. Hoare, "The Transputer and occam: A Personal Story," Concurrency: Practice and Experience, vol. 3, no. 4, 1991, pp. 249-264.
46. G. Jones and M. Goldsmith, Programming in occam 2, Prentice Hall, 1988.
47. R. Milner, Communicating and Mobile Systems: The p calculus, Cambridge Univ. Press, Cambridge, UK, 1999.
48. J.-R. Abrial, "Assigning Programs to Meanings," Mathematical Logic and Programming Languages, Philosophical Trans. Royal Society, series A, vol. 312, 1984.
49. B.P. Collins, J.E. Nicholls, and I.H. Sorensen, Introducing Formal Methods, The CICS Experience with Z, IBM TR 12.260, IBM, 1989.
50. C.B. Jones, Software Development, A Rigorous Approach, Prentice Hall, 1980.
51. E.C.R. Hehner, "Predicative Programming," Comm. ACM, vol. 27, no. 2, Feb. 1984, pp. 134-151.
52. C.A.R. Hoare, and E.C.R. Hehner,"A More Complete Model of Communicating Processes, Theoretical Computer Science, vol. 26, no. 1-2, Sept. 1983, pp. 105-120.
53. C.A.R. Hoare, and A.W. Roscoe,"Programs as Executable Predicates," Proc. Int'l Conf. Fifth Generation Computer Systems, Tokyo, Inst. for New Generation Computer Technology, 1984, pp. 220-228.
54. C.A.R. Hoare, "Programs are Predicates," Mathematical Logic and Programming Languages, Philosophical Trans. Royal Society, series A, vol. 312, 1984, pp. 475-489.
55. C.A.R. Hoare, "Programs are Predicates," New Gen. Comp., vol. 38, 1993, pp. 2-15.
56. C.A.R. Hoare and H. Jifeng, Unifying Theories of Programming, Prentice Hall, 1998.
57. C.A.R. Hoare and P.E. Lauer, "Consistent and Complementary Formal Theories of the Semantics of Programming Languages, Acta Informatica, vol. 3, no. 2, 1974, pp. 135-153.

C.A.R. Hoare, "Assertions: A Personal Perspective," IEEE Annals of the History of Computing, vol. 25, no. 2, pp. 14-25, April-June 2003, doi:10.1109/MAHC.2003.1203056
Usage of this product signifies your acceptance of the Terms of Use.