Virtual Musuem of Computing

Program Verification and Semantics
Early manuscripts by C.A.R. Hoare

Below are three early manuscripts by Tony Hoare relating to his research in the area of assertions. See also a draft paper entitled Assertions: a personal perspective by Tony Hoare.

Note: larger versions are linked form the images below.

Title page including the summary from pencilled draft of [1]

[Photograph of title page]

Formal proof from pencilled draft of [1]

[Photograph of proof]

Copy of letter to Niklaus Wirth dated 28 September 1971 accompanying an early draft of [2]

[Photograph of letter]

References

[1]
C.A.R. Hoare, An axiomatic basis for computer programming. Communications of the ACM, Vol. 12 No. 10, pages 576-580,583 (1969).

[2]
C.A.R. Hoare and N. Wirth, An axiomatic definition of the programming language PASCAL. Acta Informatica, Vol. 2 No. 4, pages 335-355 (1973).

Installed by Jonathan Bowen with the kind permission of Tony Hoare.
Part of the Virtual Museum of Computing