9 Loop Invariants

In Floyd Hoare Logic, we studied the Hoare Triple rules for assignments and conditionals. In this lecture, we will extend that discussion to the Hoare Triple rules for loops.

9.1 While Loops🔗

The Hoare rule for while loops is based on the idea of an invariant: an assertion whose truth is guaranteed before and after executing a statement. An assertion P is an invariant of s if


      {P} s {P}

holds. Note that in the middle of executing s, the invariant might temporarily become false, but by the end of s, it must be restored.

As a first attempt at a [while] rule, we could try:


            {P} s {P}
      ---------------------
      {P} while b { s } {P}

That rule is valid: if P is an invariant of s, as the premise requires, then no matter how many times the loop body executes, s is going to be true when the loop finally finishes.

But the rule also omits two crucial pieces of information. First, the loop terminates when b becomes false. So we can strengthen the postcondition in the conclusion:


              {P} s {P}
      ---------------------------
      {P} while b { s } {P && !b}

Second, the loop body will be executed only if b is true. So we can also strengthen the precondition in the premise:


            {P && b} s {P}
      --------------------------- (Hoare While)
      {P} while b { s } {P && !b}

That is the Hoare While rule. Note how it combines aspects of empty blocks and conditionals:

If the loop body executes zero times, the rule is like an empty block in that the precondition survives to become (part of) the postcondition.
Like a conditional, we can assume guard b holds on entry to the substatement

If we summarize, a loop invariant is a logical condition (a Boolean expression) that must be:

True before the loop starts
True after each iteration of the loop
Helps prove that the loop works correctly

Unlike most programming languages, Dafny requires formal verification that your loops behave correctly. Since loops may run many times, Dafny cannot rely on checking just a single iteration. Instead, it needs a logical guarantee that the loop preserves correctness at every step and will eventually terminate. This is achieved using two key elements: loop invariants, which express conditions that must remain true throughout the loop, and a termination metric (typically specified with a decreases clause) to prove that the loop will not run forever. In Dafny, loop invariants are written using the invariant keyword within the while loop.

Let’s look at examples of loops with no bodies. We ignore Dafny’s complaints that loops have no bodies.

There are two general patterns:

To enter the loop, we must show that the chosen invariant holds.
Exiting the loop, we may assume that the chosen invariant holds and the loop test failed.

Dafny

method Loop1()
{
  var x: int;

  assume x % 2 == 0;
  while x < 300
    invariant x % 2 == 0
  {
  }
  assert !(x < 300) && x % 2 == 0;
}

You can apply the same recipe step by step for the following code:

Dafny

method Loop2()
{
  var x: int;
  assume 0 <= x <= 100;
  while x % 2 == 1
    invariant 0 <= x <= 100
  {
  }
  assert !(x % 2 == 1) && 0 <= x <= 100;
}

Now that we chose a specific initial value, we can prove the loop-entry condition, rather than assuming it.

Dafny

method Loop3()
{
  var x: int := 2;
  assert x % 2 == 0;
  while x < 50
    invariant x % 2 == 0
  {
  }
  assert !(x < 50) && x % 2 == 0;
}

In the example below, we cannot prove x == 19; as the postcondition, because it does not logically follow from the preceding statement.

Dafny

method Loop4()
{
  var x: int := 0;

  assert 0 <= x <= 20;
  while x % 2 == 0
    invariant 0 <= x <= 20
  {
  }
  assert !(x % 2 == 0) && 0 <= x <= 20;
  assert x == 19; //oops

}

In the example below, the conclusion holds regardless of the chosen invariant, because it is simply the negation of the loop condition. When the loop terminates, i == 100 must be true.

Dafny

method Loop5()
{
  var i: int := 0;

  while i != 100
    invariant 0 <= i <= 100
  {
  }
  assert i == 100;

}

In the example below, the invariant and loop test both matter, to imply the assertion. invariant true (0 <= i <= 10) would be insufficient to prove i == 10

Dafny

method Loop6()
{
  var i: int := 0;

  while i < 10
    invariant 0 <= i <= 10
  {
      //what if we have i := i + 3;
  }
  assert i == 10;
}

Loop invariants become more interesting when they relate multiple variables. Do you see why the assertion 200 <= y is true?

Dafny

method Loop7()
{
  var x, y := 0, 0;

  while x < 300
    invariant 2 * x == 3 * y
  {
  }
  assert 200 <= y;
}

Now that we’ve covered enough of the basics, let’s consider a simple loop that terminates when x ≤ 0.

Dafny

method LoopToZero_1(m : int, p : int) returns (x: int, z: int) {
  x := m;
  z := p;
  while x > 0 {
    z := z - 1;
    x := x - 1;
  }
}

Here is one possible specification for this program, in the form of a Hoare triple:

Dafny

assert true;
x := m;
z := p;
while x > 0 {
  z := z - 1;
  x := x - 1;
}
assert z == p - m;

and here is the equivalent specification in terms of Dafny’s requires and ensures syntax:

Note: of course, Dafny can’t prove this without an invariant annotation

Dafny

method LoopToZero_2(m : nat, p : int) returns (x: nat, z: int)
  requires true
  ensures z == p - m
{
  x := m;
  z := p;
  while x > 0
    invariant (z - x == p - m)
  {
    z := z - 1;
    x := x - 1;
  }
}

Here is an annotated version of this program, embodying a proof of this specification:

Dafny

method LoopToZero_3(m : nat, p : int) returns (x: nat, z: int) {
  x := m;
  assert  x == m;
  z := p;
  assert x == m && z == p; // ->
  assert  z - x == p - m;
  while x > 0
    invariant  z - x == p - m
  {
    assert z - x == p - m && x > 0;  // ->
    assert (z - 1) - (x - 1) == p - m;
    z := z - 1;
    assert z - (x - 1) == p - m;
    x := x - 1;
    assert z - x == p - m;
  }
  assert z - x == p - m && !(x > 0) ==>
      z == p - m;
}

That is, an annotated program consists of the program’s text interleaved with assertions (sometimes multiple assertions separated by implications).

An annotated program can be viewed as a compact representation of a proof in Hoare Logic: the assertions surrounding each command specify the Hoare triple to be proved for that part of the program using one of the Hoare Logic rules, and the structure of the program itself shows how to assemble all these individual steps into a proof for the whole program.

Dafny’s goal is to verify such annotated programs "mostly automatically." But, before we can verify anything, we need to be able to find a proof for a given specification, and for this we need to discover the right assertions. This can be done in an almost mechanical way, with the exception of finding loop invariants. We’ll first explain in detail how to construct annotations for several short programs, all of which are loop-free or have simple loop invariants. We’ll return to finding more interesting loop invariants later.

9.1.1 Reduce to Zero🔗

Here is a while loop that is so simple that true suffices as a loop invariant when x is a nat - that is, Dafny doesn’t even need an invariant annotation to verify it (why?)

Dafny

method LoopToZero_Simple(n : nat) returns (x : nat)
  ensures x == 0
{
  x := n;
  while x > 0
    invariant true
  {
    x := x - 1;
  }
}

Here is it’s annotated version:

Dafny

(1)    {true}
         while x > 0 {
(2)       { true && x > 0 } ->
(3)       { true }
           x := x - 1
(4)       { true }
         }
(5)    { true && !(x > 0) } ->
(6)    { x = 0 }

The annotations can be constructed as follows:

Start with the outer precondition (1) and postcondition (6).
Following the format dictated by the [Hoare While] rule, we copy (1) to (4). We conjoin (1) with the guard to obtain (2). We also conjoin (1) with the negation of the guard to obtain (5).
Because the final postcondition (6) does not syntactically match (5), we add an implication between them.
Using the assignment rule with assertion (4), we trivially substitute and obtain assertion (3).
We add the implication between (2) and (3).

Finally we check that the implications do hold; both are trivial.

9.1.2 Division🔗

Let’s do one more example of simple reasoning about a loop.

The following program calculates the integer quotient and remainder of parameters m and n. (Dafny complains about the invariant and the loop’s termination. How would you fix the latter?)

Dafny

method QuotDiv (m : int, n : int) returns (x : int, y : int)
{
       x := m;
       y := 0;
       while n <= x
       {
         x := x - n;
         y := y + 1;
       }
}

If we execute this program, it will terminate with the variable x set to the remainder when m is divided by n and y set to the quotient.

In order to give a specification to this program we need to remember that dividing m by n produces a remainder x and a quotient y such that n * y + x == m && x < n.

It turns out that we get lucky with this program and don’t have to think very hard about the loop invariant: the invariant is just the first conjunct, [n * y + x == m], and we can use this to annotate the program.

Dafny

 (1)  { true } ->
 (2)  { n * 0 + m == m }
        x := m;
 (3)  { n * 0 + x == m }
        y := 0;
 (4)  { n * y + x == m }
        while n <= x {
 (5)  { n * y + x == m && n <= x } ->
 (6)  { n * (y + 1) + (x - n) == m }
          x := x - n;
 (7)  { n * (y + 1) + x == m }
          y := y + 1;
 (8)  { n * y + x == m }
        }
 (9)  { n * y + x == m && !(n <= x) } ->
(10)  { n * y + x == m && x < n }

Assertions (4), (5), (8), and (9) are derived mechanically from the invariant and the loop’s guard. Assertions (8), (7), and (6) are derived using the assignment rule going backwards from (8) to (6). Assertions (4), (3), and (2) are again backwards applications of the assignment rule.

Now that we’ve annotated the program it only remains to check that the uses of the consequence rule are correct – i.e., that (1) implies (2), that (5) implies (6), and that (9) implies (10). This is indeed the case:

(1) -> (2): trivial, by algebra.
(5) -> (6): because [n <= x], we are guaranteed that the subtraction in (6) does not get zero-truncated. We can therefore rewrite (6) as [n * y + n + x - n] and cancel the ns, which results in the left conjunct of (5).
(9) -> (10): if [!(n <= x)] then [x < n]. That’s straightforward from high-school algebra.

Here is the fully annotated Dafny program:

Dafny

method QuotDiv' (m : int, n : int) returns (x : int, y : int)
  requires n > 0
  ensures n > x
  ensures y * n + x == m
{
  x := m;
  y := 0;
  assert y * n + x   == m;
  while n <= x
    invariant y * n + x   == m
  {
    assert n <= x && y * n + x   == m ==> y * n + x   == m;
    assert (y+1) * n + (x-n) == m;
    x := x - n;
    assert (y+1) * n + x == m;
    y := y + 1;
    assert  y * n + x == m;
  }
  assert !(n <= x) && y * n + x   == m ==>  n > x &&  y * n + x == m;
}

9.2 Finding Loop Invariants🔗

Once the outermost precondition and postcondition are chosen, the only creative part of a verifying program using Hoare Logic is finding the right loop invariants. The reason this is difficult is the same as the reason that inductive mathematical proofs are:

Strengthening a loop invariant means that you have a stronger assumption to work with when trying to establish the postcondition of the loop body, but it also means that the loop body’s postcondition is stronger and thus harder to prove.
Strengthening an induction hypothesis means that you have a stronger assumption to work with when trying to complete the induction step of the proof, but it also means that the statement being proved inductively is stronger and thus harder to prove.

As you recall the [Hoare While] rule,


            {P && b} s {P}
      --------------------------- (Hoare While)
      {P} while b { s } {P && !b}

if P is an invariant of s, then no matter how many times the loop body executes, s is going to be true when the loop finally finishes.

P must be strong enough to prove the postcondition and weak enough to be inferred from the precondition. This section explains how to approach the challenge of finding loop invariants through a series of examples and exercises.

9.2.1 Slow Subtraction🔗

The following program subtracts the value of x from the value of y by repeatedly decrementing both x and y. We want to verify its correctness with respect to the pre- and post-conditions shown:

Dafny

{ x == m && y == n }
  while !(x == 0) do
    y := y - 1;
    x := x - 1;
  end
{ y == n - m }

To verify this program, we need to find an invariant [Inv] for the loop. As a first step we can leave [Inv] as an unknown and build a skeleton for the proof by applying the rules for local consistency, working from the end of the program to the beginning, as usual, and without any thinking at all yet.

This leads to the following skeleton:


        (1)    { x == m && y == n }  ->                   (a)
        (2)    { Inv }
                 while x > 0 {
        (3)    { Inv && x > 0 }  ->                       (c)
        (4)    { Inv [x := x-1] [y := y-1] }
                   y := y - 1;
        (5)    { Inv [x := x-1] }
                   x := x - 1
        (6)    { Inv }
                 }
        (7)    { Inv && !(x > 0) }  ->                    (b)
        (8)    { y == n - m }

By examining this skeleton, we can see that any valid [Inv] will have to respect three conditions:

it must be weak enough to be implied by the loop’s precondition, i.e., (1) must imply (2);
(b) it must be strong enough to imply the program’s postcondition, i.e., (7) must imply (8);
(c) it must be preserved by each iteration of the loop (given that the loop guard evaluates to true), i.e., (3) must imply (4).

These conditions are actually independent of the particular program and specification we are considering: every loop invariant has to satisfy them.

One way to find an invariant that simultaneously satisfies these three conditions is by using an iterative process: start with a "candidate" invariant (e.g., a guess or a heuristic choice) and check the three conditions above; if any of the checks fails, try to use the information that we get from the failure to produce another – hopefully better – candidate invariant, and repeat.

For instance, in the reduce-to-zero example above, we saw that, for a very simple loop, choosing [true] as an invariant did the job. Maybe it will work here too. To find out, let’s try instantiating [Inv] with [true] in the skeleton above and see what we get...


        (1)    { x == m && y == n } ->      (a - OK)
        (2)    { true }
                 while x > 0 {
        (3)    { true && x > 0 } ->         (c - OK)
        (4)    { true }
                   y := y - 1;
        (5)    { true }
                   x := x - 1
        (6)    { true }
                 }
        (7)    { true && !(x > 0) } ->      (b - WRONG!)
        (8)    { y == n - m }

While conditions (a) and (c) are trivially satisfied, (b) is wrong: it is not the case that [true && !(x > 0)] (7) implies [y == n - m] (8). In fact, the two assertions are completely unrelated, so it is very easy to find a counterexample to the implication (say, [y = x = m = 0] and [n = 1]).

If we want (b) to hold, we need to strengthen the invariant so that it implies the postcondition (8). One simple way to do this is to let the invariant be the postcondition. So let’s return to our skeleton, instantiate [Inv] with [y == n - m], and try checking conditions (a) to (c) again.


    (1)    { x == m && y == n } ->         (a - WRONG!)
    (2)    { y == n - m }
             while x > 0 {
    (3)    { y == n - m && x > 0 } ->      (c - WRONG!)
    (4)    { y - 1 == n - m }
               y := y - 1;
    (5)    { y == n - m }
               x := x - 1
    (6)    { y == n - m }
             }
    (7)    { y == n - m && !(x > 0) } ->   (b - OK)
    (8)    { y == n - m }

This time, condition (b) holds trivially, but (a) and (c) are broken. Condition (a) requires that (1) [x == m && y == n] implies (2) [y == n - m]. If we substitute y by n we have to show that [n == n - m] for arbitrary m and n, which is not the case (for instance, when m = n = 1). Condition (c) requires that [n - m - 1 == n - m], which fails, for instance, for n = 1 and m = 0. So, although [y == n - m] holds at the end of the loop, it does not hold from the start, and it doesn’t hold on each iteration; it is not a correct invariant.

This failure is not very surprising: the variable y changes during the loop, while m and n are constant, so the assertion we chose didn’t have much chance of being an invariant!

To do better, we need to generalize (7) to some statement that is equivalent to (8) when x is 0, since this will be the case when the loop terminates, and that "fills the gap" in some appropriate way when x is nonzero. Looking at how the loop works, we can observe that x and y are decremented together until x reaches 0. So, if [x == 2] and [y == 5] initially, after one iteration of the loop we obtain [x == 1] and [y == 4]; after two iterations [x == 0] and [y == 3]; and then the loop stops. Notice that the difference between y and x stays constant between iterations: initially, [y == n] and [x == m], and the difference is always (n - m). So let’s try instantiating [Inv] in the skeleton above with [y - x == n - m].


    (1)    { x == m && y == n } ->            (a - OK)
    (2)    { y - x == n - m }
             while x > 0 {
    (3)    { y - x == n - m && x > 0 } ->     (c - OK)
    (4)    { (y - 1) - (x - 1) == n - m }
               y := y - 1;
    (5)    { y - (x - 1) = n - m }
               x := x - 1
    (6)    { y - x == n - m }
             }
    (7)    { y - x == n - m && !(x > 0) } ->  (b - OK?)
    (8)    { y = n - m }

Success? If everything is a natural number conditions (a), (b) and (c) all hold now; However, the same is not true if everything is an integer, as !(x > 0) does not imply x = 0. In that case, we would need to further strengthen the invariant to include that x >= 0 (assuming that’s the case to begin with):

    
    (1)    { m >= 0 && n >= 0 && x == m && y == n } ->      (a - OK)
    (2)    { y - x == n - m }
             while x > 0 {
    (3)    { x >= 0 && y - x == n - m && x > 0 } ->         (c - OK)
    (4)    { (x - 1) >= 0 && (y - 1) - (x - 1) == n - m }
               y := y - 1;
    (5)    { (x - 1) >= 0 && y - (x - 1) = n - m }
               x := x - 1
    (6)    { x >= 0 && y - x == n - m }
             }
    (7)    { x >= 0 && y - x == n - m && !(x > 0) } ->      (b - OK)
    (8)    { y = n - m }

Dafny

method SlowSubtraction(n:int, m:int) returns (y:int)
  requires m >= 0
{
  assert true ==> n - m == n - m;
  assert n - m == n - m;
  var x := m;
  assert  n - x == n - m;
  y := n;
  assert  y - x == n - m;
  while !(x == 0)
    invariant y - x == n - m
    decreases x
  {
    assert (y - 1)-(x - 1) == n - m;
    y := y - 1;
    assert y - (x - 1) == n - m;
    x := x - 1;
    assert y - x == n - m;
  }
  assert y - x == n - m && x == 0 ==> y == n - m;
}

Or simply:

Dafny

  method SlowSubtraction'(n:int, m:int) returns (y:int)
  requires m >= 0
{
  var x := m;
  y := n;
  while !(x == 0)
    invariant y - x == n - m
    decreases x
  {
    y := y - 1;
    x := x - 1;
  }
}

9.2.2 Slow Assignment🔗

A roundabout way of assigning a number currently stored in x to the variable y is to start y at 0, then decrement x until it hits 0, incrementing y at each step. Here is a program that implements this idea.

Dafny

method Slow_Assignment(m : nat) returns (y:nat)
ensures m == y
{
  var x:= m;
  assert x == m ==> x >= 0;
  y := 0;
  assert x + y == m && x >= 0;
  while x > 0
    invariant x + y == m && x >= 0
  {
    assert x + y == m && x >= 0;
    assert x-1 + (y+1) == m && x >= 0;
    x := x - 1;
    assert x + (y+1) == m && x >= 0;
    y := y + 1;
    assert x + y == m && x >= 0;
  }
  assert  x + y == m && x >= 0 && ! (x > 0)  ==>  y == m;
  assert  x + y == m;
}

9.2.3 Parity🔗

Here is a cute way of computing the parity of a value initially stored in x.


       { x == m }
         while 2 <= x do
           x := x - 2
         end
       { x = parity m }

The parity function used in the specification is defined in as follows:


function parity(x:nat): nat {
  match x
  case 0 => 0
  case 1 => 1
  case _ => parity (x - 2)
}

Dafny

method compute_parity(m:nat) returns (x:nat)
  // requires true
  // ensures (x == parity(m))
{
  // { true } ->
  // { parity(m) == parity(m) }
  x := m;
  // { parity(x) == parity(m) }
  while 2 <= x
  {
    // {parity(x) == parity(m) && 2 <= x}
    // {parity(x - 2) == parity(m)}
    x := x - 2;
    // {parity(x) == parity(m)}
  }
  // { parity(x) == parity(m) && !(2 <= x)} ->
  // { x == parity(m) }
}

The postcondition does not hold at the beginning of the loop, since [m == parity m] does not hold for an arbitrary m, so we cannot hope to use that as an invariant. To find an invariant that works, let’s think a bit about what this loop does.

On each iteration it decrements x by 2, which preserves the parity of x. So the parity of x does not change, i.e., it is invariant. The initial value of x is m, so the parity of x is always equal to the parity of m. Using [parity x == parity m] as an invariant we obtain the following annotated program:


      { x == m } ->                                         (a - OK)
      { parity x == parity m }
        while 2 <= x {
                     { parity x == parity m && 2 <= x } ->   (c - OK)
                     { parity (x-2) == parity m }
          x := x - 2
                     { parity x == parity m }
        }
      { parity x == parity m && !(2 <= x) } ->               (b - OK)
      { x == parity m }

With this invariant, conditions (a), (b), and (c) are all satisfied. For verifying (b), we observe that, when [x < 2], we have [parity x = x] (we can easily see this in the definition of [parity]). For verifying (c), we observe that, when [2 <= x], we have [parity x = parity (x-2)].

Dafny

method compute_parity(m:nat) returns (x:nat)
  ensures (x == parity(m))
{
  assert true==> parity(m) == parity(m);
  x := m;
  assert parity(x) == parity(m);
  while 2 <= x
    invariant parity(x) == parity(m)
  {
    assert parity(x) == parity(m) && 2 <= x;
    assert parity(x - 2) == parity(m);
    x := x - 2;
    assert parity(x) == parity(m);
  }
  assert parity(x) == parity(m) && !(2 <= x) ==> x == parity(m);
}

9.2.4 Square Root🔗

The following program computes the integer square root of m by naive iteration:

z := 0;
while (z+1)*(z+1) <= m {
  z := z+1
}
{ z*z<=m && m<(z+1)*(z+1) }

Very often, when a variable is used in a loop in a read-only fashion (i.e., it is referred to by the program or by the specification and it is not changed by the loop), it is necessary to record the fact that it doesn’t change in the loop invariant.

We try z*z <= m as the loop invariant:

Dafny

method SquareRoot(m:int) returns (z:int)
  ensures z * z <= m <= (z + 1) * (z+1)
  requires m >= 0
{
  assert m >0 ==> 0 * 0 <= m;
  assert 0 * 0 <= m;
  z := 0;
  assert z * z <= m;
  while (z+1)*(z+1) <= m
    invariant z * z  <= m
    decreases m - z * z
  {
    assert (z+1)*(z+1) <= m;
    z := z + 1;
    assert z * z <= m;
  }
  assert z*z <= m < (z+1)*(z+1) && !((z+1)*(z+1) <= m);
}

9.2.5 Squaring🔗

Here is a program that squares x by repeated addition:

{ x == m }
y := 0;
z := 0;
while y < x {
  z := z + x;
  y := y + 1
}
{ z == m*m }

The first thing to observe is that the loop reads the value of x but does not modify it. Meanwhile, z increases as the loop index y increments, maintaining the relationship z = x * y at each step. Below is the fully annotated Dafny code.

Dafny

method Square(x:nat) returns (z:nat)
  ensures x * x == z
{
  assert true ==>0 == 0 * x;
  assert 0 == 0 * x;
  var y := 0;
  assert 0 == y * x;
  z := 0;
  assert z == y * x;
  while y < x
    invariant z == x * y
    invariant 0 <= y <= x
    decreases x - y
  {
    assert z + x == x * (y+1) ==> z == x * y;
    z := z + x;
    assert z == x * (y+1);
    y := y + 1;
    assert z == x * y;
  }
  assert z == x * y && !(y < x) ==> z == x * x;
}

It is worth comparing the postcondition [z == x * x] and the [z == y * x] conjunct of the invariant. It is often the case that one has to replace parameters with variables – or with expressions involving both variables and parameters, like [x - y] – when going from postconditions to invariants.

9.2.6 Factorial🔗

Recall that n! denotes the factorial of n (i.e., n! = 1*2*...*n). We can easily define it in Dafny as follows:


function fact (n : nat) : nat {
  match n
  case 0 => 1
  case _ => n * (fact(n-1))
}

Let’s write the imperative Dafny program factorial that calculates the factorial.

Dafny

method factorial(n:nat) returns (x:nat)
  requires true
  ensures (x == fact(n))
{
  var i := 0;
  x := 1;
  assert x == fact(i) ;
  while (i < n)
    invariant x == fact(i)
    invariant 0 <= i <= n
    decreases n - i
  {
    assert x == fact(i) && 0 <= i <= n;
    i := i + 1;
    x := x * i;
    assert x == fact(i) && 0 <= i <= n;
  }

  assert x == fact(i) && 0 <= i <= n && !(i < n);
  // simplify
  assert x == fact(i) && i == n;
}

9.2.7 Minimum🔗

Dafny

method Min(a:nat, b:nat) returns (z:nat)
  ensures z == a || z == b
  ensures z <= a && z <= b
{
  assert true;
  assert a == a && b == b;
  var x := a;
  assert x == a && b == b;
  var y := b;
  assert x == a && y == b;
  z := 0;
  assert x + z == a && y + z == b;
  while x != 0 && y != 0
    decreases x
    decreases y
    invariant x + z == a && y + z == b
    invariant 0 <= x <= a
    invariant 0 <= y <= b
  {
    assert (x-1) + (z+1) == a && (y-1) + (z+1) == b ==>
        x + z == a && y + z == b;
    x := x - 1;
    assert x + (z+1) == a && (y-1) + (z+1) == b;
    y := y - 1;
    assert x + (z+1) == a && y + (z+1) == b;
    z := z + 1;
    assert x + z == a && y + z == b;
  }
  assert x + z == a && y + z == b  && !(x != 0 && y != 0) ==>
      (z == a || z == b) && z <= a && z <= b;
}

Or simply

OCaml REPL

method Min'(a:nat, b:nat) returns (z:nat)
  ensures z == a || z == b
  ensures z <= a && z <= b
{
  var x := a;
  var y := b;
  z := 0;
  while x != 0 && y != 0
    invariant x + z == a && y + z == b
    invariant 0 <= x <= a  && 0 <= y <= b
  {
    x := x - 1;
    y := y - 1;
    z := z + 1;
  }
}

9.2.8 Two Loops🔗

Here is a pretty inefficient way of adding 3 numbers:

x := 0;
y := 0;
z := c;
while x != a {
  x := x + 1;
  z := z + 1
};
while y <> b {
  y := y + 1;
  z := z + 1
}

Here is the fully annotated version of TwoLoops

Dafny

method TwoLoops(a:nat, b:nat, c:nat) returns (z:nat)
  ensures z == a + b + c
{
  assert true;
  assert c == c;
  var x := 0;
  var y := 0;
  assert c == x + c;
  z := c;
  assert z == x + c;
  while x != a
    decreases a - x
    invariant 0 <= x <= a
    invariant z == c + x
  {
    assert z+1 == x+1 + c ==> z == x + c;
    x := x + 1;
    assert z+1 == x + c;
    z := z + 1;
    assert z == x + c;
  }
  assert z == x + c && !(x != a) ==> z == a + c;
  assert z == a + c + y;
  while y != b
    decreases b - y
    invariant 0 <= y <= b
    invariant z == a + c + y
  {
    assert z+1 == a + c + y+1 ==> z == a + c + y;
    y := y + 1;
    assert z+1 == a + c + y;
    z := z + 1;
    assert z == a + c + y;
  }
  assert z == a + c + y && !(y != b) ==>
      z == a + b + c;
}

9.2.9 Power Series🔗

Here is a program that computes the series:

1 + 2 + 2^2 + ... + 2^m = 2^(m+1) - 1

x := 0;
y := 1;
z := 1;
while x != m {
  z := 2 * z;
  y := y + z;
  x := x + 1;
}

Here is the annotated imperative implemenation of Power

Dafny

function pow2(n : nat) : nat {
  match n
  case 0 => 1
  case _ => 2 * (pow2 (n-1))
}
method power(n:nat) returns (y:nat)
  ensures y == pow2(n+1)-1
{
  assert true;
  assert 3 == 3;
  assert 1 + 2 * 1 == pow2(0+1+1)-1;
  var x := 0;
  assert 1 + 2 * 1 == pow2(x+1+1)-1;
  y := 1;
  assert y + 2 * 1 == pow2(x+2)-1;
  var z := 1;
  assert y + 2 * z == pow2(x+2)-1;
  while x != n
    decreases n - x
    invariant 0 <= x <= n
    invariant z == pow2(x)
    invariant y == pow2(x+1)-1
  {
    assert y + 2 * z == pow2(x+2)-1;
    z := 2 * z;
    assert y+z == pow2(x+2)-1;
    y := y + z;
    assert y == pow2(x+1+1)-1;
    x := x + 1;
    assert y == pow2(x+1)-1;
  }
  assert !(x != n) && z == pow2(x) && y == pow2(x+1)-1 ==>
      y == pow2(n+1)-1;
}

9.2.10 Fibonacci Again🔗

The recursive Fibonacci algorithm is extremely slow, making it a classic example for practicing loop-based optimizations.

Dafny

function Fib(n: nat): nat {
  if n < 2 then n else Fib(n - 2) + Fib(n - 1)
}

method ComputeFib(n: nat) returns (x: nat)
  ensures x == Fib(n)
{
  x := 0;
  var i, y := 0, 1;
  assert 0 <= i <= n && x == Fib(i) && y == Fib(i + 1);
  while i != n
    decreases n - i
    invariant 0 <= i <= n
    invariant x == Fib(i) && y == Fib(i + 1)
  {
    assert i != n && 0 <= i <= n && x == Fib(i) && y == Fib(i + 1);
    assert 0 <= i+1 <= n && y == Fib(i + 1) && x + y == Fib(i + 2);
    x, y := y, x + y;
    assert 0 <= i+1 <= n && x == Fib(i + 1) && y == Fib(i + 2);
    i := i + 1;
    assert 0 <= i <= n && x == Fib(i) && y == Fib(i + 1);
  }
  assert i == n && x == Fib(i) && y == Fib(i + 1) ==>
          x == Fib(n);
}

9.2.11 Lists Revisited🔗

Let us implement the List<T> functions with loops.

Dafny

datatype List<T> = Nil | Cons(head: T, tail: List<T>)

function Length<T>(ls: List<T>): nat {
  match ls
  case Nil => 0
  case Cons(_, ls') => 1 + Length(ls')
}

method LengthLoop<T>(ls: List<T>) returns (sum: nat)
  ensures sum == Length(ls)
{
  var l := ls;
  sum := 0;
  while l.Cons?
    invariant sum + Length(l) == Length(ls)
    // Invariant:  what additional work needs to be done,
    //  to produce the final answer
    decreases Length(l)
    // Use the Length function to show termination
  {
    sum := sum + 1;
    l := l.tail;
  }
}

predicate Member<T(==)>(x: T, ls: List<T>) {
  match ls
  case Nil => false
  case Cons(y, ls') => y == x || Member(x, ls')
}

method MemberLoop<T(==)>(x: T, ls: List<T>) returns (b: bool)
  ensures b == Member(x, ls)
{
  var l := ls;
  while l.Cons?
    invariant Member(x, l) == Member(x, ls)
    // The invariant for the Memeber is simpler, because the
    // transformed current problem instance is exactly equivalent to
    // the original instance.

    decreases Length(l)
  {
    if l.head == x {
      return true;
    } else {
      l := l.tail;
    }
  }
  return false;
}

function At<T>(xs:List<T>, i:nat):(r:T)
  requires i < Length(xs)
  ensures Member(r,xs)
{
  if i == 0 then xs.head else At(xs.tail, i-1)
}

method AtLoop1<T>(ls:List<T>, n:nat) returns (r:T)
  requires n < Length(ls)
  ensures r == At(ls,n)
{
  var l := ls;
  var i := n;
  while true
    invariant 0 <= i <= n
    invariant Length(l) == Length(ls) - (n - i)
    invariant At(l,i) == At(ls,n)
    decreases i
  {
    if i == 0 {
      return l.head;
    }else{
      i := i - 1;
      l := l.tail;
    }
  }
}

method AtLoop2<T>(ls:List<T>, n:nat) returns (r:T)
  requires n < Length(ls)
  ensures r == At(ls,n)
{
  var l := ls;
  var i := n;

  while i > 0
    invariant 0 <= i <= n
    invariant Length(l) == Length(ls) - (n - i)
    invariant At(l,i) == At(ls,n)
    decreases i
  {
      i := i - 1;
      l := l.tail;
  }
    return l.head;
}

contents ← prev up next →

	Syllabus
	Texts
	Schedule
	Notes
	Assignments
	Midterms
	Final
	Software

1	Dafny Cheatsheet
2	Dafny Basics
3	Getting Started with Dafny
4	Dafny Collections
5	Floyd Hoare Logic
6	Inductive Proofs
7	Inductive Types
8	Sorting
9	Loop Invariants
10	Arrays
11	SAT Solvers
12	Solving SAT and SMT Problems Using Z3