YAML-based format: Rename loop_invariant entry?

[michael-schwarz]

In a discussion between some Munich Goblint folks and @MartinSpiessl and others from the CPAChecker team on Friday we were wondering whether loop_invariant is actually the right name for the entry as it is currently specified:

• There is nothing specific about loops to the loop_invariant entry - one could just as well provide invariants for locations / program points that are not in loops
• In the example in the repository, it already seems to be used independent of loops:

  loop_invariant: 
    string: (x >= 1024U) && (x <= 4294967295U) && (y == x)
    type: assertion
    format: C

Calling this assertion the loop invariant is a bit strange as it does not hold inside the loop, but only after the loop.

Maybe just invariant or location_invariant is a better name?

[michael-schwarz]

There is some overlap of this suggestion with #59 which proposes adding such a location_invariant on top of the current loop_invariant entry.

[sim642]

There's another problem regarding loop_invariant and its positioning in the code that got discussed during some SV-COMP community meeting a while ago AFAIK, but I don't recall any solution.
Namely, a loop invariant isn't an invariant that can be inserted into the specified code location as an assertion at a single point (which is how I remember its semantics being defined somewhere, if I'm not mistaken). Rather, that invariant expression should actually hold at four different code locations:

1. before the loop,
2. in the beginning of the loop body,
3. at the end of the loop body,
4. after the loop.

So a loop invariant is stronger than an assertion inserted into any single of the four possible locations.

[MartinSpiessl]

There is some overlap of this suggestion with #59 which proposes adding such a location_invariant on top of the current loop_invariant entry.

Indeed, I forgot that I already tasked Sven with this before hand!

So a loop invariant is stronger than an assertion inserted into any single of the four possible locations.

Indeed, this is the usual semantics.There are also some pecularities regarding special cases when variables go out of scope after the loop (i.e., the C expression is not valid "after" the loop). This is not a problem for the witness automata from the graphml-based format, but when one tries to translate these into concrete locations then there might be no specific location to put 4. to. As such an loop_invariant cannot simple be replaced by 4 location_invariants.