Ambiguously associating loop invariant

[ArmborstL]

The following C code has a nested loop:

int main() {
    int i;
    //@ loop_invariant true;
    while(i<10)
        //@ loop_invariant i<10;
        while(1==1) {
            i = 1;
        }
    return 0;
}

VerCors determines that the invariant i<10 above the inner loop cannot be established, even though it is the condition of the outer loop.
This is due to the fact that the outer loop only contains the inner loop, and thus omitted the curly braces around its body. Therefore, the invariant of the inner loop could also be interpreted as belonging to the outer loop, using the syntax while(cond) /*@contract*/ {body}. VerCors indeed uses this interpretation, and correctly determines that the invariant cannot be established for the outer loop.
I think it's clear in this case that the invariant was meant for the inner loop: The indentation gives a clear hint, the outer loop already has a contract above, and the inner loop does not have a contract except for the ambiguous one.

There are different viewpoints on this issue:

1. loops without curly braces are bad style. Use braces, and you don't have a problem. No change to VerCors.
2. change VerCors to disallow the syntax while(cond) /*@contract*/ {body}. In the vast majority of cases we place the contract above the loop header anyway, so let's just get rid of the other option and remove any ambiguity.
3. Be smart and detect this case: IF the outer loop only contains one statement AND that statement is another loop AND the outer loop already has a contract above AND ... THEN (and only then) the invariant is actually meant for the inner loop.
4. Bob's suggestion, a mix of the previous two: only allow the syntax while(cond) /*@contract*/ {body} if there are curly braces around the body. If there are no curly braces, the invariant goes to the inner loop (if there is one, error if not).
5. Another combination of 2 and 3: Any loop can only use one style; either having a contract before or within, not both.

What do people think? Which viewpoint do you prefer?

[bobismijnnaam]

Re 5: that would still be ambiguous right? E.g.:

while(true)
//@ loop_invariant true;
while(true) assert true;

2 also sounds nice from a perspective of simplification and preventing easy mistakes. Otherwise my preference would be 4 or 5.

[ArmborstL]

Indeed, 5 would not get rid of the ambiguity if you have annotated only some of the loops.

[pieter-bos]

Just for reference:

• OpenJML: "a <loop-specification> may only appear immediately prior to a Java loop statement";
• FramaC: only directly before the loop, implied via the grammar;
• Viper: between the condition and the opening curly brace

[ArmborstL]

I assume the openJML one was meant to be "a loop invariant may"? Or a what?

[pieter-bos]

You can apparently .

[ArmborstL]

Interesting. Thanks for clearing it up 👍

[pieter-bos]

I think I slightly prefer only before the loop, i.e. (2). It also makes sense in the context of how side-effectful conditions are now encoded: they are executed after the invariant is established.