Well, as far as I understand it, the triggers come in when quantifiers are involved. So to prove an assertion with a universal quantifier, we need one or more arbitrary values (with particular properties) to instantiate the quantified variable and continue
the proof. In some sense I can think of the proof (at least as far as quantifiers are involved) as trying to make a chain of arbitrary values and matching triggers.
I think this is where that second to last assertion is involved: the way the array index is being calculated in your loop counter/invariant is not matching the trigger for the quantifier in your post condition. Putting in that assertion bridges the gap, matching
on the facts provided by the loop invariant on loop exit, and providing a fact that matches the post condition trigger.
By the way, there is some implicit quantification of the whole proof, we are trying to prove "for all initial states that satisfy the precondition, executing the procedure terminates in a state where the postcondition is satisfied" (total correctness).
But, other than the quantifiers, it is also the case that the verification is modular in some ways. There is procedural abstraction at method boundaries, Dafny doesn't look at the body of called procedures when trying to verify the calling procedure. It establishes
the pre-condition at the call site, and then assumes the post-condition. Something similar happens at a loop, the body of the loop is abstracted. Dafny proves the invariant at loop entry, and assumes the invariant (and the negation of the loop condition) at
loop exit. It modularly also verifies that the loop body maintains the loop invariant, in a similar way that it modularly verifies that called procedures do infact entail their post condition given their precondition.
So the proof of the
method doesn't involve the body of the
method. In fact, if you comment out the whole body (including the curly brackets) of the ms method, you can still verify
- the proof of
only uses the pre/post conditions of
not its body. You can do something similar with the loop bodies too.
If you comment out the body of the loops, the method
will still verify. Although you won't be able to compile and execute it until you fill the loop body in...
k := 0;
while (l+k <= u)
invariant 0 <= k <= u-l+1
invariant 0 <= l <= u < a.Length
invariant k <= buf.Length
invariant old(a).Length == a.Length;
invariant forall x :: 0 <= x < l ==> old(a[x]) == a[x];
invariant forall x :: l+k < x < a.Length ==> old(a[x]) == a[x];
invariant forall x :: u < x < a1.Length ==> a1[x] == a[x];
invariant forall x :: 0 <= x < k ==> a[l+x] == buf[x];
a[l + k] := buf[k];
k := k + 1;
Beyond that this all has to do with weakest precondition calculation, and Hoare Logic, if that points you in the right direction.
So, in short its is a bit triggers under the hood, but in your case its more about the way that Dafny goes about verifying loops and procedure calls.