Dafny

method MyMethod(x: int) returns (y: int)
  requires 10 <= x
  ensures 25 <= y
{
  var a, b;
  a := x + 3;
  if x < 20 {
    b := 32 - x;
  } else {
    b := 16;
  }
  y := a + b;
}

Dafny

method MyMethod_forward(x: int) returns (y: int)
  requires 10 <= x
  ensures 25 <= y
{
  We start with the precondition.
  assert 10 <= x;

  var a, b;
  // Variable declaration. The variables could store anything!

  a := x + 3;
  assert 10 <= x && a == x + 3;
  // We use "and" to record that we learned the value of 'a'.

  if x < 20 {
    // Important: here we know that the 'if' test succeeded!
    assert 10 <= x && a == x + 3 && x < 20;

    b := 32 - x;
    assert 10 <= x && a == x + 3 && x < 20 && b == 32 - x;
  } else {
    // Now we know that the test failed.
    assert 10 <= x && a == x + 3 && !(x < 20);
    b := 16;
    assert 10 <= x && a == x + 3 && !(x < 20) && b == 16;
  }

  // What is true after the 'if'?
  // We must have followed one of the two paths, which is
  // well-expressed with 'or'.
  assert (10 <= x && a == x + 3 && x < 20 && b == 32 - x)
       || (10 <= x && a == x + 3 && !(x < 20) && b == 16);

  y := a + b;
  assert ((10 <= x && a == x + 3 && x < 20 && b == 32 - x)
    || (10 <= x && a == x + 3 && !(x < 20) && b == 16))
    && y == a + b;
  // At this point, we simply check that the formula we calculated
  // implies the method postcondition!  That check can be phrased
  // as a formula itself:
  assert (((10 <= x && a == x + 3 && x < 20 && b == 32 - x)
      || (10 <= x && a == x + 3 && !(x < 20) && b == 16))
      && y == a + b)
    ==> 25 <= y;
}

Dafny

method Swap(x: int, y: int) returns (a: int, b: int)
  ensures a == y && b == x
{
  a, b := x, y;
  assert a == x && b == y;

  var tmp := a;
  assert a == x && b == y && tmp == a;
  // OK, the next one is going to be trouble.
  a := b;
  // assert a == x && b == y && tmp == a && a == b;
  // Nope, can't prove that one!
  b := tmp;
}

Dafny

method Swap_backward(x: int, y: int) returns (a: int, b: int)
  ensures a == y && b == x
{
  // The final formula we calculate is obviously true, which is
  // necessary, since we have no precondition/'requires'.

  // This rule easily generalizes to parallel assignment (multiple
  // variables to left of ':=').
  assert y == y && x == x;
  a, b := x, y;

  assert b == y && a == x;
  var tmp := a;

  assert b == y && tmp == x;
  a := b;

  // The rule for assignment may now be surprising: replace all
  // mentions of the variable being assigned, turning them into
  // copies of the expression being assigned!
  assert a == y && tmp == x;

  b := tmp;

  // Our easy starting point: copy in the postcondition.
  assert a == y && b == x;
}

Dafny

method MyMethod_backward(x: int) returns (y: int)
  requires 10 <= x
  ensures 25 <= y
{
  // We need to confirm that our precondition truly implies that
  // formula, which proof goal we restate here explicitly.
  assert 10 <= x ==> ((x < 20 && 25 <= (x + 3) + (32 - x))
         || (!(x < 20) && 25 <= (x + 3) + 16));

  var a, b;

  assert (x < 20 && 25 <= (x + 3) + (32 - x))
         || (!(x < 20) && 25 <= (x + 3) + 16);
  a := x + 3;

  // Now we mechanically create an "or" of the two top formulas
  // of the blocks, also "and"ing in the 'if' expression or its
  // negation.
  assert (x < 20 && 25 <= a + (32 - x))
         || (!(x < 20) && 25 <= a + 16);
  if x < 20 {
    assert 25 <= a + (32 - x);
    b := 32 - x;
    assert 25 <= a + b;
  } else {
    assert 25 <= a + 16;
    b := 16;
    assert 25 <= a + b;
  }
  // For an 'if', copy the current formula into
  // the ends of the two blocks.

  assert 25 <= a + b;
  y := a + b;

  // Easy start: copy in the postcondition.
  assert 25 <= y;
}

Dafny

method Seq1(a: int, b: int) returns (r: int)
  ensures r == a + b
{
  // Great: we're down to a simple arithmetic formula that is easy
  // to check.
  assert 0 <= 0 < 3 && 0 <= 2 < 3 && 0 <= 1 < 3
         && a + 3 * b - 2 * b == a + b;
  // That last assertion can be simplified using algebraic
  // properties of sequence operations, to the above:
  assert 0 <= 0 < |[a, 2 * b, 3 * b]|
         && 0 <= 2 < |[a, 2 * b, 3 * b]|
         && 0 <= 1 < |[a, 2 * b, 3 * b]|
         && ([a, 2 * b, 3 * b][0]
            + [a, 2 * b, 3 * b][2]
            - [a, 2 * b, 3 * b][1]) == a + b;
  var s : seq<int> := [a, 2 * b, 3 * b];
  assert 0 <= 0 < |s| && 0 <= 2 < |s| && 0 <= 1 < |s|
         && s[0] + s[2] - s[1] == a + b;
  r := s[0];
  assert 0 <= 2 < |s| && 0 <= 1 < |s| && r + s[2] - s[1] == a + b;
  r := r + s[2];
  // Note that we add a requirement of in-bounds access, in
  // processing a read from a sequence.
  assert 0 <= 1 < |s| && r - s[1] == a + b;
  r := r - s[1];
  assert r == a + b;
}

Dafny

method Seq2(s: seq<int>, i: int) returns (r: seq<int>)
  requires 0 <= i < |s|
  ensures r == s
{
  // This top assertion trivially simplifies into the precondition.
  assert 0 <= i < |s| && s == s;
  // Going from the line below to the one above, we use the fact
  // that concatenating these two particular slices rebuilds the
  // original sequence.
  assert 0 <= i < |s[..i] + s[i..]| && s[..i] + s[i..] == s;
  r := s[..i] + s[i..];
  assert 0 <= i < |r| && r == s;
  assert 0 <= i < |r| && 0 <= i < |r| && r[i := r[i] + 10 - 10] == s;
  // OK, that last formula is getting unwieldy!
  // Let's do two rounds of simplification.
  assert 0 <= i < |r| && 0 <= i < |r[i := r[i] + 10]|
         && r[i := r[i] + 10][i := r[i := r[i] + 10][i] - 10] == s;
  r := r[i := r[i] + 10];
  assert 0 <= i < |r| && r[i := r[i] - 10] == s;
  r := r[i := r[i] - 10];
  assert r == s;
}

Dafny

method Set1(a: int, b: int) returns (r: bool)
  ensures r == (a == b)
{
  return |{a, b}| == 1;
  // Tricky way to compute equality, huh?
}

Dafny

method Set2(s: set<int>, t: set<int>, u: set<int>)
  ensures s + t == t + s                   // '+' is union.
  ensures s * t == t * s                   // '*' is intersection.
  ensures s * (t + u) == s * t + s * u     // distributivity
  ensures 13 !in s ==> |s + {13}| == |s| + 1 // membership
  ensures s <= s + t + u                    // subset
{
  // Dafny automatically proves the Postconditions.
  // We don't actually need to write any code here.
  // We could still calculate formulas using set operators!
}

Dafny

method Multiset1(a: int, b: int) returns (r: bool)
  ensures r == false
{
  return |multiset{a, b}| == 1;
  // Why does this expression indeed always return 'false'?
  // Because this multiset always has two elements, never one!
  // It just might be that the two elements are equal.
}

method Multiset2(m : multiset<int>) returns (m': multiset<int>)
  requires |m| > 0
  ensures m + m != m  // Negation of a set property that doesn't
                      // hold for multisets!
  ensures m * m == m // But this one does.
  ensures |m'| > |m|
{
  m' := m[42 := m[42] + 8];
  // This notation adjusts the count of element 42, to 8 more
  // than it started out. If 42 was not in the original multiset,
  // 'm[42]' evaluates to 0.
}

Dafny

method Map1(ak: int, bk: int, av: int, bv: int)
            returns (m: map<int, int>)
  requires ak != bk
  ensures |m| == 2
  ensures ak in m
  ensures m[ak] == av
  ensures bk in m
  ensures m[bk] == bv
  ensures m.Keys == {ak, bk}
  ensures m.Values == {av, bv}
  ensures (ak, av) in m.Items
  ensures (bk, bv) in m.Items
  // We snuck in an example of tuples!
{
  m := map[];
  m := m[ak := av];
  m := m[bk := bv];
}

Dafny

method IsDuplicateAt(s: seq<int>, n: int) returns (b: bool)
  requires 0 <= n < |s|
  ensures b == (s[n] in s[..n] || s[n] in s[n+1..])
{
  // This assertion helps Dafny figure out why the method meets
  // its specification.  Think of it like proposing a useful lemma
  // on the way to a theorem.  Dafny doesn't invent the lemmas on
  // its own, but it is able to check them and then use them to
  // prove later facts.
  assert s == s[..n] + [s[n]] + s[n+1..];
  return multiset(s)[s[n]] > 1;
}

• If statement s begins execution in a state satisfying assertion P,

• and if s eventually terminates in some final state,

• then that final state will satisfy the assertion Q.

• We begin with the unannotated program (the unnumbered lines).

• We add the specification – i.e., the outer precondition (1) and postcondition (5). In the precondition, we use parameters m and n to remember the initial values of variables x and y so that we can refer to them in the postcondition (5).

• We work backwards, mechanically, starting from (5) and proceeding until we get to (2). At each step, we obtain the precondition of the assignment from its postcondition by substituting the assigned variable with the right-hand-side of the assignment. For instance, we obtain (4) by substituting x with x - y in (5), and we obtain (3) by substituting y with x - y in (4).

• We start with the outer precondition (1) and postcondition (8).

• Following the format dictated by the [hoare_if] rule, we copy the postcondition (8) to (4) and (7). We conjoin the precondition (1) with the guard of the conditional to obtain (2). We conjoin (1) with the negated guard of the conditional to obtain (5).

• In order to use the assignment rule and obtain (3), we substitute z by y - x in (4). To obtain (6) we substitute z by x - y in (7).

• Finally, we verify that (2) implies (3) and (5) implies (6). Both of these implications crucially depend on the ordering of x and y obtained from the guard. For instance, knowing that x <= y ensures that subtracting x from y and then adding back x produces y, as required by the first disjunct of (3). Similarly, knowing that !(x <= y)] ensures that subtracting y from x and then adding back y produces x, as needed by the second disjunct of (6). Note that n - m + m = n does _not_ hold for arbitrary natural numbers n and m (Dafny, in particular, won’t even let you perform a subtraction that would get you in the negatives)