The Eiffel Compiler / Interpreter (tecomp)

In this text describes a pure procedure call without any reference to object orientation. The ideas are from the book "The science of programming" from David Gries.

We assume a procedure call of the following form

(1) proc p(value x; value result y; result z) {P} B {Q}

with the following conditions:

- x, y and z are collections of variables.
- x, y and z must be distinct identifiers.
- P contains only x and y.
- Q contains only y and z.
- The body B can use only x, y, z and all local variables. It cannot refer to global variables.

The procedure call

p(a,b,c)

must fulfill the following conditions:

- a is a collection of expressions.
- b and c are collections of variables.
- a, b and c have the same type as x, y and z respectively.
- x,y and z are fresh identifiers not accessible at the point of the call p(a,b,c).

The procedure call

p(a,b,c)

is semantically defined as

x,y:=a,b; B; b,c:=y,z

therefore in wp-calculus we get

wp(p(a,b,c),R) = wp("x,y:=a,b; B; b,c:=y,z", R)

The semantical effect of the body B is what it does to the procedure variables y and z.

Since B cannot access any outside variables and all assignments to local variables except y and z are of no interest after the call, we can capture the effect of B by the values it assigns to y and z.

Lets assume B assigns during its execution the values u and v to y and z. With that we can substitute B by y,z:=u,v. Then we get

p(a,b,c) is x,y:=a,b; y,z:=u,v; b,c:=y,z

or with the assertions put into their proper place

x,y:=a,b {P}; y,z:=u,v {Q}; b,c:=y,z {R}

Now we want to calculate wp(p(a,b,c), R).

In order to have R after the call wp-calculus gives us as a condition before the call

((R[b,c:=y,z])[y,z:=u,v])[x,y:=a,b]

<=> (R[b,c:=u,v])[x,y:=a,b] <=> "R does not contain neither x nor y because they have to be fresh identifiers"

R[b,c:=u,v]

The substituted R still contains the free variables u and v. Therefore it is not yet in a usable form, because R[b,c:=u,v] is required to hold for all possible values of u and v. In order to make it usable we need to exploit {P} B {Q}.

We assume that {P} B {Q} has already be proved (as a proof that the procedure body does the job it promised). In order to use that fact, we need to be sure, that P is valid before the body. I.e. we require that

P[x,y:=a,b]

must hold before the procedure call.

At the point after the body

Q => R[b,c:=y,z]

has to hold. If we transform that before the procedure call we get

((Q=>R[b,c:=y,z])[y,z:=u,v])[x,y:=a,b]

<=>

(Q[y,z:=u,v]=>R[b,c:=u,v])[x,y:=a,b]

<=> neither Q nor R contain x; y has already been substituted

Q[y,z:=u,v]=>R[b,c:=u,v]

So we have

wp(p(a,b,c), R) <=>

P[x,y:=a,b] and Q[y,z:=u,v]=>R[b,c:=u,v]

Since the predicate contains free variables, it needs to be universally quantified

wp(p(a,b,c),R) <=> P[x,y:=a,b] and (A u,v |: Q[y,z:=u,v]=>R[b,c:=u,v])

The above form is still a little bit clumsy. And indeed the variables u and v are not necessary. We can write the equivalent condition

wp(p(a,b,c),R) <=> P[x,y:=a,b] and (A y,z |: Q=>R[b,c:=y,z])

With the basic convention that all free variables need to be universally quantified we get

wp(p(a,b,c),R) <=> P[x,y:=a,b] and Q=>R[b,c:=y,z]

Local Variables: mode: outline coding: iso-latin-1 outline-regexp: "=\\(=\\)*" End: