# Definition of pc for while loops

Hello,

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.

2 Likes

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

1 Like