CODEWITHSUNDEEP
boogie
depechec0de
depechec0de

Reputation: 131

Invariants and old() in Boogie

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 ?

Upvotes: 0

Views: 57

Answers (1)

depechec0de
depechec0de

Reputation: 131

I received an answer from @bkragl here: https://github.com/boogie-org/boogie/discussions/344

Basically old(v) refers to the procedure previous value of v and not the one in the previous iteration of the loop.

The correct code looks like this:

var v: int;

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

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

}

Upvotes: 0

Related Questions