A Proof Rule for Euclid Procedures.
John V. Guttag, James J. Horning, Ralph L. London · Defense Technical Information Center (DTIC) · 1977
The proof rules of Euclid, like the axiomatization of Pascal, presents a single definition of the various features of the language being defined. Little effort is made to explain the proof rules or to compare them to alternatives. In this paper we take one of our more complex proof rules, the rule for procedure definition and call, and attempt both to explain its workings and to compare it to two alternative rules. The rules we have chosen for comparison are Hoare's adaptation rule, from which our rule is derived, and the Pascal procedure-call rule. (Author)