Loop Invariant Annotations
Okay. So you were explaining that loops have multiple paths, but... you don't know how many?
Right! That's the big difference with loops, as I said. We can't predict ahead of time how many loops there will be, except in simple cases. But operation POs depend on being able to calculate the possible paths through the operation body.
So what do we do?
We make it the user's problem! :-)
You're kidding.
Well, a little yes, but we need more information from the user to be able to generate useful obligations for loops. Have you come across the idea of loop invariants before?
It sounds familiar... remind me?
A loop invariant is a bool predicate that is true before the loop, and at the start of each loop iteration, and at the end of each loop iteration, and after the loop completes.
But presumably it checks something useful?
Right. You could just say x + x = 2 * x or y or not y, but those wouldn't be useful. In general, we need to reason about the variables that the loop is modifying, to show how they relate to each other.
Hmmm... that sounds tricky. I mean, simple cases are easy but, in general, that's hard?
Yes, that's what I mean by us making it the user's problem, though it may be possible to automatically find loop invariants in future -- perhaps a new analysis plugin. For now though, you have to annotate your own loops.
Annotate?
An annotation is just a comment that you add to the specification before the loop, with a special syntax. In this case it's something like -- @LoopInvariant(a + b = c). The annotation has to be at the start of the comment like this, though it can be a block or line comment, and things can appear after the invariant in the same comment.
You'd better show me again, sorry...
No problem. Let's tweak our example to create a loop:
op: nat ==> ()
op(a) ==
(
dcl local : nat := 0;
sv := a;
while sv > 0 do
(
sv := sv - 1;
local := local + 1
)
);
That's a simple loop that counts down the sv variable from a, while incrementing the local variable. At the end, sv will be zero and local will be a.
Okay, that's simple. But where is the invariant?
So first, I want to show you what happens without the invariant. If we try to generate POs, it will generate loop obligations but tell us that the invariant is missing. Here's the first PO:
Proof Obligation 1: (Unproved)
check invariant before while condition
op: loop invariant obligation in 'DEFAULT' (test.vdm) at line 12:9
(forall a:nat, mk_Sigma(sv):Sigma &
(let local : nat = 0 in
(let sv : nat = a in
(-- Missing @LoopInvariant, assuming true at 12:9
(let $LoopInvariant : bool = true in
$LoopInvariant)))))
Notice that the comment says, "check invariant before while condition"? So this is saying that there ought to be a loop invariant and we need to check it's true before the loop. The context shows the creation of local and the setting of sv before the loop, but then it says, -- Missing @LoopInvariant, assuming true and it creates a $LoopInvariant placeholder, which is true.
Hmmm... so as it stands, that PO is trivially true?
Right. It's just there to encourage you to create a sensible invariant. It doesn't actually constrain the specification. If we give it to QuickCheck, it says:
> qc 1
PO #1, PROVABLE by trivial $LoopInvariant in 0.005s
>
So a real loop invariant would have to say that the two variables are going up and down in a predictable, related way?
Yes. In fact, if we add the local and sv variables together, the result is always the starting value, a. This is a common pattern in loop invariants that process one variable "into" another in some way. So let's add that as an annotation and see how the obligation changes:
-- @LoopInvariant(sv + local = a)
while sv > 0 do
(
...
Proof Obligation 1: (Unproved)
check invariant before while condition
op: loop invariant obligation in 'DEFAULT' (test.vdm) at line 12:38
(forall a:nat, mk_Sigma(sv):Sigma &
(let local : nat = 0 in
(let sv : nat = a in
((sv + local) = a))))
So notice now that the warning comment has gone, and the obligation checks that sv + local = a before the loop.
That's quite neat. But what if I wanted to add normal comments in the spec around that loop too. Would those interfere with the invariant annotation?
The only limitation is that annotations must appear at the start of a comment of their own, so only whitespace between the -- or /* and the @ of the annotation. You can add comments before or after the annotation comment, and even after the annotation itself, like this:
-- Comments before are fine
-- @LoopInvariant(sv + local = a) and here is fine
-- After is fine too
while sv > 0 do
...
-- But this annotation would be ignored, @LoopInvariant(sv + local = a)
-- because it's not at the start of a comment.
while sv > 0 do
...
Okay, thanks. And that invariant obligation we generated seems pretty easily provable?
Agreed, though QuickCheck finds it difficult to disprove because it doesn't work symbolically and there are an infinite number of natural numbers for it to consider. So it gives a MAYBE result.
Disppointing. But I guess this obligation looks provable anyway. Presumably there are other POs for other points in the loop, in this case?
Very good! Yes, let's look at them all:
> pog
Generated 4 proof obligations:
Proof Obligation 1: (Unproved)
check invariant before while condition
op: loop invariant obligation in 'DEFAULT' (test.vdm) at line 12:38
(forall a:nat, mk_Sigma(sv):Sigma &
(let local : nat = 0 in
(let sv : nat = a in
((sv + local) = a))))
Proof Obligation 2: (Unproved)
check invariant before first while body
op: loop invariant obligation in 'DEFAULT' (test.vdm) at line 14:9
(forall a:nat, mk_Sigma(sv):Sigma &
(let local : nat = 0 in
(let sv : nat = a in
((sv > 0) =>
((sv + local) = a)))))
Proof Obligation 3: (Unproved)
op: subtype obligation in 'DEFAULT' (test.vdm) at line 15:22
(forall a:nat, mk_Sigma(sv):Sigma &
(let local : nat = 0 in
(let sv : nat = a in
((sv > 0) =>
(forall local:nat, sv:nat &
(((sv + local) = a) and (sv > 0) =>
(sv - 1) >= 0))))))
Proof Obligation 4: (Unproved)
check invariant preserved by while body
op: loop invariant obligation in 'DEFAULT' (test.vdm) at line 14:9
(forall a:nat, mk_Sigma(sv):Sigma &
(let local : nat = 0 in
(let sv : nat = a in
((sv > 0) =>
(forall local:nat, sv:nat &
(((sv + local) = a) and (sv > 0) =>
(let sv : nat = (sv - 1) in
(let local : nat = (local + 1) in
((sv + local) = a)))))))))
So you'll notice these are similar to each other. We've looked at PO #1. But PO #2 is for the start of the first while loop iteration. Notice that it includes a sv > 0 => context, because that's the while-loop condition that must be true if the loop happens at all.
Got it. And PO#3 is a subtype obligation to make sure the decrement of the sv value is a nat. But that includes context that says forall local:nat, sv:nat & ((sv + local) = a) and (sv > 0) =>. What's that about?
Well spotted! So that's saying that in an arbitrary loop iteration, all we know is that for all the possible values of local and sv, the loop invariant must hold and the while condition must have passed too. So that's the basis that we have for trying to show that the sv decrement is legal.
This is strange. You mean we don't know the exact values of the loop modified variables?
That's right. We know the general case, as given to us by the invariant. But we don't know precisely what the state is for any given loop iteration. There is some ambiguity here, but the forall <changes> and invariant mean that we are covering all loop cases, assuming the invariant is sensible and reasons about the variables that are updated in the loop. In effect, we're reasoning about all of the loop iterations at the same time.
Hmmm, okay. So then PO#4 says it's a check that the invariant is preserved by the loop body. So that takes the situation at the start, modifies it according to the body, and then asserts that the invariant must still hold?
Exactly. So you can see this is an inductive proof pattern? We create a PO for the initial loop entry, then show that if the invariant holds at the start, then it holds at the end. That means it holds for the start of the next loop too, and so on for any number of loops.
Ah! Yes, I thought that pattern was familiar. Why isn't there an obligation for the point after the loop?
The problem is that the context for that obligation would have to use the invariant to constrain the possible values after the loop, along with the fact that the while-condition is false. Then, the base obligation would verify that the invariant is met. Well of course it will be, because that's the context for this position in the specification! So actually, there is no point in producing this obligation, as it is trivially true. It looks like this:
...
(forall local:nat, sv:nat &
(((sv + local) = a) and (not (sv > 0)) => -- Note the "not" because the loop has ended
(sv + local) = a))))) -- Trivially true
But if we cause another obligation in statements after the loop, you would see the context above. So the check after the loop is implicit in what follows it.
Okay, so what does QuickCheck make of these POs?
Let's try:
> qc
PO #1, MAYBE in 0.002s
PO #2, MAYBE in 0.003s
PO #3, MAYBE in 0.284s
PO #4, MAYBE in 0.238s
>
That may be a bit disappointing. But remember, this invariant is correct (I assert, without proof!), so QuickCheck won't find any counterexamples. It says MAYBE because it hasn't tried all possible natural numbers -- it can't.
Could we try deliberately breaking the invariant?
LOL, I like the way you think! Yes, of course, let's try:
-- @LoopInvariant(sv * local = a) -- NOTE! CHANGED "+" to "*" !!
> qc
PO #1, FAILED in 0.023s
Counterexample:
op: loop invariant obligation in 'DEFAULT' (test.vdm) at line 12:38
(forall a:nat, mk_Sigma(sv):Sigma &
--> sv = 0, a = 1
(let local : nat = 0 in
(let sv : nat = a in
((sv * local) = a))))
--> returns false
PO #2, FAILED in 0.002s
Counterexample:
op: loop invariant obligation in 'DEFAULT' (test.vdm) at line 14:9
(forall a:nat, mk_Sigma(sv):Sigma &
--> sv = 0, a = 1
(let local : nat = 0 in
(let sv : nat = a in
((sv > 0) =>
((sv * local) = a)))))
--> returns false
PO #3, MAYBE in 0.726s
PO #4, FAILED in 0.004s
Counterexample:
op: loop invariant obligation in 'DEFAULT' (test.vdm) at line 14:9
(forall a:nat, mk_Sigma(sv):Sigma &
--> sv = 0, a = 1
(let local : nat = 0 in
--> local = 0
(let sv : nat = a in
--> sv = 1
((sv > 0) =>
(forall local:nat, sv:nat &
--> local = 1, sv = 1
(((sv * local) = a) and (sv > 0) =>
(let sv : nat = (sv - 1) in
(let local : nat = (local + 1) in
((sv * local) = a)))))))))
--> returns false
>
So now we have counterexamples, except the subtype one, which may still be correct (it has nothing to do with the invariant as such).
Right, I get the idea. So that's how we handle while-loops. Are the various for-loops the same?
Roughly, yes, but there are some differences. Let's tweak our example to be a for-index loop and see what happens:
-- @LoopInvariant(sv + local = a)
for x = 1 to a do
(
sv := sv - 1;
local := local + 1
)
> pog
Generated 3 proof obligations:
Proof Obligation 1: (Unproved)
check invariant before for-loop
op: loop invariant obligation in 'DEFAULT' (test.vdm) at line 13:38
(forall a:nat, mk_Sigma(sv):Sigma &
(let local : nat = 0 in
(let sv : nat = a in
((1 <= a) =>
(let x : nat1 = 1 in
((sv + local) = a))))))
Proof Obligation 2: (Unproved)
op: subtype obligation in 'DEFAULT' (test.vdm) at line 16:22
(forall a:nat, mk_Sigma(sv):Sigma &
(let local : nat = 0 in
(let sv : nat = a in
((1 <= a) =>
(forall x:nat1, local:nat, sv:nat &
(((x >= 1) and (x <= a)) and ((sv + local) = a) =>
(sv - 1) >= 0))))))
Proof Obligation 3: (Unproved)
invariant preservation for next for-loop
op: loop invariant obligation in 'DEFAULT' (test.vdm) at line 15:9
(forall a:nat, mk_Sigma(sv):Sigma &
(let local : nat = 0 in
(let sv : nat = a in
((1 <= a) =>
(forall x:nat1, local:nat, sv:nat &
(((x >= 1) and (x <= a)) and ((sv + local) = a) =>
(let sv : nat = (sv - 1) in
(let local : nat = (local + 1) in
(let x : nat1 = (x + 1) in
((sv + local) = a))))))))))
So you'll notice that this generates very similar obligations. PO#1 tests the invariant of the first loop value, when x = 1, PO#2 is a subtype as before, and PO#3 checks that if the loop index is valid and the invariant passes at the start of a loop, then the invariant is true for the x+1 value at the end of the loop, which is the start of the next loop.
What is that 1 <= a about?
That's just to make sure you actually enter the loop, like the sv > 0 check in the while loop. If you pass an a value of zero, the loop doesn't actually execute.
So there isn't really a PO before the loop, as with the while-loop? I mean, PO#1 is really the first loop case?
It makes more sense if you think of unwinding the for loop into a while loop. You would declare a loop variable dcl x:nat := 1; and then you would perform a while loop that runs while x <= a and increments x := x + 1 at the end. So the "before" case is before the while loop, which is when x=1. See?
Okay, and there were obligations after the loop, those would see the effect of the loop in their context, presumably, as with while loops?
That's right. Let's try adding let z = 1/sv in skip after the loop. That does nothing, but lets us see what is in the context at that point:
Proof Obligation 4: (Unproved)
op: non-zero obligation in 'DEFAULT' (test.vdm) at line 20:18
(forall a:nat, mk_Sigma(sv):Sigma &
(let local : nat = 0 in
(let sv : nat = a in
((1 <= a) =>
(forall local:nat, sv:nat &
(let x : nat1 = (a + 1) in
(((sv + local) = a) =>
sv <> 0)))))))
Proof Obligation 5: (Unproved)
op: non-zero obligation in 'DEFAULT' (test.vdm) at line 79:18
(forall a:nat1, mk_Sigma(sv):Sigma &
(let local : nat = 0 in
(let sv : nat = a in
((1 > a) =>
(-- Did not enter loop at 13:9
(((local + sv) = a) =>
sv <> 0))))))
So you can see that the first extra POs include the invariant, but the x value is one beyond the end, because the loop has terminated.
And why are there two extra POs, not just one? They look the very similar?
If you look closely, you'll see that the second one has a different 1 > a test? That means "if the loop is not entered", and you see the comment too. So in that case, we know that the loop had no effect. So we don't have the forall <changes>. The path just drops straight to the sv <> 0 test, though the invariant still holds, because it held before the loop.
Got it! So does that cover for-loops?
Just one more thing. With for-set and for-seq loops, you can include a "ghost variable" in the invariant.
Sounds spooky!
Ha! The point is, if you say, for all x in set {1, 2, 3} do ..., what order will the loop execute in?
Oh. I've never thought about that. Sets don't have a defined order, so I'm not sure.
Right, this isn't defined. So for-set loops have to be slightly different to cover all the possibilities. Let's tweak the example yet again:
-- @LoopInvariant(sv + local = a)
for all x in set {1, ..., a} do
...
> pog
Generated 3 proof obligations:
Proof Obligation 1: (Unproved)
check invariant before for-loop
op: loop invariant obligation in 'DEFAULT' (test.vdm) at line 12:38
(forall a:nat, mk_Sigma(sv):Sigma &
(let local : nat = 0 in
(let sv : nat = a in
(let DONE_13$ : set of nat1 = {} in
((sv + local) = a)))))
Proof Obligation 2: (Unproved)
op: subtype obligation in 'DEFAULT' (test.vdm) at line 15:22
(forall a:nat, mk_Sigma(sv):Sigma &
(let local : nat = 0 in
(let sv : nat = a in
(({1, ..., a} <> {}) =>
(forall x:nat1, local:nat, sv:nat, DONE_13$:set of nat1 &
(((DONE_13$ psubset {1, ..., a}) and (x in set ({1, ..., a} \ DONE_13$))) and ((sv + local) = a) =>
(sv - 1) >= 0))))))
Proof Obligation 3: (Unproved)
invariant preservation for next for-loop
op: loop invariant obligation in 'DEFAULT' (test.vdm) at line 14:9
(forall a:nat, mk_Sigma(sv):Sigma &
(let local : nat = 0 in
(let sv : nat = a in
(({1, ..., a} <> {}) =>
(forall x:nat1, local:nat, sv:nat, DONE_13$:set of nat1 &
(((DONE_13$ psubset {1, ..., a}) and (x in set ({1, ..., a} \ DONE_13$))) and ((sv + local) = a) =>
(let sv : nat = (sv - 1) in
(let local : nat = (local + 1) in
(let DONE_13$ : set of nat1 = (DONE_13$ union {x}) in
((sv + local) = a))))))))))
So you'll see there is a variable called DONE_13$ being used? It starts as the empty set, and then accumulates values as each member of the loop set is chosen. That variable is in scope for the invariant, so it can reason about "what has been done so far". And finally, of course, after the loop the DONE_13$ value is the complete set, here {1, ..., a}.
So... is that variable real? I mean, is it something that actually has a value during a simulation?
Yes and no. It's a ghost, which means it only exists for internal purposes. But the interpreter does add the variable to the runtime environment when it is evaluating loops with invariants. So if you step through, perhaps trying to debug your invariant, you can see the DONE_13$ value. But you can't just use it in your spec, like other variables. You can use it in the invariant though, meaning "the cases done so far". So you might see something like -- @LoopInvariant(total = sum(DONE_13$)), assuming total should always be the sum of the cases so far.
Why the 13 on the end? Is that just a random thing?
It just means the loop it relates to starts on line 13. So if you have nested loops, the variables are distinct. But you can change the name of the ghost for any loop by adding an extra argument, like -- @LoopInvariant(total = sum(SO_FAR), SO_FAR). If you have an invariant that reasons about the ghost, it's sensible to rename it because the "_13$" line number may change as you edit the spec!
Okay. You mentioned the runtime environment. Does that mean loop invariants are checked at runtime?
Yes. In fact if you single-step a loop execution, you will occasionally see control flick up to the -- @LoopInvariant comment when the value is being checked. Now that you know how these work though, you should understand what's happening. You can even put a breakpoint on the invariant annotation itself, if that helps. But remember it's not a function call, so control jumps to the invariant annotation and back again as you step through the loop. Here's a screenshot of a loop invariant failure in VSCode:
I think all this is driving me loopy!
That would be understandable. It's quite a bit more complicated than the obligation work we've done with functions. But it is rational, and it does allow us to find problems with many more specifications than before this was added.
Okay. Dare I ask if there is more to know?
Well, just to say that for-seq loops are basically the same idea as for-set loops, but with ghost sequences. Try it for yourself sometime.
I will. Anything else?
One last annotation to mention... @LoopMeasure
Does this have anything to do with recursive measures, as with functions?
It's related, but this isn't about recursion. It's about loop termination, specifically while-loop termination.
You don't bother with for-loops?
Their termination is guaranteed, because they work out their loop parameters once at the start, and iterate over a fixed range.
Ah yes, of course. But while-loops are different?
Yes, they can loop forever in principle. So if you don't want that to happen, you can define a @LoopMeasure which is an expression whose value should be a natural number that decreases towards zero. In the literature these are sometimes called "loop variants".
Just like function measures.
Yes, it's a similar idea, but here used to prove termination of a loop rather than termination of a recursive function invocation. So in our original while-loop example, the variable sv would be a valid measure of the loop, because it decreases with each loop iteration, stopping at zero. But in general a measure can be an arbitrary expression, and can call helper functions.
So what happens if we add that @LoopMeasure annotation?
You get a new proof obligation of course! Let's try:
-- @LoopInvariant(sv + local = a)
-- @LoopMeasure(sv)
while sv > 0 do
(
...
Proof Obligation 1: (Unproved)
check measure after each while body
op: loop invariant obligation in 'DEFAULT' (test.vdm) at line 15:9
(forall a:nat, mk_Sigma(sv):Sigma &
(let local : nat = 0 in
(let sv : nat = a in
(forall local:nat, sv:nat &
(((sv + local) = a) and (sv > 0) =>
(let LOOP_14$ : nat = sv in --- set here
(let sv : nat = (sv - 1) in
(let local : nat = (local + 1) in
sv < LOOP_14$)))))))) --- checked here
So note that this is saying that for every loop iteration, if we pick up sv and call it LOOP_14$ at the start, we can check sv again at the end and it will be less than the saved value.
So that 14 is just the line number again?
Yes, the while loop is now on line 14. Without this we would need some way to invent a unique name that doesn't clash with those already declared. As with @LoopInvariant, you can pass a second argument with a specific measure variable name if you wish.
Okay. And is this checked by the runtime as well? I mean, that LOOP_14$ is another ghost, isn't it?
Yes, it's ghostly, so you can't refer to that variable directly. But you can see the value in the runtime environment as you step through and the decrease is checked at runtime. If we add a breakpoint during a measure, it looks like this in VSCode:
Cool. Is there more?
No, that's everything. Hope that didn't drive you too loopy :-)