Let's walk through why these assertions are failing and how to resolve them using Dafny's loop invariants—they're the key to helping the verifier track variable behavior across loop iterations.

Exercise 1a: Fixing the cnt > 0 Assertion #

The issue here is that Dafny's verifier can't automatically infer the relationship between idx and cnt as the loop runs, nor can it guarantee cnt ends up greater than 0. The decreases clause only proves the loop terminates—it doesn't provide any information about how variables change or relate to each other.

To fix this, we need to add loop invariants that explicitly state the relationships we know to be true before and after each loop iteration:

method exercise_1a(n: int) requires n > 0 {
    var idx := 0;
    var cnt := 0;
    while idx < n decreases n - idx 
        invariant idx == cnt  // idx and cnt are always equal
        invariant idx <= n    // idx never exceeds n
    {
        idx := idx + 1;
        cnt := cnt + 1;
    }
    assert idx > 0; // Now valid: idx equals n (which is >0)
    assert cnt > 0; // Now valid: cnt equals idx, so it's also >0
}

Why this works: #

• The idx == cnt invariant tells Dafny that these two variables are perfectly synchronized. So any conclusion we can draw about idx (like it equals n at loop exit) applies directly to cnt.
• The idx <= n invariant ensures we never go out of bounds, and since the loop exits when idx >= n, we know idx must equal n (since we start at 0 and increment by 1 each time). Given n > 0, both assertions hold.

Exercise 1b: Fixing Both Assertions #

In this version, adding a second decreases clause (for lexicographic termination) makes the verifier even more unsure about the loop's final state. The loop condition idx < n && cnt < n means the loop could exit if either condition fails—but without invariants, Dafny can't prove that either variable reached a value greater than 0.

We use similar invariants here to track the relationship between idx and cnt:

method exercise_1b(n: int) requires n > 0 {
    var idx := 0;
    var cnt := 0;
    while idx < n && cnt < n decreases n - idx, n - cnt 
        invariant idx == cnt  // idx and cnt remain equal through iterations
        invariant idx <= n
        invariant cnt <= n
    {
        idx := idx + 1;
        cnt := cnt + 1;
    }
    assert idx > 0; // Valid: idx equals n (>0)
    assert cnt > 0; // Valid: cnt equals idx, so it's also >0
}

Why this works: #

• Again, idx == cnt is critical. Since both variables increment together, the loop can only exit when both idx >= n and cnt >= n (if one hit n, the other would too).
• With n > 0, both variables end up equal to n, so both assertions are now valid.

内容的提问来源于stack exchange，提问作者Attila Karoly