London, Lampson, Horning, Mitchell, and Popek - Proof rules for the programming language Euclid

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 ³***, B.W. Lampson J.G. Mitchell', and G.J. Popek⁵****

USC Information Sciences Institute. 4676 Admiralty Way, Marina del Rey, CA 90291, USA = Computer Science Dept., University of Southern California, Los An^geles, 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

⁵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^guage 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 stora^ge 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^ge Euclid has been desi^gned to facilitate the construction of verifiable system pro^grams. Its defining report [11] closely follows the defining report [15] of the Pascal lan^gua^ge (see also [10]). The present document, giving Hoare-style 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 1-3. Other semantic defini‑

* To whom offprint requests should be sent. Supported by the Defense Advanced Research Projects Agency under contract DAHC-15-72-C-0308

** Supported in part by the National Science Foundation under grant MCS-76-86089 and the Joint Services Electronics Program monitored by the Air Force Office of Scientific Research under contract F 44620-76-C-0061

*** Supported in part by a Research Leave Grant from the University of Toronto and a ^grant 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⁷3-C-0368. 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 referenced-counted) 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(₃1v) may he read "P with y for .x."

^P(.^1.1^x1^,4'J•„)

denotes simultaneous substitution for all occurrences of any x_; by the corresponding v₁. 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, non-Euclid 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 type-checked 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₂, c„ are distinct elements of T.

.2. These are the only elements of T.

.3. = T. slice (ed for i= I, n

.4. c₁= 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}cv •_=7..--_i(_As>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₀.

3.1. T. first =in

3.2. 7'. last =

3.3. For all i in T₀ 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₀. prcd(i).

Note that since all elements of T are elements of all operators of T_oapply
to them.

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.;⁷1, • •• • ^Sru^: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₂, ..., 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₁) 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₂=--> 5₂' :7; end k₂

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_ir= x , for i = 1, ..., m5.4a. 7'(x₁, 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₁, 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₁, x„„ k_j, x„ ,) is also an element of T.

5.4 b. T(x, , k_j,x„,₁

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(₁, 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).

Machine-dependent 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₁)] + M₂)] + • + ⁷1^xJ1- 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₂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 1-6 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 8A-8.4 which depend on premises 1-6) 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 1-6 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 4-5: 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 single-valued 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.1-8.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 parameter-less 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₄1 Q4(A/t) A Q,

(3) P2(A/t) Q1S₂1 Q2(A/t) Q ,

(4) 3 gl (P3(.410 Q {S ₃}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 (₀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.1-8.4. Although not written, calls in S₂,S₃, S₄,and S₆ 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 3-5. Non-exported 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₂, ... (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₁ :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 one-to-one. 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_tis 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 1-6 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

^Ua 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. (procedure-call 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' _AP {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 ,) _tl 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 non-overlapping rule guarantees that there exists a k where 1 k Sm such that i_k+j,„ the substitution is well-defined. Applying the rule for array
element substitution will reduce this to

R((13. i„,): a ift)/B, (B, -•• .,/,,>: ₀2)/B).

At this point simultaneous substitution is no longer well-defined. We therefore define extended simultaneous substitution with the rule

R(IB, <i₁, 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 procedure-call rule. In this environment, we know, because of the non-overlapping 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 function-call statement corresponding to a procedure-call 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. (function-call 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 single-valued; 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 single-valued. 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, component-by-component (bitwise) equality of the modules' concrete representations. With respect to this equality, Euclid functions of modules arc also single-valued 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 top-of-stack 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 push-push-pop; 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 "top-down" 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

Structured Statements

Compound Statements

12.1. , lS₁1 I; for i= n

l„ ' S_t; .,.; S,,}

If Statements

12.2. P I31S,1 Q, P A-- 113 (S₂1 Q

P :if B then S, else S, end if; Q 12.3. P A B ;S) Q, P A-113DQ

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 half-open 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.

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 half-right — 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 long-term 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. I-lad 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 Springer-Verlag, 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 procedure-call 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 function-call 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 function-call^-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₂end if) Q, it suffices to show the three premises

PD P_f(x),

PA f(x)>0(S,} Q, P_A1f(x)>O(S₂) Q.

The first premise shows that it is legal to call f (x) and, by the function-call 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 function-call 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 ^praise-Ha ** 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 non-Euclid 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

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 1-6, 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.1a-8.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) _Ay= 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 _Ax= {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 Hoare-like axiom systems. Conference Record of the Fourth ACM Symposium on Principles of Programming Languages, Los Angeles, pp. 10-20. New York: ACM 1977

2. Donahue, J.E.: Complementary definitions of pro^gramming lan^guage semantics. In: Lecture Notes in Computer Science, Vol. 42. Berlin-Heidelberg-New York: Springer 1976

3. Ernst, G.W.: Rules of inference for procedure calls. Acta Informat 8, 145-152 (1977)

4. Guttag, J.V., Hornin^g, J.J., London, R.L.: A proof rule for Euclid procedures. In: Formal Description of Pro^gramming Concepts (E. Neuhold, ed.), pp. 211-220. Amsterdam-New York-Oxford: North-Holland 1978. Also USC Information Sciences Institute, Technical Report ISIIRR-77-60, 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,IRR-76-48, August 1976

6. Hoare, C.A.R.: An axiomatic basis for computer programming. Comm. ACM 12, 576-580, 583 (1969)

7. Hoare. C.A.R.: Procedures and parameters: An axiomatic approach. In: Symposium on Semantics of Algorithmic Lan^guages (E. Engeler, ed.), Lecture Notes in Mathematics. Vol. 188, pp. 102-116. Berlin-Heidelberg-New York: Springer 1971

8. Hoare, C.A.R.: Proof of correctness of data representations. Acta Informal.. 1, 271-281 (1972)

9. Hoare, C.A.R., Wirth, N.: An axiomatic definition of the programmin^g language PASCAL. Acta Informat. 2, 335-355 (1973)

10. Jensen. K., Wirth, N.: PASCAL user manual and report. Lecture Notes in Computer Science, Vol. 18. 2nd ed. Berlin-Heidelberg- 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^grammin^g language Euclid. Xerox Research Center. Technical Report CSL 78-2, 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•RR-77-62. 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^gs of an ACM Conference on Lan^gua^ge Design for Reliable Software, Raleigh, North Carolina. SIGPLAN Notices 12, No. 3, 11-18 (1977)

14. Spitzen. J.. Wegbreit, B.: The verification and synthesis of data structures. Acta Informat. 4, 127-144119751

15. Wirth, N.: The pro^gramming lan^gua^ge PASCAL. Acta Informal. 1. 35-63 (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.