A loop runs its body again and again, and a verifier cannot replay every pass. It only knows what you tell it stays true. In this loop, the only thing Dafny is told is that i stays in range. After the loop it has nothing connecting sum to the array, so it cannot prove the result.
while i < a.Length
invariant 0 <= i <= a.Length
{
sum := sum + a[i];
i := i + 1;
}The postcondition could not be proved after the loop.
Needed
sum == Sum(a[..])
The bound is true on every pass and keeps the index in range. It does not say what sum means.
Illustrative, not copied verifier output.
The working definition
What is a loop invariant?
A loop invariant is a statement about the program that is true every time control reaches the top of a loop: before the first pass, and after each pass.
Think of dropping coins into a jar one at a time. After every coin you can say: the jar holds the total of the coins counted so far. That sentence is true before the first coin (empty jar, total zero). It stays true after each coin. When the coins run out, it is the total of all of them. That sentence is the invariant.
When the loop ends, the invariant combines with the exit condition to give the result. The invariant is not the final answer by itself. It connects what the loop has done so far to what is left.
The Dafny guide describes invariants as specifications that must hold before and after each loop iteration.
Safety
0 <= i <= a.Length
Keeps the index in range, so a[i] never reads past the end.
Correctness
sum == Sum(a[..i])
Says what sum holds: the total of the elements already processed.
Verifier walkthrough
Choose the missing invariant
The method should return the sum of every element of a. To read the code: Sum(s) is a helper that adds up a whole list, a[..i] means the first i elements of a, and a[..] means all of them. Look at the gap in the loop and compare two ways to fill it. This program is an illustration. It is not one of the graded exercises.
function Sum(s: seq<int>): int
{
if |s| == 0 then 0
else Sum(s[..|s|-1]) + s[|s|-1]
}
method SumArray(a: array<int>) returns (sum: int)
ensures sum == Sum(a[..])
{
sum := 0;
var i := 0;
while i < a.Length
invariant 0 <= i <= a.Length
// <- the missing invariant goes here
{
sum := sum + a[i];
i := i + 1;
}
}Option A
invariant sum >= 0
Sounds sensible, but it is not true for every array. If a is [-5], sum becomes -5 after the first pass and the claim breaks. Even where it holds, it never says what sum equals, so the postcondition still cannot be proved.
Option B
invariant sum == Sum(a[..i])
The part already processed always explains the current total. Together with the exit condition, that is the postcondition.
This comparison explains the proof state. A real Dafny run may ask for small helper assertions about slices, which do not change the idea. The course uses Dafny to grade exercises.
The proof
Three checks, one invariant
A loop invariant works only when the proof has a beginning, survives the body, and becomes useful when the loop ends. Each check is something the verifier must prove. These are called proof obligations.
01
Initialization
Before the first pass, i is 0 and sum is 0. The processed prefix is empty, so Sum(a[..0]) is 0. The invariant starts out true.
sum == Sum(a[..i]) == Sum(a[..0]) == 0
02
Maintenance
Assume the invariant at the top of a pass. Adding a[i] extends the total by one element. Increasing i makes the same relationship true for the next pass.
Sum(a[..i]) + a[i] == Sum(a[..i+1])
03
On exit
When the loop stops, the loop condition is false, so i >= a.Length. The bound invariant says i <= a.Length. Together, i == a.Length. Substituting that into the invariant gives the promised result. Textbooks call this step termination.
sum == Sum(a[..i]) == Sum(a[..a.Length]) == Sum(a[..])
Whether the loop ever stops is a separate question. Dafny can often guess a measure that shrinks on its own. Here, that is a.Length - i. Unit 5 covers it.
A repeatable method
How to find a loop invariant
Start from the postcondition, then ask what version of that statement can be true before the loop has finished. Each step below shows what it looks like for the sum.
01
Name the progress variable
Find the variable that measures how far the loop has got.
i counts how many elements have been added.
02
Describe the completed part
Rewrite the postcondition so it talks only about the part already processed.
sum == Sum(a[..i])
03
Add the safety bounds
State the range the progress variable stays in, so every access is valid.
0 <= i <= a.Length
04
Check initialization
Plug in the values that exist before the first pass.
i == 0, sum == 0, and Sum(a[..0]) == 0
05
Check one pass
Assume the invariant, run the body on symbols, and confirm it holds again.
Sum(a[..i]) + a[i] == Sum(a[..i+1])
06
Use the exit condition
Combine the invariant with the stopped loop. The postcondition should follow.
i == a.Length, so Sum(a[..i]) == Sum(a[..])
Transfer the idea
Selection sort
After the first i positions have been filled, the prefix is sorted and every value in it is no greater than every value in the remaining suffix.
Roadmap
Binary search
The target, if it exists, remains inside the current search interval. Each branch proves the discarded half cannot contain it.
Unit 5 · An index that cannot go out of rangeA strong invariant is specific enough to prove the result and weak enough to stay true throughout the loop.
Debug the proof
Common loop invariant mistakes
01The statement is true but too weak
0 <= i <= a.Length is true on every pass and keeps the index safe. It says nothing about what sum holds, so it cannot prove the result. Bounds and correctness invariants usually work together.
02The invariant only restates the loop condition
The condition decides whether another pass runs. The invariant must still be true when the loop exits. i < a.Length is false at exit, so it cannot be an invariant here.
03The final postcondition is used too early
sum == Sum(a[..]) is usually false in the middle of the loop. After two passes, sum covers only two elements. Generalize it around the progress variable instead.
04Initialization is skipped
If the code before the loop does not make the invariant true, it is not an invariant for that loop. Starting sum at 1 would break sum == Sum(a[..i]) before the first pass.
05The invariant is not true for every allowed input
sum >= 0 looks sensible, but it is false for some arrays with negative numbers, such as [-5]. A few friendly arrays can build intuition. The invariant still has to survive every state the method's preconditions allow.
Frequently asked
Loop invariant questions
What is a loop invariant in simple terms?
It is a fact that is true each time the loop comes back to the top. It summarizes what the loop has done so far, so you do not have to replay every earlier pass.
Why are loop invariants useful?
They help prove that a loop is safe and that it produces the promised result. They also expose missing assumptions and unclear relationships between variables before those problems turn into bugs.
How do you prove a loop invariant?
Check three things. It is true before the first pass (initialization). If it is true at the top of a pass, it is still true at the top of the next one (maintenance). When the loop stops, it combines with the exit condition to give the postcondition (on exit).
What is the difference between an invariant and a postcondition?
A postcondition is what must be true after the method finishes. An invariant is what is true at the top of every pass through the loop. When the loop ends, the invariant plus the exit condition gives you the postcondition.
Is the loop condition an invariant?
Not usually. The loop condition is true when a pass starts and false when the loop exits. An invariant must be true both times.
Can a loop have more than one invariant?
Yes. A loop often needs one invariant for the bounds of its variables and another that connects its current state to the final result.
Does an invariant prove the specification is correct?
No. It helps prove that the code meets the specification you wrote. The result is still relative to that specification and the assumptions you gave the verifier.