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: blampson@microsoft.com. This paper is at http://www.research.microsoft.com.
Abstract:
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.