Definition of pc for while loops


I just ran into a problem. I can not actually find the rules for pc for a while loop and applying the one I have written down yields something wrong. The while rule for vc is on page 12 of the speficiation, this is my rule for pc:

pc while(e)_Invariant(i)_Term(t; k) Q = i && (0 <= t <= k + 1)

I think the problem might be that I added the termination condition at all.

For example I test this program and get an assertion error:

int x;
_Assume(x >= 0);
while(x != 0)_Inv(1)_Term(x; k) {
    x = x - 1;
_Assert(x == 0);

I computed vc and pc by hand and using the above formula I get:

pc ... true = (x >= 0) => (0 <= x <= k + 1)
              // this is equivalent to:
              (x >= 0) => (x <=  k + 1)
vc ... true = true

If in the formula for pc I only return the invariant I would get that pc ... true = true.

Interestingly, I cannot find it in this year’s materials right now either.

However, I can tell you that it should be
i && (0 <= t)

So t is not allowed to go below 0 (this is needed so that the termination condition holds) and the invariant must hold, but k does not yet come into play.


The pc rule for total correctness is now added to the project description.

1 Like