Annotated class code. After each class we will release an annotated version of the code we looked at: on this page, that’s class02.dfy.
Exercise starting code. We will also post the exercise files that were distributed in class: on this page, scroll down to find class02/example.dfy, class02/swap.dfy, and class02/containers.dfy.
class02.dfy// Here is an innocuous method that meets a simple specification.
// How does Dafny check that the method is correct?
method ExampleMethod(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;
}
// Let's trace through _what Dafny knows_ at each line, by using
// assertions.
method ExampleMethod_forward(x: int) returns (y: int)
requires 10 <= x
ensures 25 <= y
{
// Well, to start with, we know the precondition.
assert 10 <= x;
var a, b;
// We don't learn anything going through this 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's true 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;
// We could check whether the postcondition would also hold in alternative
// scenarios.
assert (((10 <= x && a == x + 3 && x < 21 && b == 999 - x)
|| (10 <= x && a == x + 3 && !(x < 21) && b == 13))
&& y == a + b) ==> 25 <= y;
// Do note that this implication is checked given our knowledge of what could
// be true at this point in the program. If the formula to the left of the
// implication _contradicts_ what we know, then the implication holds trivially!
}
// There was a gotcha lurking in our intuitive method of modeling the effect of
// an assignment statement. How does it work for this program?
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;
}
// When variables are being reassigned as a method proceeds, our naive forward
// calculation of predicates gives the wrong results. Instead,
// counterintuitively, we can calculate _backward_!
// Please read the assertion annotations here from the end of the method to the
// beginning.
method Swap_backward(x: int, y: int) returns (a: int, b: int)
ensures a == y && b == x
{
// Excellent! 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;
}
// Let's repeat the backward exercise for our initial example.
method ExampleMethod_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;
}
// Ooo, an 'if'. What do we do? Start by copying 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;
}
// It turns out there _is_ actually a complete rule we can use to calculate
// formulas in the forward direction! In the case of assignment, we have to
// use an 'exists' quantifier. Here, then, is how we calculate forwards for our
// swapping method.
method Swap_forward(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;
// We trigger a different, more-complex rule when we _reassign_ a variable vs.
// assigning it in the first place.
a := b;
assert (exists old_a :: old_a == x && b == y && tmp == old_a) && a == b;
// See how we copied the previous formula, replacing 'a' with a fresh 'old_a'
// that we assert exists within the new formula?
// This version is more of a mouthful! Dafny also raises a warning about not
// being confident that it fully understands how to take advantage of this
// quantifier. Indeed, quantifiers tend to trigger less predictable behavior
// in the automatic program checker, so that's a pretty good reason to prefer
// the backwards style. But let's finish this example anyway.
b := tmp;
assert (exists old_b :: (exists old_a :: old_a == x && old_b == y && tmp == old_a) && a == old_b) && b == tmp;
// Then we can run the final implication check:
assert ((exists old_b :: (exists old_a :: old_a == x && old_b == y && tmp == old_a) && a == old_b) && b == tmp)
==> (a == y && b == x);
// By the way, these forward-direction calculation rules compute what are known
// as _strongest postconditions_. Here, "strongest" means "most precise." It
// is always logically sound to be a little less precise, allowing additional
// program states. If we let our imaginations run wild and add too many
// additional possibilities, we will often find ourselves unable to prove
// postconditions! However, it's often helpful to apply algebraic
// simplifications and general beautification. Here's one alternative to the
// formula we found with two quantifiers, just noticing that each quantified
// variable winds up known to be equal to another variable.
assert tmp == x && a == y && b == tmp;
// Actually, the method's postcondition is another formula we could choose
// to simplify to at this point, even independently of proving the method
// correct!
}
// See Chapter 2 of "Program Proofs" for a more formal take on all of these matters.
// For instance, it presents the dual concept of weakest preconditions.
// Instead of going into those formalities, let's meet some of the useful
// built-in, _immutable_ container types of Dafny, which turn out to work very
// well with this calculational style, because we are allowed to mention
// containers and operations on them in formulas.
// Here's a simple use of sequences, immutable arrays/lists.
// We will annotate all these examples with formulas in the backwards style
// (so again start from the end of the method).
method Sequence1(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;
}
// Here is another example, using _slicing_ and _functional update_.
// Each kind of operation builds a _new_ "modified" sequence, since sequences
// are immutable.
method Sequence2(s: seq<int>, i: int) returns (r: seq<int>)
requires 0 <= i < |s|
ensures r == s
{
// This top assertion trivially simplifies into the precondition. Done!
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;
}
// By the way, strings are just a special kind of sequence in Dafny: 'seq<char>'.
// We also have sets, just like in Python (though with some syntactic differences).
method Equal?_by_Set(a: int, b: int) returns (result: bool)
ensures result == (a == b)
{
return |{a, b}| == 1;
// Tricky way to compute equality, huh?
}
// Foreshadowing a pattern we'll learn a lot more about in the coming weeks, we
// can essentially use method specifications to check mathematical theorems.
method Facts_about_Set(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 7 !in s ==> |s + {7}| == |s| + 1 // membership
ensures s <= s + t + u // subset
{
// We don't actually need to write any code here.
// If we did, we could still calculate formulas using set operators!
}
// Most unusually, there are multisets (as we used to express correctness of
// sorting). Multisets are like sets but allow duplicates. Another way of
// putting it is that multisets are sequences where we forget element order.
method Two_by_Multiset(a: int, b: int) returns (result: int)
ensures result == 2
{
return |multiset{a, b}|;
// 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.
}
// Finally, another key data structure is maps, which are an immutable version
// of e.g. dictionaries in Python.
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];
}
// We can code up a variety of interesting transformations across container types.
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;
}class02/example.dfymethod ExampleMethod(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;
}
method ExampleMethod_forward(x: int) returns (y: int)
requires 10 <= x
ensures 25 <= y
{
// (1) what do we already know?
assert true;
var a, b;
// we don't learn anything from declaring those variables
a := x + 3;
// (2) use && to create a formula that records what we knew and what we know:
assert true;
// time to reason through an `if`...
if x < 20 {
// (3a) if we got here, what do we know?
assert true;
b := 32 - x;
// (4):
assert true;
} else {
// (3b) if we got here, what do we know?
assert true;
b := 16;
// (5):
assert true;
}
// (6) combine formulas (4) and (5)... how?
assert true;
y := a + b;
// (7):
assert true;
// (8) we need that formula to imply the postcondition:
assert true;
}
method ExampleMethod_backward(x: int) returns (y: int)
requires 10 <= x
ensures 25 <= y
{
// (8) we need the precondition to imply that formula:
assert true;
var a, b;
// (7):
assert true;
a := x + 3;
// (6) mechanically combine (4), (5), and the guard of the `if` (also use its negation):
assert true;
if x < 20 {
// (5):
assert true;
b := 32 - x;
// (3b) what needs to be true here?
assert true;
} else {
// (4):
assert true;
b := 16;
// (3a) what needs to be true here?
assert true;
}
// time to reason back through an `if`...
// (2) before assignment, we need:
assert 25 <= a + b;
y := a + b;
// (1) start with the postcondition:
assert 25 <= y;
}class02/swap.dfymethod Swap(x: int, y: int) returns (a: int, b: int)
ensures a == y && b == x
{
a, b := x, y;
var tmp := a;
a := b;
b := tmp;
}
method Swap_forward_incorrect(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;
a := b;
assert a == x && b == y && tmp == a && a == b; // oops, we can't prove that!
b := tmp;
}
method Swap_backward(x: int, y: int) returns (a: int, b: int)
ensures a == y && b == x
{
// (6): what can we simplify that to?
assert true;
// (5): same rule works for parallel assignment:
assert true;
a, b := x, y;
// (4):
assert true;
var tmp := a;
// (3):
assert true;
a := b;
// (2) the rule for assignment may be surprising... replace all mentions of
// the variable being assigned with copies of the expression being assigned:
assert true;
b := tmp;
// (1) easy starting point... copy in the postcondition:
assert true;
}class02/containers.dfymethod Equal?_by_Set(a: int, b: int) returns (result: bool)
ensures result == (a == b)
{
// implement without directly comparing a and b, instead put them in a set:
return true;
}
method Facts_about_Set(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 7 !in s ==> |s + {7}| == |s| + 1 // membership
ensures s <= s + t + u // subset
{
}
method Two_by_Multiset(a: int, b: int) returns (result: int)
ensures result == 2
{
var x := multiset{a, b};
// implement using x:
return 0;
}