SourceForge.net LogoThe Eiffel Compiler / Interpreter (tecomp)

doc/internals/verify eiffel sw/procedure call

procedure call

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.

Definition of procedure and procedure call

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:

  1. x, y and z are collections of variables.
  2. x, y and z must be distinct identifiers.
  3. P contains only x and y.
  4. Q contains only y and z.
  5. 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:

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

Semantics of a procedure call

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]

Simplificaton of the weakest precondition

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

- Definition of procedure and procedure call

- Semantics of a procedure call

- Simplificaton of the weakest precondition


ip-location