Proof rules for the programming language Euclid

Ralph London, Butler Lampson, Jim Horning, Jim Mitchell, and Gerry Popek


Citation: Acta Informatica 10, 1 (Jan. 1978), pp 1-26.

Links: Abstract, Acrobat. Here is an HTML version created by OCR for the benefit of search engines; it is not meant for human consumption.

Email: This paper is at



In the spirit of the previous axiomatization of the programming language Pascal, this paper describes Hoare-style proof rules for Euclid, a programming language intended for the expression of system programs which are to be verified. All constructs of Euclid are covered except for storage allocation and machine dependencies.