This document was made by
OCR from a scan of the technical report. It has not been edited or proofread
and is not meant for human consumption, but only for search engines. To see the
scanned original, replace OCR.htm with Abstract.htm or Abstract.html in the URL
that got you here.
Acta
Informatica 10, 1— 26 (1978)
Proof
Rules for the Programming Language Euclid
R.L. London^{l}*,
J.V. Guttag *^{lc},^{ }J.J. Horning ^{3 }***, B.W.
Lampson J.G. Mitchell', and G.J.
Popek^{5}****
USC Information
Sciences Institute. 4676 Admiralty Way, Marina del Rey, CA 90291, USA = Computer Science Dept.,
University of Southern California, Los An^{g}eles, CA 90007, USA Computer Systems Research Group,
University of Toronto, Toronto, M5S 1A4, Canada Xerox Research Center, 3333 Coyote Hill Road, Palo
Alto, CA 94304, USA
^{5 }3532 Boelter Hall, Computer Science
Dept., University of California, Los Angeles, CA 90024, USA
Summary. In the spirit of the previous
axiomatization of the programming lan^{g}uage Pascal, this paper describes Hoarestyle 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 stora^{g}e
allocation and machine dependencies.
The symbolic form
of the work has been forced upon us by necessity: without its help we should hare been unable to perform the requisite reasoning.
A.N. Whitehead and B. Russell. Pri ne ipi a 1hithematica.
p. vii
Rules
are rules." Anonymous
Introduction
The programming langua^{g}e Euclid has been desi^{g}ned to facilitate the construction of verifiable system pro^{g}rams. Its defining report [11] closely follows the
defining report [15] of the Pascal
lan^{g}ua^{g}e (see
also [10]). The present document, giving Hoarestyle proof rules applicable only to legal Euclid programs, owes a
great deal to (and is in part
identical to) the axiomatic definition of Pascal [9]. Major differences from [9] include the treatment of
procedures and functions, declarations.
modules, collections. escape statements, binding, parameterized types, and the examples and detailed explanations in
Appendices 13. Other semantic defini‑
* To whom offprint requests should
be sent. Supported by the Defense Advanced Research Projects Agency under contract
DAHC1572C0308
** Supported in part by
the National Science Foundation under grant MCS7686089 and the Joint Services Electronics Program
monitored by the Air Force Office of Scientific Research under contract F 4462076C0061
*** Supported in part by a Research Leave Grant
from the University of Toronto and a ^{g}rant from the National Research Council of
Canada. Current address: Xerox Research Center **** Supported in part by the
Defense Advanced Research Projects Agency under contract DAHC^{7}3C0368.
The views expressed are those of the authors
don methods are certainly applicable to Euclid. We have
used proof rules for two reasons: familiarity and the existence of the Pascal
definition. Readers unfamiliar with proof rules may to read [6, 7].
One may regard the proof rules as a definition of Euclid
in the same sense as the Pascal axiomatization defines Pascal. By stating
what can be proved about Euclid programs, the rules define the meaning of most
syntactically and semantically legal Euclid programs, but they do not give the
information required to determine whether or not a program is legal. This
information may be found in the language report. Neither do the proof rules define
the meaning of illegal Euclid programs containing, for example, division by zero
or an invalid array index. Finally, explicit proof rules arc not provided for
those portions of Euclid defined in the report by translation into other legal
Euclid constructs. This includes pervasive, implicit imports through thus, and some uses of return and exit. All such
transformations must be applied before the proof rules are
applicable.
As is the case with Pascal, the Euclid axiomatization
should be read in conjunction with the language report, and is an almost
total axiomatization of a realistic and useful system programmin^{g} language. While the primary goal of the Euclid
effort was to design a practical programming language (not to provide a vehicle
for demonstrating proof rules), proof rule considerations did have significant
influence on Euclid [13]. All constructs of the language are covered except for
storage allocation (zones and collections that are not referencedcounted) and
machine dependencies. In a few instances rules arc applicable only to a subset of
Euclid; the restrictions are noted with those rules.
Conventions Notation
In describing these Euclid proof rules we have used as
much as possible of the Pascal axiomatization. We have also deliberately followed
the same order and style of presentation and tried to use the same
terminology.
The notation P(y/x) to
denote substitution is used for the formula which is obtained by systematically
substituting v for all free occurrences of x in the predicate P.
If this
introduces conflict between free variables of y and bound variables of P,
the conflict is
resolved by systematic change of the latter variables. The notation P(_{3}1v) may
he read "P with y for .x."
^{P}(.^{1.}1^{x}1^{,}^{ }4'J•„)
denotes simultaneous
substitution for all occurrences of any x_{;} by the corresponding v_{1}. Thus
occurrences of x_{;} within any y_{i} are not
replaced. The
expressions
x,, x„
must be distinct; otherwise the simultaneous substitution is not defined.
The
meaning of substitution for subscripted and qualified expressions is defined
in Sections 4 and 5.
Euclid expressions in assertions must be legal Euclid
expressions. Assertions may contain, outside of expressions, nonEuclid
notations such as quantifiers or
In Ihe proof rules, S and S_{i}
denote a sequence of zero or more statements. As is done in the Pascal
axiomatization, we refer to values of a type as elements of that type.
Also, the rule of consequence
PQ,O{S}LI,UR P{S} R
may be
used in proofs.
Data
Types
The axioms presented in this and the following sections
display the relationship between a type declaration and the axioms which specify
the properties of values of the type and operations defined over them. The
treatment is not wholly formal, and the reader must be aware that:
1.
Free variables in axioms are assumed to he universally
quantified over the appropriate type.
2.
The expression of the "induction" axiom is
always left informal.
3.
The types of variables used in the axioms have to be
deduced either from the section heading or from the more immediate context.
4. The name of a
type is used as a transfer function constructing a value of the type (such a use of the type identifier is not available in
Euclid).
5. The verifier can
assume that everything will be typechecked by the compiler or that the
compiler will generate the necessary legality assertions.
6. In defining Euclid's types we will not be
presenting proof rules that may he directly applied to Euclid programs. Rather, we
will provide a set of assertions, denoted by about the values of the type
being defined. These assertions are incorporated into proof rules in Section
9 on constant, variable, and type declarations. Rule 9.1, for example, tells us
that in the case of an identifier declaration,
we may use the fact that )(ET,
i.e., x has the attributes associated with values of type T
Parameterized types arc covered in Section 9.5. The rules
for type compatibility in Euclid are defined in the language report.
Scalar Types
type T=(c,,c2,...,c,,)
I.I. c,, c_{2}, c„ are distinct elements of T.
.2. These are the only elements of T.
.3.
= T. slice (ed
for i=
I, n
.4. c_{1}=
T. pred(c_{i} _{.0})_{
}for 1= n — 1
.5.
<
.6. < A (37 < 1^{})^{ }<
.7. (x e„) (x
< T. sitee(x))
.8.
I.). _{A l}c_{
}v
•_{=7.. }_{i}(_{A}s>s)
I.10, ,^{t. —I}^{ }<
1.11. X Y t^{y}
1.12. T .
first e,
1.13. 7'. last =e„
1.14. T. ord(cd=i —
1 for i=1, 11.
The standard scalar type Boolean is
defined as
type Boo/ean
= (False, True).
The Boolean operators not, and, or, and
(implication) are those of the conventional logical calculus
except that some operands may possibly not be evaluated. Specifically,
in terms of conditional expressions,
x and v means if x then
v else false, i.e., x cand y, x or
i' means if x then true
else y, i.e.,
x cor y, X r means if x
then v else
true.
(Note, however, that conditional expressions are not
included in Euclid.)
The standard type integer stands
for the set of the whole numbers. The arithmetic operators +. *,
and div are those of whole number
arithmetic. The modulus operator mod is defined by the
equation2.4. u < r char . ord (u)< char . ard(c).
These axioms have been designed to make possible
interchange of programs between implementations using different character sets.
It should be noted that the function char. ord does not necessarily map the
characters onto consecutive
integers.
Subrange Types
type T=nt..n
Let m, n be elements of scalar type T_{0}._{}
3.1. T. first =in
3.2. 7'. last =
3.3. For all i in T_{0} such that m a, i is
an element of T.
3.4. These are the only elements of 7:
3.5.
T.. first i < T. last P T.
succ(i)= succ(i)
3.6.
7'.
first <i T. last P7'. pred (0 T_{0}.
prcd(i).
Note
that since all elements of T are elements of all operators of T_{o }apply
to
them.
m mod — m —(m div n)_{*}n
whereas
div denotes division
with truncated fraction, i.e., move toward zero. Implementations
are permitted to refuse the execution of programs which refer to
integers outside the appropriate range, signedlat or unsignedlat.
Type Char
2.1. The elements of type char are
the 26 (capital) letters, the 10 (decimal)
digits, and possibly other characters defined by particular
implementations. In programs, a constant of type Char is
denoted by preceding the character
with
a S.
The sets of letters and digits are ordered, and the digits arc coherent, i.e., (x, stands for T(x,„, ...,X_{f}_ _{t},_{ }y, x_{j±i},_{}
2.2. A <S $0^{.}<5b $ 1= char . succ ($ 0)
B <S C $b<Sc $ 2= char . succ (S
1)
•••
)'<5
Z $ y <5 2. 5 9= char . succ($ 8).
Axioms 1.51.13 apply to the char type.
The functions char ore! and Chr arc
defined by the following additional axioms:
13. If u is an clement of char, then
char.
ord(u) is a nonnegative integer (called the
ordinal
number of u), and
Chr(char.
and (u))= u
The formula 1'(y/v(i)),
denoting a substitution for an array reference, is then
defined to be
^{P}((^{x},^{ }^{I: }1^{7})/^{x})^{.}
To
extend this definition to substitution for a multiplysubscripted array
reference, we
define
(x, ...,1„): y), where n 2
12.I et ('roof Rules l'or Inc Programming
Language Euclid 7
o he equal to
in: y))
and the formula
My/x(i,) (i„)), where n 2
is equivalent to
P((^{x}, <i,, y)/x).
4.4. x. I
ndexType = x • Component Type = To.
Record Types
type T = record,
^{S}.^{ };^{ 7}1, • •• • ^{S}ru^{: }end T
where each s, must be preceded by const or var.
Let x, be an element of T_{i} for =
1, ..., m.
5.1. 7^{.}(x,,
x_{2}, ..., x,„) is an element of T 5.2. These are the only elements of T.
5.3. T(x,, x„,) s_{i}= x_{i} for i= 1, , tn.
(x, r) stands for T(x,, ..., y, x_{i+}_{ }x„).
The formula P(y/x s_{1}) is defined analogously to arrays (sec definitions following 4.3).
1^{,}itriant Records
type 7;,(c). record ,
s„,: TM;
case c of
k, s',:
T,' end k,
k_{2}=> 5_{2}'
:7; end k_{2}
k„ s„: T„' end k„
end case
end T
where the type of c is
a scalar or subrange type with elements k k„. Note
that I. k,„ S stands for k„ S; S; ...; S.
Consider type T
=T_{o}(k_{j}), and
let x'_{j} be an element of 77 for j= I, 11.
5.1 a. T(x,, x„„ k_{j},
.9 is an element of T.
5.2a. These are the only elements
of T.
5.3 a. Ttv, „„ k . s_{i}r=
x , for i
= 1, ..., m5.4a. 7'(x_{1}, x_{,,}„_{ }s_{i}=x;
for = 1, n
5.5 a. Letting z
stand for T(x, , x„„ x'_{j}),
the standard Euclid component
itsTag is defined by z.
itsThg= k_{j}.
A variant record may also contain an otherwise clause otherwise 7;;_{+},
in which case the type of c may contain elements in addition to k_{1}, k„. If there is such a clause, we have the following additional axioms for the otherwise (n + 1) situation:
Let k_{J} be an element of the type of c
such that k_{j}+k_{i}
for I . in, and let
x;,,, be an element of
5.1 b. T(x_{1}, x„„ k_{j},
x„ ,) is also an element of T.
5.4 b. T(x, , k_{j},_{ }x„,_{1}
5.511 Identical to 5.5a.
The case with a field list containing
several fields
s_{j}, : end k_{J}
is to be interpreted as
end k_{i}
where is a fresh identifier, and 77
is a type defined as
type 77 = record To,............. T_{h} end record.
In this case x. s_{j}, is interpreted as x. s_{j},.
Now consider type T = Tdany).
5.1 c. T(x,, y,
x') is an element of T
for (y,
x') = (1(_{1}, xi), ,(k„, x„), (k,,,
where k,
k_{i} for = 1, It.
5.2c. These are the only elements of T.
5.3c. T(x, , x,„,
y, x') s_{i}= x, for i= 1, ...,
There is no 5.4c since access to the variant part
of the record may only be done using
the discriminating case statement (see Section 12.5).
Machinedependent
records do not change verification properties. The ad‑
ditional information supplied can be ignored (unless the machine interprets certain locations specially).
Set Types
type T.—set of T_{o}
Let x, be an element of T_{o}.
6.1. T( ) is an element of T.
6.2. If x is an element of T, then x+ T(x_{o}) is an element of T (the operator + is defined below).
6.3. These arc the only elements of T
6.4. TCV/„X2....,.x„)
means T([[T( )+ T(x_{1})] + M_{2})] + • + ^{7}1^{x}J1
6_{.}5,
T. Base Type To.
It I denotes the empty set, and T(x_{o}) denotes
the singleton set containing .x^{.}„. The operators +, *, xor, and in, applied to elements whose type is set, denote the conventional operations of set union,
intersection, difference, symmetric difference, and membership. The operators < = and > = denote set
inclusion. The specific axioms
defining these operators are omitted.
Note that Euclid
allows implementations to restrict set types to he built only on base types with a specified
maximum number of elements.
Alodule
Types
Because modules are by far the most
complex part of Euclid, this section contains a large amount of explanation as well as the technical details of the module
rule. The explanatory material can be
read now. However, we recommend that Section 10 on procedures and functions be
read before reading the rule and the technical
details. An example of the use of the module rule appears as Appendix 3. Additional comments on the module construct appear
in the Epilogue. The material on modules appears here because modules, like
subrange types and array types, are
type constructors.
type T(const C)= pre P1; post QI; module t invariant Q0; imports
(var Y const D readonly R)
exports
(const (K I, p, J^{.})
var VI readonly RI)
const K; var V
procedure p(var X2 nonvar C2)= imports (var Y2 nonvar D2) pre P2; post Q2; begin 5_{2 }end
function ^{•}(nonvar C3) returns G = imports
(nonvar D3) pre
P3; post
Q3; begin
S, end
initially imports (var Y4 nonvar D4)
post Q4; begin S, end abstraction
function A returns
t, =imports
(nonvar D5) begin
S. end
invariant Q
finally imports (var Y6 nonvar D6) pre
P6; begin S, end end
T
The parts of a module definition are
explained in the section on module types in the Euclid report. We assume that
equality is not exported. Nonvar denotes
the list of const and readonly identifiers. Each of c, y, d, r, kl,v1,r1, k. r. x2, c2, d2, e3, d3, y4, d4,
d5, r6, and d6 denotes the list of
identifiers in the corresponding upper
case declaration (p and f denote declared routines). As the Euclid report requires, the lists kl, vl, and ^{•}l are sublists of k, v, and v (yes, r, not r), respectively. The
declarations K and V may not
include identifiers from v or r. The
list (15 is a sublist of c, d, k, and v H. The arguments of PIand QI may
include as free variables only identifiers from c,
y, d, and r.
the arguments of P2, Q2, P3, Q3, Q4, and P6 may only include t and their respective formal parameter and import lists; Q3 may also include g. Q, the "concrete invariant," may only include c, (1, k, and
v vl, that is to say, the same identifiers as (15. Q0, the "abstract invariant,"
may include c, d, and t.
The exported identifiers of kl, vl, and rl are treated as if they were fields of a record type named T. The abstraction function A maps the identifiers in d5 into a value of type T(c); its body may contain constructs outside Euclid. The function A is for verification purposes and is not callable from a Euclid program.
The module is a
mechanism for providing encapsulation and the support of data abstractions. There are two points from which
it may be viewed: The users of the
module sec only the abstract pre and postconditions associated with module routines and the pre and postcondition of
the module itself. The implementor of
the module also secs the bodies of the routines and the (concrete) identifiers declared within the module. The
connection between the concrete and abstract
identifiers is the abstraction function, A, which
transforms a set of concrete
identifiers to an abstract identifier. See [8] for a more complete dis‑
cussion of the role of A.
The module rule given below contains a conclusion and eight premises. We shall explain the structure of the rule, describe the purpose and workings of each premise, and finally give the rule itself.
The conclusion of the rule involves the
instantiation of a module identifier and
the use of that identifier in a scope. Premises 16 are properties required of the module definition: these verifications need
be done only once per module definition.
Premise 7 discharges the instantiation precondition; this must be proved each time a module is instantiated. Premise
8, itself in five parts, uses the
verified definitions (formulas 8A8.4 which depend on premises 16) to verify the uses, in premise 8.5, of the module identifier
in the scope. Thus the module rule has
the structure
1, 2, 
3, 4, 
5, 6, 

7, 



[8.1, 
8.2, 
8.3, 
8.4] I 8.5 
P(varx:
T(a); R A QI
We now describe each premise in more detail. In premises 16 the substitution of a call of the abstraction function, A, for the name of the module, t, converts a predicate on the abstract identifier t to one involving concrete identifiers. Premise 1: concrete invariant implies abstract invariant. Premise 2: module precondition across declaration of module's local variables and body of initially establishes the postcondition of initially and the concrete invariant. Premise 3: verification of each exported procedure body, i.e., precondition and concrete invariant across body establishes postcondition and preserves concrete invariant. Premises 45: these two premises arc for each exported function body. Premise 4 is analogous to premise 3 except (a) the concrete invariant is automatically preserved since functions have no side effects, and (b) the singlevalued requirement described following Rule 10.2 is included. Premise 5 also concerns functions
;Hid is the
consistency clause described after Rule 10.2. Premise 6:
finally establishes the postcondition of the module.
Premise 7: instantiation environment implies module precondition with act
ua Is substituted for formals.
Premise 8: shows how the instantiated module variable x is used in the scope S. It must be shown in premise 8.5 that the instantiation environment across initially, S, and finally establishes R. In showing premise 8.5 one maj• use the four formulas 8.18.4, which give the properties of the procedures, functions, initially. and finally, respectively. Formulas 8.1 and 8.2 correspond to the conclusions of the procedure and function call rules; the only difference is that the abstract invariant may be used in proving the preconditions and is assumed following the calls. (This is the source of much of the utility of the module construct. it allows us to prove theorems using data type (generator) induction.) Formula 8.3 treats x. Initially as a parameterless procedure call that establishes the abstract invariant. Formula 8.4 treats x. Finally as a parameterless procedure call for which the abstract invariant may be used in establishing its precondition. (If x is declared to be an array of modules or a record containing modules, then x. Initially and x Finally must each be replaced in 8.3, 8.4, and 8.5 by a sequence of calls to initialization and finalization routines, respectively. These sequences are defined in the report.)
Ilere, then, is the full module rule.
7.1. (module rule)
(1)
Q D Q0 WO,
(2)
PI const K; var
V; S_{4}1 Q4(A/t) A Q,
(3) P2(A/t) Q1S_{2}1 Q2(A/t) Q ,
(4)
3 gl (P3(.410 Q {S _{3}}_{ }Q3 (A/t) Ag=g/(4, c, d)),
(5)
3 g(P3(.,1/1) Q DQ3(A/t)),
(6)
MAP) A Q {S,,} Q1,
(7) P
D PI (a/c),
(8.1) [Q0 (a/c, x/t, x'/t') D (P2 (x/t, x' /t' , a2/x2, e2/c2,
a/c) A
(Q2 (x2#/t, x' it' , a2#/x2, e2/c2, a/c, y2it/y2, a2/x2',
.y2/ y2')D R1(x24/x. a 2#/a2, )' 2#/y2))) . p (_{0}2,
e2)} RI A Q0 (a/c, x/t, x'/t'),
(8.2) (Q0 (a/c, x/i)D a3/c3,
a/c)
)
(x/t, a3/c3, a/c, f(a3, d3)/g) A QO
(a/c, x/t),
(8.3) PI (a/c) A (Q4(x4#/t, _{x'/t', }a/c,
y4#/y4, y4/y4')D R4 (x4ft/x, y4#/y4)) {x. R4 A QO
(a/c, x/t, x'/C),
(8.4) (Q0 (a/c, x/t„x'/I')D P6(x/t, x'
/t', a/c)) A (QI (a/c, j^{,}6#/j76, _{)},6/y6')D R(1.6#/y6)) .
Finally) R]
I‑
(8.5)
P(xft/x) {x. Initially; S; x. Finally) R(4/x)
P {var x: T(a); R AQI
where the "u" denotes fresh identifiers
and the scope of x is exactly S. As noted above, calls in S to
module routines use formulas 8.18.4. Although not written, calls in S_{2},_{ }S_{3}, S_{4},_{ }and S_{6} to module
routines are similarly handled, but using the A/t substitution ("x." is missing) and
without assuming Q0(a/c,
x/t) or
Q0(a/^{•}, x/t, Since a module may not import its own name, premise 2 is never "recursively applied" in T In the interest of simplicity, the formulas for recursion, return, and H are omitted in premises 35. Nonexported routines follow the rules for routines in Section 10.
In the simple case where the module T imports no var variables, i.e., initially and finally can have no side effects outside T, premise 6 and QI are missing (finally can have no visible effect) and premise 8 can be just
[8.1,
8.2]1— P(xft/x) A Q4 (x/t) Q0(x/t) (S) R (4/x)
where 8.1 and 8.2 contain no It's on
identifiers from y.
This formulation
of the module rule follows [8]. Other approaches [14, 5], which use different specification methods, might
have been substituted and, of course,
may be used to verify programs containing modules. With these alternative approaches there would be changes only to
the verification information
of the module.
Pointer
and Collection Types
type
T_{o }= collection of 7" var C:
type T= C
8.1. C. nil is an element of T
8.2. There are an
unbounded number of elements of T: ,
7r_{2}, ... (see 8.7).
8.3. If 13,, ...,11„ are elements of T' and Tr„ are distinct members, C. nil,
of T, then
.7r,,:fi„}) is an element of T_{o}.
Note that 7r,:/1,
indicates that 7r, denotes the component in the collection.
8.4. These are the only elements of T_{o}.
8.5. If C= n„:13„})
then C(70=13,.
8.6. For any element Tr+ C . nil of type T, n j=C(it).
We introduce the following
abbreviation:
If
C=
To({ 71_{1} :11,, ..., 7r„:/i,,))
then (C, y) stands
for
To({7(1431,••,TE,,:fl„)—{ni:fli} +
No operations are defined on the elements of T except test of equality, 1', and the standard function C. Index. The only defined property of C. Index is that it is onetoone. For every collection
there are two standard procedures, C. New(t) and
C. Free (t), involving the elements of T. Assume the declaration var
t: T, and that C=
(fir,: /I_{"} &D.
8.7. C. New(t) means 1:=7t
where i_{t }is an element of 7; 7r* 7r, for i= 1, ..., n,
and C:=1;,ttn_{i}: tr„:/3„; {n: fl}) where /3 is undefined (and may not
be referenced).
8.8. C. Pree(t) means
C:=T„({7,: — {1: C(t)}) (recall C(t) means It)
t C. nil.
Declarations
The purpose of a declaration is to
introduce a named object (constant, type, variable, function, or procedure) and to prescribe its properties. These
properties may then he assumed in any
proof relating to the scope of the declaration.
Constant, Variable, and Type Declarations
If D is a sequence of variable and type declarations,
then
D;
S
is called a scope, and the following are its rules of inference (some
expressed in the usual notation for
subsidiary deductions):
9.1. its Type= T, x#E T1 P{S(xtt/x)} Q
P{varx:
T; S} Q
where its7:rpe
is the standard Euclid component. The substitution of the fresh identifier 4 for
x expresses the fact that x is a "local" variable. T is any type except a module (see Section 7) or a structured
type (record or array) involving modules whose initially
or finally clauses
modify imported var identifiers.
The separate rules required to cover
these structured types are omitted.
9.2. P(e/x){const x : e} P.
This axiom also
applies to structured constants according to the order of the components.
9.3a. x =
y n P(4/x) {S} Q(xitlx, x/y)
P {bind varBindingCondition x to
y; S} Q
9.3 b. i= = y(i) P(x#/x) (S}
Q(xit/x, (y, i_{o}: x)/y)
P {bind
varBindingCondition .x
to y(0; S} Q
where, in all cases, l_{c}, and 4 arc fresh
variables; and where varBindingCondition is readonly, var or empty.
9.4. II P IS) Q
P {type
T= •• ; S} Qwhere
II
is the set of assertions derived
from the type declaration of T in the manner
described in Sections 16 and 8.
Parameterized Types
type T(c)= pre
PI; De/it
9.5. PD PI (a/c), P {const c: = a;
type T' = Defn; var x: T'; S}
Q
P{var T(a); S} Q
type 1"(...,:v, ...)— •• •
type T,,= collection
of T'(..., unknown,
...) var C:
type T= j C
If T is referenced as the object type of a collection, then one or more of the actual parameters may be specified as unknown. In such cases the component of 11 (in Rule 9.4) associated with t is the disjunction
^{U}a in x (anyi [te collection of T'
(..., a, ...)].
9.6. C.
Nov (t,
y) means all of Section 8.7 except
that the type of /3 is y,...).
Procedure Declarations and Calls
procedure p(var X, nonvar C)= imports
(var Y, nonvar D)
pre P;
post Q; begin
S end
Nonvar denotes the list of const and readonly identifiers. Let x, c, y, and d be the identifiers declared in X, C, Y, and D, respectively. P and Q are each predicates involving as free variables only x, c, y, and d. Q may also involve x' and V. fresh variables which denote the initial values of x and y on entry to the procedure body.
10.1. (procedurecall rule)
[P(al/x, el /c) n (Q(alit/x, el /c, 4/y, al /x', y/y')m
R1 (a 1 tt/al , .4/y)) {p(al, el)} RI, Q {return
asserting Q} false,
H]
=x' y = y' _{A }P {S} Q
^{P}(0/x, _{c/c) }n (Q (4/x, e/c, 4/y, a/x', y/y')p R(att/a, 4/y))
{p(a, e)} R
This rule, which is similar to the adaptation rules in [7, 3], assumes the above declaration of procedure p. If the procedure p is nonrecursive, the premise of 10.1 can be just
[42 {return asserting Q}
false, II] x=x' n y= P{S} Q.
14 12.. I 1 ,) _{t}l ct
In 10.1 a and e are the list of actual parameters which correspond
respectively to the formal parameters specified as variable
and nonvariable parameters. Note that the elements of a and
'' will, in any legal Euclid program, all be distinct in
the sense that none can overlap any other. H is the conjunction of the
assertions for each x€ X and CE C, that they are elements of their declared type.
(The members of Y and D need not be included in this H, but
are covered by 9.1 and 9A.) The "n" indicates that fresh variables are to be
used. Recall that the prime symbol (') denotes initial value of
the corresponding formal parameter at procedure body entry. By convention, 1' and
R do
not contain primes. An example of the application of Rule 10.1
is contained in Appendix I. A full discussion of this rule appears in
[4] which compares this rule to several other rules, including those contained in [7, 9].
It should be noted that if two or more of the
actuals, a, are
components of the same array, a slight complication arises in
substituting for the actuals. RIa a, y# ,/y) may evaluate to a formula of
the form
R (a 1 ft1B(1,) a2 /^{B}(!1) (.1„))•
Since the nonoverlapping rule guarantees that there
exists a k where 1 k
Sm such that i_{k}+j,„ the
substitution is welldefined. Applying the rule
for array
element substitution will reduce this to
R((13. i„,): a ift)/B,
(B, •• .,/,,>: _{0}2)/B).
At
this point simultaneous substitution is no longer welldefined. We therefore define
extended
simultaneous substitution with the rule
R(IB, <i_{1}, i„,>: a I ft)/B, (13, 0,, j„>: (124/B)
= RW13, <i,, ...,i„,>: 0,, a2tt)/B).
Note that in verifying Euclid programs this
situation can only arise in connection with substitutions
generated by application of the procedurecall rule. In
this environment, we know, because of the nonoverlapping restriction, that replacing
the simultaneous substitution with sequential substitutions produces identical
results regardless of the order in which they are performed.
Note that we do not have an
independent rule covering the return
statement. Rather, we have embedded it
in the above rule for procedure calls, which allows us to use the axiom
Q (return asserting
Q) false
in proving P {S} Q for p. Informally the rule states
that any return causes us to exit
the statically enclosing procedure. Although the syntax of Euclid is just "return,"
we have added the "asserting
Q" clause
in order to state succinctly the axiom for return. We
assume a preprocessor, if necessary, that determines the
statically enclosing procedure associated with each return and adds to
each return the corresponding Q. This
addition is necessary to ensure against making an unsound
inference about a return from an internally nested procedure with a
different postcondition. The statement return
when B may
be replaced (as
Rules I,n the hogranuning Language kuelid Is
specified in the Euclid report) by the statement if
B then return end if.
Beware, the axiom involving return may
not be used immediately if the procedure p contains an instantiation of
a module whose finally clause
falsifies Q. In
such cases, the expansion described in the Euclid report for
moving the finally clause
must he first
applied.
Rule 10.I may he used in proving assertions
about calls of the procedure p, including those occurring
within S itself
or in other declarations in the same scope. The rule is applicable
to all recursive calls because of the clause in the premise
to the left of the turnstile, H. In this "recursion" clause note that
the symbols are deliberately different from those in the rule's conclusion: R1 replaces
R, and
al and
el replace
a and
e to
allow different formulas and actual parameters to be used for
recursive calls. The entire premise of Rule 10.1 need be
proved only once for each procedure declaration, not once for each call.
For a procedure declaration itself we have
10.1a. R (procedure p ... begin S end) R.
Function
Declarations and Calls
function
f(nonvar C) returns G =imports (nonvar
D) pre
P;
post Q; begin S end
The same notation is used as in procedures. Nonvar
denotes the list of const
and g. A rule
similar to 1 0. 1 a applies to function declarations:
and readonly identifiers; P is
a predicate involving c and (1; Q involves c, (1,
I0.2a. R Junction f ... begin S end) R.
Function calls, unlike procedure calls, appear in
expressions which arc part of statements. There is no functioncall
statement corresponding to a procedurecall statement. The proof
rule for functions depends crucially on the fact that Euclid
functions have no side effects, a consequence of the absence of var in a
function declaration. Therefore, the order of evaluation of functions within an
expression does not matter.
Suppose in an expression, possibly within S itself
or in other declarations in the same scope, there is a call f(a) of
the function f with
actual parameters a.
The
rule
10.2. (functioncall rule)
[P(a 1/c) Q (a 1/c,
f (a 1 (1)/g),Q (return
asserting Q) false,
H] [P{S}
Q, 3 gl(PISI g^{=}g1(c,d)n,
H g(PQ)
P(a/c)Q(a/c,f(a,d)/g)
I 1 I
may he used in
verifying the properties of the expression involving _{.}I(a)._{ }Since
the term ((a, (IL rather than ((a), occurs in the conclusion of the rule,
applying this rule to
an assertion R will first require the verifier to apply the substitution
fla, (I) f(o) to R. This rule is due to David Musser;
a full discussion is in [12].
The
second premise, called the consistency clause, ensures that the lemma in the conclusion of the rule will
not be inconsistent. In the first premise, the P;S}Q part gives the relation which the function's declared body, S, and it single precondition, P, and single postcondition, Q, must satisfy. The part in volving 3 gl is a requirement that the function be singlevalued; it is discussed below. These, like the second
premise, need be proved only once per function declaration. The other three parts of the premise
(before the H) are the recursion clause, the definition of the return
statement, and the
type information for each cc C and g, respectively. The return statement is the same as in
procedures, including
the "asserting Q" clause. The statements
return expr when B return expr
are
equivalent to
if B then gi=expr; return end if
g:= expr; return,
respectively.
In 3 g1(P{S) g = gl (c, d)), gl is a mathematical
function of c and (I. The premise is thus equivalent
to requiring that S defines a mathematical function, i.e.,
that it
be singlevalued. Note that the implicit universal quantifiers associated with formulas in the
Hoare logic go inside the existential quantifier in this formula. If the function
contains no module variables in its parameter or import lists, the 3g/ part is
automatically true because Euclid is a deterministic language.
The standard equality of Euclid modules (if equality is
exported) is, informally, componentbycomponent (bitwise) equality of the modules'
concrete representations. With respect to this equality, Euclid functions of
modules arc also singlevalued and thus the 3g/ part is again true. However, other
equality relations may be needed in the verification of programs which use
Euclid modules. In particular, the abstraction function of a module, A, may be used to induce an equality relation
on the concrete objects, a relation that is different from the standard equality.
For example, suppose a stack module uses for its concrete representation an
array and a topofstack pointer. The stack operations push, a second push,
and then a pop ought to yield the same stack as does just the first push. Using
an abstraction function that ignores the "unused" part of the array
(where the second pushed element remains), the single push will give a stack
equal to that of pushpushpop; using the standard equality, this will not he true. Thus
always using the standard equality will not suffice to verify certain programs. As
another example, consider sets represented by arrays. Equal sets, by a useful
abstraction function, contain identical elements although not necessarily in the same
order within the array. The abstract operation of choosing an arbitrary element
from the set can be implemented by returning the first element
Statements
Statements are
classified into simple statements and structured statements. The meaning of all
simple statements (except procedure calls) is defined by axioms, and the meaning
of structured statements (and procedure calls) is defined in terms of rules of
inference permitting the properties of the structured statement to be deduced from
properties of its constituents. However, the rules of inference are formulated so
as to facilitate the reverse process of deriving necessary properties of the
constituents from postulated properties of the composite statement. The reason for
this orientation is that in deducing proofs of properties of programs it is most
convenient to proceed in a "topdown" direction.
Simple Statements
Assignment Statements 11.1. P(y/x) {x:= y } P
The substitution definitions given in Sections 4, 5, and 8
apply here. Procedure Statements
Procedure statements are explained
in Section 10 on procedure declarations and calls.
Escape
Statements
Return statements are explained in
Section 10. Exit statements are explained in Section 12.6.
Empty
Statements
11.2. P{ P
Assertion
Statements
11.3. P Q {assert P n Q
11.4. If the checked option is specified, we
may use Q )assert Q A
B where Li is a Boolean expression. 
Note that exit plays the same role with
respect to loops that return plays with respect to
procedures and functions (among other things, it is associated with the nearest
enclosing loop and a corresponding exit assertion; and the axiom involving exit
may not be used directly with certain module instantiations). Like return
when B, the statement exit when B may be replaced by the
statement 
I if
B then exit end if.
Structured Statements
Compound Statements
12.1. ,
lS_{1}1
I;
for i= n
l„ ' S_{t}; .,.; S,,}
If Statements
12.2. P I31S,1 Q, P A 113 (S_{2}1 Q
P :if B then
S, else
S, end if;
Q 12.3. P A B ;S) Q, P
A113DQ
B then
S end if)
Q
Case Statements
12.4a.
P
(x = k_{i}) 1S_{i}) Q, for i = 1, n
For Statements
For statements may always be expanded as explained in the
Euclid report. However, for simplified cases the following rules
are available, where the loop body S may not contain an escape statement:
Let T be a subrange type.
12.7. (T. first x S T. last) A P([T. first ..
x)) {S} P([T. first .. x])
P([ ]) {for x in
Tloop S end loop} P([T.
first .. T. last]) 12.8. (T. first x T. last) A P((x .. T. last]) {S}
P([x .. T. last])
P([ ]) {for x decreasing
in T
loop S end loop) P([T. first . .7'.
last])
[u . . r] denotes
the closed interval u, v,
i.e., the set Ulu i v), and [u.. v)
denotes
the halfopen interval u, v, i.e., the set (flu i< Similarly, (u v] denotes
the set {ilu <i
v}. Note that [u.. u)=(u . u] is the empty set. Since X, T. first, and
T. last arc constants, S cannot
change x, T:
first, or 7'. last.
Let
T be
a set type.
P :case x of S_{i}; ...; S„ end case) Q
12.4 b. P A = k_{i}) (S_{i}l Q for i I, n, P x not in (k„ Q
F {case x of
k, S,; ...; S„; otherwise S„ end case} Q
Note
that k„,k,„...,k,„S stands for 5; S. The
type of
is constrained as in the section on variant records.
12.5. P {var onyx: T(k_{i}); S; begin
var x: T(k):=anyx; S_{i} end) Q, for i= 1, n Epilogue
onyx: T(any);
S; case x:= unyx of S,; ...; k„ S„ end case) Q
There may be other formal parameters in T besides the
single any (see the expansion
in the procedure declarations section of the Euclid report). The case
var onyx: T(any); S; anyx:=
y
is already covered by the assignment axiom (Rule 11.1).
Loop Statements
12.6.
Q {exit asserting Q} false P{S}
P
Ptloop S end
loop) Q
We would like to note a few points about our experiences
in constructing these proof rules.
We began to axiomatize Euclid in early 1976, and
essentially ended over a year later. At the start we
expected an interesting but not terribly challenging project. We
were halfright — it was for us interesting and challenging.
We learned a great deal about both proof rules and Euclid—two topics we were
not nearly so well versed in as we thought.
Our increased understanding of Euclid paid a
clear and immediate dividend. A number of improvements to
the language were made as a direct result of facts discovered
during the axiomatization. (This in turn meant the need for new proof rules.)
The longterm payoff of our increased understanding of proof rules is less
certain. We would like to believe that were we to begin a similar project
today. we would rind it considerably less painful. It is,
however, far from dear to us that it would be the routine task it must
eventually become if rigorous definitions of new
programming languages are to be the norm. We would surely try
to write the proof rules in parallel with the design rather than afterward, as
we did in some
instances with Euclid. We spent an inordinate amount of time
and effort on problems related to modules. Ilad we felt free to make substantial
changes to this part of Euclid, much of this time and effort could have. been
avoided, and the proof rules themselves simplified substantially.
A somewhat disturbing aspect of these proof rules
is our lack of complete confidence in them. There are some rules with
which we arc still unhappy, although we know of no errors in
them. Nevertheless, it would be naive for us to believe that
there are no remaining errors; many bugs were found in earlier versions, and
we have too much programming experience to interpret this as a good sign. Our
approach to "verifying" these proof rules has been to study each rule
in (as much as possible) isolation. We have informally
presented (to ourselves and others) the reasons we
believe each rule to be appropriate, and have tested each rule
on as many distinct cases as we had the energy to look at. The inadequacies of
this approach have been cogently argued in the literature on programming. What
is needed is a more formal approach to validating proof rules. The work by
Donahue [2] on "verifying" soundness via a complementary definition
and by Clarke [I] on completeness seems a step in this direction. We would
very much encourage and be happy to talk with anyone who
wishes to examine rigorously the soundness and completeness of
these proof rules.
Ark nowted gmems. We arc greatly indebted to C.A. R. Hoare and Niklaus Wirth
for their axiomatization of Pascal. We are grateful
to them, and to SpringerVerlag, for permission to use sections of the Pascal a x loam tiza t ion [91 in this paper.
Suggestions, comments, and criticisms by numerous colleagues and the referees have greatly aided us; David Musser has
been especially helpful. As always, responsibility
for errors and problems remains with us. We appreciate the efforts of Betty
Randall and Lisa Moses in typing and
formatting the various versions of this work.
Appendix 1 Procedures
Consider the trivial procedure, with only one var parameter, one const parameter,
and no imported variables
procedure p(var signedInt, b: signed 1110= pre true;
post a 2_{*
}b;
begin var c: signed Int; c: = 2* b; if a>
c then a = c end if end.
Letting S stand for the body of this procedure,
it is easy to prove true {S} a 2 * b.
The invocation of this procedure will (in general) change
the value of a in
some manner dependent on the initial values of a and it (and, if present and
referenced from within S, on values of imported variables).
Now the effect of any call of p(z, w) is to change z such that z.5_2_{*}
w, and using the procedurecall rule (10.1) we may validly conclude for any R that
true A (42*WDR(.7 if/z)) {p(z, w)} R.
In particular, R might be just z 2*w or R might
involve variables other than z and w if the call p(z, it) followed statements
involving those other variables. The properties of a call of
p arc contained
solely in the postcondition a 2*
b.
The given postcondition is not the only property
that can be proved about p. For
example, if the postcondition a= min(a', 2* b), where the prime denotes the
initial value of a, had been supplied with p, we could validly conclude
that
true A (4= min (z, 2 * w)p R (4/z)) {p(z, w)} R.
It is important to see how the rule accommodates
a structured actual variable in a var position.
For a call p(d(i), i) where
d is an array and R is d(i)2* i we may validly conclude, using
the original postcondition, that
true A (4(i) 2 * iPdit(i) 2* i) {p(d(i), i)} d(i) 2*
i.
If the formal
parameter it were
also a var parameter, we may validly conclude true
A (4(0 * 4(4 52_{*} ift) {p(d(i), i)} d(i) 2
* i
which uses ift in place of i in three places. In the var
b case,
by the rules of simultaneous substitution (see discussion following
Rule 10.1), Q(d#(0/a,
i#/h) is dft(i)2*i# while RW11(01(04/0 is dft(i41)2_{*}4 In
the const b case, Q(4(i)/a, i/b) and R(dft(i)/d(i)) arc both d#(05 2*
Note that while making the second formal var has no
effect on the behavior of the program, it does reduce the number of things we can
prove. Though the procedure does not change the second parameter,
this cannot be deduced from the postcondition
associated with p.
Appendix 2
Functions
Suppose we have the function declarations
function f (c: signedint) returns in: signedlat =
pre P_{f}(e); post Q_{r}(c, at); begin
S_{f} end
function g(c: signedlat) returns at: signed Int =
pre P_{g}(c); post
Q(c, in); begin
S_{R} end
and suppose that we
have proved of the two bodies P_{f} {S_{f}} Q_{f} and P_{g}{S_{g}} Q_{g}
and proved
of the pre and postconditions Q_{i})
and 3 in(P_{g} Q).
The axiom for the assignment statement x = f(g (x)) +
leads to
R(Lf(g(x))+ (x:=f(g(x))+ I} R.
The two function calls g(x) and f(g(x)) appear in the expression f(g(x))1 1. The functioncall rule applied to g requires that the precondition P(x) be established which in turn yields the postcondition Q_{g}(x, g(x)). The latter may be used is applying the functioncall^{}rule to f to establish P_{f}(g(x)) which yields Qi(g(x),f(g(x))). The two postconditions Q_{r}(g(x), f(g(x))) and Q_{g}(x, g(x)) may be used to establish the substituted R term. Having done all the above, we may conclude that R holds after the assignment.
As another simpler example, to show
P (if f(x) > 0 then S, else S_{2 }end if) Q, it suffices to show the three premises
PD P_{f}(x),_{}
PA f(x)>0(S,} Q, P_{A}1f(x)>O(S_{2}) Q.
The first premise shows that it is
legal to call f (x) and, by the functioncall rule applied to 1'
to use the postcondition Q_{f}(x, f(x)) as an
additional hypothesis in establishing
the second and third premises of the if rule. As a concrete example of this schema, suppose we have the function
declaration
function power (x, y: signed nt) returns
z: signed]^{.} nt =
prey? 0; post
z= x ** y; begin S end
and suppose that we have proved
rO{S}
:=x**y,
3 z(j,0Dz..v**y).
We wish to show
h 1 power(a, b)> 0 then c: = true else c: = false end if) c
Ha ** b> 0).
Since
b b.0,
the functioncall rule applied to power(a,
b) yields the conclusion power(a, b). a ** h. Using this equation it is easy to show
b I A pOlVer(ub)> 0 (c:= t rue ) c = (a ** h> 0), b I A power (ct, b) 0 {c^{:}= false} = (a ** h > 0), that is,
b I **
b>0Da **b>0
b 1 A ** h ^{p}raiseHa
** 17>
0).
Note that if the formal parameter y were of type unsigneant, the precondition of power could be just the constant true. In this case the compiler, rather than the verifier, would have to be satisfied that 13 0. The compiler might, of course, produce a legality assertion for the verifier.
Appendix 3 Modules
As an example of the use of the module rule, we shall use a variant of the small' ntSet example in [81 Our module small' nt Set provides the abstraction of a set of integers in the range 1. . 100. The abstract operations are insertion and removal or individual elements and a membership test. When a variable of type small' ntSet is declared, it is initialized to the empty set. The set will be represented by a Boolean array, S, of 100 elements,
S: array 1 . 100 of
Boolean.
S(i)=true iff i belongs to the set. In this
example } are used for set brackets. Comment
brackets around nonEuclid pre and post are omitted.
type small'
ntSet =
pre true
module smallSet
invariant true
exports
(insert, remove, has, = ) var S: array 1 .. 100 of
Boolean
procedure insert
(i: integer) =
pre 1 . 100 n smallSet
= smallSet'
post smallSet
= smallSet'u { i) begin S(i): = true end
insert
procedure remove
(i: integer) =
pre
1 5 i 100 A smallSet = smallSet' post smallSet
= smallSet' {i} begin S(i): = false end remove
I'rool kale, for the Pi^{.}..Tramming
I angwige
function has (i: integer) returns
hasResult: Boolean =
pre 1 100
post hasResult (iesmallSet)
begin hasResult:= S(i) end has
initially
post smallSet=emptySet I
begin for] in S. I ndexType loop S(j):= false end loop end
abstraction function set Value returns
result Set = imports (S) begin
resultSet = ji S(j) A 1 j 1001 end
invariant
true end smallIniSet
At the point where we encounter this module definition program, we verify the asserted properties of the definition. The necessary formulas to be verified here are derived from the module definition and the first six premises of the
module rule:
(I) true D true
(2) true {liar 5: array
1.
. 100 of Boolean
begin for j in
S. IndexType
loop
S(j): = false end loop
end) set Value(S)= emptySet A true
(3) (insert) 1 i 100 A set Value(S)= set Value(S) A true (S(i):= true)
set
Value(S)= set Value(S)u A true
(3) (remove) 1 i
100 A set
Value (S)= set Value(S') A true
{SW. = false)
set Volue (S)= set Value(S') {i) A true
(4)
3 g1(1
i 100 A true {hasResult S(0)
hasResult
(i E set Value (S)) A hasResult = g I (set Value (S)))
(5) 3 hasResult (I i 100 A true hasResult
=(iesetValue(S)))
(6) there is no finally, so this premise is missing.
In the above formulas the abstraction function set Value has its imported identifier S included as an argument. We shall not go through the exercise of proving these. They are all trivially verifiable.
Now, to show
x =2 (var x:
smallIntSet; x. insert (3); x. insert
(5); y:=X. has(3);
x. delete(3);
z: = x end)
:= {5}
A y= true A x
=2,
where v and z have been declared prior to x, we can use the remainder of the module rule.
First, to verify the declaration var x: smallIntSet, we need only show
(7) x=2 D true.
Having verified this, and premises 16, we may now derive and, by premise 8 in the module rule, assume and use the formulas (where xl, x2, x3, and x4 are fresh variables)
(8.1 a)
true:D(1 3 100 A (x =xo {3} Dx/ = {3} A xtt=2))
x. insert (3)) x= ;3) n4=2
(8.(
b) true (1^{.}5 100
A (x2=x u (5) Dx2= {3, 5} A x#=2))
{x. insert(5)} x= {3, 5) A 4=2
(8.1e)
trueD(1 100 A (x3 =x (31 Dx3 ={5) x#=2 A y=
true))
. delete (3)} x= {5) A x#= 2 A y= true
(8.2) (trueD 1 3 100)
x Ims(3) = 3 ex
(8.3) true A (x4
= empt ySet P x4 = etnptySet x# =
2) (x . Initially)
x=
empt_ySet xlt= 2, i.e., x#= 21x . X ^{=}emptySet
A4=2.
(8.4)
This premise is missing because there is no finally.
We now instantiate premise 8.5 by
setting S to be
x insert(3); x. insert(5); y:= x. has(3); x
delete(3); z:= x end and R to be
x= {5} A y= true A X=2
obtaining
(8.5) 4=2 {x . Initially; 5} z= (5) A y= true
A4=2.
We now prove premise 8.5 using the formulas
8.1a8.3. Using (8.3) we reduce the
formula to be proved to
.4=2 A x =emptySet {S} z= (5) A y= true A Xtt ^{=}2. Next, using (8.1 a), we get
4=2 A x= (31 fx. insert
(5); = X . has
(3); x. delete(3);
z;= x)
z= {5) A y=
true A .4=2.
Then, by (8.11)), we get
4=2 A = {3, 5) {y:=x.
has(3); x. delete(3);
z:= x) (5) _{A }y= true A x#=2.
By (8.2) and the assignment axiom, the
problem reduces to
x#= 2 A X= {3, 5) A y = true ix delete(3); z:= x} z= {5} A y= truc xlf= 2. By (8.1 c) we get
xt= 2 _{A }x= {5) A y=
true{z.:=x}z= PI A y=true A 4=2
which, by the assignment axiom, is true.
Since the module smalllntSet imports no var variables, the instantiation of premise 8.5 could have been from the simpler form of premise 8. If this were done, there would be no formula 8.3 to be used.
References
1. Clarke, E.M. Jr.: Programmin^{g}
language constructs for which it is impossible to obtain good Hoarelike axiom systems.
Conference Record of the Fourth ACM Symposium on Principles of Programming Languages, Los
Angeles, pp. 1020. New York: ACM 1977
2. Donahue, J.E.: Complementary
definitions of pro^{g}ramming lan^{g}uage semantics. In:
Lecture Notes in
Computer Science, Vol. 42. BerlinHeidelbergNew York: Springer 1976
3. Ernst, G.W.: Rules of inference for
procedure calls. Acta Informat 8, 145152 (1977)
4. Guttag, J.V., Hornin^{g},
J.J., London, R.L.: A proof rule for Euclid procedures. In: Formal Description of Pro^{g}ramming
Concepts (E. Neuhold, ed.), pp. 211220. AmsterdamNew YorkOxford: NorthHolland 1978. Also
USC Information Sciences Institute, Technical Report ISIIRR7760, May 1977
5. Gutta^{g}. J.V., Horowitz,
E., Musser, D.R.: Abstract data types and software validation. Comm. ACM (to appear). Also: USC
Information Sciences Institute, Technical Report ISI,IRR7648, August 1976
6.
Hoare, C.A.R.: An axiomatic basis for computer
programming. Comm. ACM 12, 576580, 583 (1969)
7. Hoare. C.A.R.: Procedures and
parameters: An axiomatic approach. In: Symposium on Semantics of Algorithmic Lan^{g}uages
(E. Engeler, ed.), Lecture Notes in Mathematics. Vol. 188, pp. 102116. BerlinHeidelbergNew York:
Springer 1971
8. Hoare, C.A.R.: Proof of
correctness of data representations. Acta Informal.. 1, 271281 (1972)
9. Hoare, C.A.R., Wirth, N.: An
axiomatic definition of the programmin^{g} language PASCAL. Acta Informat. 2, 335355 (1973)
10. Jensen. K., Wirth, N.: PASCAL user
manual and report. Lecture Notes in Computer Science, Vol. 18. 2nd ed. BerlinHeidelberg
New York: Springer 1975
11. Lampson, B.W.. Hornin^{g},
J.J.. London, R.L., Mitchell, J.G., Popek, G.J.: Revised report on the pro^{g}rammin^{g}
language Euclid. Xerox Research Center. Technical Report CSL 782, 1978. An earlier version appeared in: SIG
PLAN Notices 12. No. 2 (February 1977)
12. Musser. D.R.: A proof rule for
functions. USC Information Sciences Institute, Technical Report ISI•RR7762.
October 1977
13. Popek, G.J., Horning, J.J.,
Lampson, B.W.. Mitchell, J.G.. London, R.L.: Notes on the design of Euclid. Proceedin^{g}s
of an ACM Conference on Lan^{g}ua^{g}e Design for Reliable
Software, Raleigh, North
Carolina. SIGPLAN Notices 12, No. 3, 1118 (1977)
14. Spitzen. J.. Wegbreit, B.: The
verification and synthesis of data structures. Acta Informat. 4, 127144119751
15.
Wirth, N.: The pro^{g}ramming lan^{g}ua^{g}e PASCAL.
Acta Informal. 1. 3563 (1971)
Received
June 9. 1977
Note
Added in Proof
There may be some inconsistence
between these proof rules and the latest version of the Euclid report [Il]. The latter was recently
revised.