Invariants and old()

[ghost]

I'm verifying the following piece of code with boogie:

var v: int;

procedure main()
    modifies v;
{

    v := 0;

    while(true)
        invariant v > old(v) || v == 0;
    {
        v := v+1;
    }

}

And the output is:

main2.bpl(10,9): Error: This loop invariant might not be maintained by the loop.
Execution trace:
    main2.bpl(7,7): anon0
    main2.bpl(9,5): anon2_LoopHead
    main2.bpl(12,11): anon2_LoopBody

Boogie program verifier finished with 0 verified, 1 error

P.S. I know "This is Boogie 2" is very outdated and the last docs are very incomplete, any other source of information other than trial and error ?

[bkragl]

old(v) refers to the value of v at the beginning of the procedure (even before v := 0;). In your example this can be anything, because you do not have a precondition that talks about v. When Boogie checks the maintenance of the loop invariant, it could be that old(v) == 42 and v == 0 so the invariant holds, but after the loop body executes we have old(v) == 42 && v == 1 and the invariant does not hold anymore.

These are fundamental concepts, so you will find all the explanation you need in "This is Boogie 2".

[ghost]

Thanks for your answer. I had the impression that I could use old for referring the old value in a loop iteration, which I understand now I cannot. The paper only talks about procedures, is that right?

The modified example verifies correctly and (I think) it makes sense.

var v: int;

procedure main()
    requires v == 0;
    modifies v;
{

    while(true)
        invariant v > old(v) || v == 0;
    {
        v := v+1;
    }

}

[bkragl]

The paper only talks about procedures, is that right?

From the intro of the paper:

The paper describes the syntax, typechecking, and semantics of Boogie, as well as a rationale for its design and examples of how to encode proof obligations and assumptions in the language.

It certainly explains loop invariants and old expressions.

[ghost]

Sorry, I expressed it incorrectly. I was talking about the semantics of old(v) inside loop invariants. The semantics is the same, it refers to the old value of v before starting the procedure and not before the previous value of v in the iteration. Is there any way to refer to the previous value in the iteration?

[bkragl]

Is there any way to refer to the previous value in the iteration?

Nothing built-in. But you can introduce a fresh local variable that you assign at the beginning of the loop. However, note that you might need to assign some meaningful value to this variable also before the loop, since the loop invariant will also be interpreted before the loop starts.

[RustanLeino]

Note, also, that old only affects the interpretation of global variables. For a local variable x, old(x) is always just the same thing as x.

For loops, introducing a fresh variable and doing what @bkragl suggested is the way to go.