Induction in general is finding a way to build your goal up one step at a time. Viewed another way, it is proving your goal in terms of a smaller version. The distributive lemma is proven by deconstructing the concatenated sequence one element at a time until the first sequence is entirely gone. This case is proven as a base case, and then the whole chain of deconstructions is verified.

The key to making this work is that Dafny never has to consider the whole chain of calls. By checking termination, it can get the chain is finite. Then all it has to do is check one step. If one arbitrary step is valid, then the whole chain must be as well. This is the same logic that Dafny uses for loops: check that the invariant holds initially, and that one arbitrary step preserves it, and you have checked the whole loop, regardless of how many times the loop goes around. The similarity is more than superficial. Both kinds of lemmas (and both kinds of reasoning Dafny makes about your program) are inductive. It is also not suprising given the relationship between iteration and recursion as two means of acheiving the same thing.

With this in mind, we can complete the lemma by calling the lemma recursively in the else branch of the if statement:

edit

if (a == [])

{

assert a + b == b;

}

else

{

DistributiveLemma(a[1..], b);

assert a + b == [a[0]] + (a[1..] + b);

}

Now the lemma verifies. But what if we wanted to express that every pair of sequences is related in this way? We must look at another way of specifying lemmas in Dafny in order to be able to do this, which we will explore with another example.

Function Lemmas

As a final example, we will prove something which requires us to use a function lemma. A function lemma is just like a method lemma, except it uses the post-condition of a function rather than method to prove the desired result. The advantage of this is that the function can be used in annotations, and not just inside methods. This means that we can get the forall quantification that we couldn't achieve above.

The problem that we will consider is that of paths through a directed graph. A directed graph is composed of a number of Nodes, each with some links to other Nodes. These links are single directional, and the only restriction on them is that a node cannot link to itself. Nodes are defined as:

class Node

{

// a single field giving the nodes linked to

var next: seq<Node>;

}

We represent a graph as a set of non-null Nodes that only point to other nodes in the graph, and not to itself. We call such a set of nodes closed:

function closed(graph: set<Node>): bool

reads graph;

{

null !in graph && // graphs can only consist of actual nodes, not null.

forall i :: i in graph ==>

(forall k :: 0 <= k < |i.next| ==> i.next[k] in graph && i.next[k] != i)

}

We represent a path as a non-empty sequence of nodes, where each node is linked to by the previous node in the path. We define two predicates, one that defines a valid path, and another that determines whether the given path is a valid one between two specific nodes in the graph:

function pathSpecific(p: seq<Node>, start: Node, end: Node, graph: set<Node>): bool

reads p;

requires closed(graph);

{

0 < |p| && // path is non-empty

start == p[0] && end == p[|p|-1] && // it starts and ends correctly

path(p, graph) // and it is a valid path

}

function path(p: seq<Node>, graph: set<Node>): bool

requires closed(graph) && 0 < |p|;

reads p;

decreases |p|;

{

p[0] in graph &&

(|p| > 1 ==> p[1] in p[0].next && // the first link is valid, if it exists

path(p[1..], graph)) // and the rest of the sequence is a valid

}

Now we are ready to state the lemma we want to prove. We consider a graph and a sub-graph: a subset of the nodes of the graph which also form a graph. This sub-graph must be closed, i.e. not contain links outside of itself. If we have such a situation, then there cannot be a valid path from a node in the sub-graph to a node outside this subgraph. We will call this fact the Closed Lemma. It can be stated in Dafny as a traditional method lemma:

edit

ghost method ClosedLemma(subgraph: set<Node>, root: Node, goal: Node, graph: set<Node>)

requires closed(subgraph) && closed(graph) && subgraph <= graph;

requires root in subgraph && goal !in subgraph && goal in graph;

ensures !(exists p: seq<Node> :: pathSpecific(p, root, goal, graph));

{

...

}

The pre-conditions state all the requirements: that both the graph and sub-graph are valid, that the root node is in the sub-graph but the goal isn't, and that everything is contained in the main graph. The post-condition states that there is no valid path from the root to the goal. Here we only prove it for a specific pair of start/end nodes.

One way of proving the non-existence of something is to prove given any sequence of nodes that it cannot be a valid path. We can do this with, you guessed it, another lemma. This lemma will prove for any given sequence, that it cannot be a valid path from root to goal. There is a catch, however: we want to be able to invoke this lemma within a quantifier. We want to say thatforall sequences, they are not a valid path. Thus we must use a function lemma.

A function lemma is like a method lemma in that both use their post-conditions to express the properties they are trying to prove. Functions must return a value, so function lemmas returnbools with an addition postcondition saying that they always return true. This lets them be used in implications and other boolean expressions. The general form of a function lemma is:

function Lemma(a: T, ...): bool

ensures desirable property;

ensures Lemma(a, ...);

{

... //proof

}

In our case, the disproof of a path lemma looks like:

edit

function DisproofLemma(p: seq<Node>, subgraph: set<Node>,

root: Node, goal: Node, graph: set<Node>): bool

requires closed(subgraph) && closed(graph) && subgraph <= graph;

requires root in subgraph && goal !in subgraph && goal in graph;

reads p;

ensures DisproofLemma(p, subgraph, root, goal, graph);

ensures !pathSpecific(p, root, goal, graph);

{

...

}

The pre-conditions are the same as ClosedLemma, and the reads clause allows us to look at thenext fields of the nodes along the path. The first post-condition says that the function will always return true. This will allow us to put it in a quantifier:

edit

ghost method ClosedLemma(subgraph: set<Node>, root: Node, goal: Node, graph: set<Node>)

...

ensures !(exists p: seq<Node> :: pathSpecific(p, root, goal, graph));

{

assert forall p :: DisproofLemma(p, subgraph, root, goal, graph);

}

As you can see, this causes the ClosedLemma to verify, so our test of the the lemma is successful. Thus DisproofLemma is strong enough, and our work is reduced to just proving it.

There are a few different ways that a sequence of nodes can be an invalid path. If the path is empty, then it cannot be a valid path. Also, the first element of the path must be root and the last element needs to be goal. Because root in subgraph and goal !in subgraph, we must haveroot != goal, so the sequence must have at least two elements. To check that Dafny sees this, we can put preconditions on our lemma as follows:

edit

function DisproofLemma(p: seq<Node>, subgraph: set<Node>,

root: Node, goal: Node, graph: set<Node>): bool

requires ...; // as before

requires |p| < 2 || p[0] != root || p[|p|-1] != goal;

...

{

true

}

Note that this will cause ClosedLemma to stop verifying, as the lemma now only works for some sequences. We will ignore ClosedLemma until we have finished DisproofLemma. This verifies, which means that Dafny is able to prove the post-condition in these circumstances. Thus we only need to prove that the path is invalid when these conditions do not hold. We can use an implication to express this:

1 < |p| && p[0] == root && p[|p|-1] == goal ==> (further proof)

If the path is at least two elements long, the first element is root, and the last is goal, then we have a further proof. If these conditions are not met, Dafny will prove the post-condition on its own. When the first part of the implication is false, then the whole implication is true, so the lemma will return true as required. Now we just need to fill in the further proof part. This should always be true, but it can rely on the first part of the implication being true. Now we can use the same inductive trick as above, but this time to show something must be false.

If the sequence starts at root and ends at goal, it cannot be valid because the sequence must at some point have a node which is not in the previous nodes next list. When we are given any particular sequence like this, we can break it into two cases: either the sequence is invalid in the link from the first node to the second, or it is broken somewhere down the line. Just like in the counting example, Dafny can see that if the first to second node link is not valid, then the sequence cannot be a path because this mirrors the definition of path. Thus we only have further work to do if the first link is valid. We can express this with another implication:

1 < |p| && p[0] == root && p[|p|-1] == goal ==>

(p[1] in p[0].next ==> (yet further proof))

Here comes the induction. We know that p[0] == root and p[1] in p[0].next. We also know from the pre-conditions that root in subgraph. Thus, because closed(subgraph), we know that p[1] in subgraph. These are the same conditions that we started with! What we have here is a smaller version of the same problem. We can just recursively call DisproofLemma to prove that p[1..] is not a path. This means, per the definition of path, that p cannot be a path, and the second post-condition is satisfied. Further, since the lemma always returns true, the implications will always be true, and the first post-condition will also be satisfied. This can be implmented as:

edit

function DisproofLemma(p: seq<Node>, subgraph: set<Node>,

root: Node, goal: Node, graph: set<Node>): bool

requires closed(subgraph) && closed(graph) && subgraph <= graph;

requires root in subgraph && goal !in subgraph && goal in graph;

reads p;

ensures DisproofLemma(p, subgraph, root, goal, graph);

ensures !pathSpecific(p, root, goal, graph);

{

1 < |p| && p[0] == root && p[|p|-1] == goal ==>

(p[1] in p[0].next ==>

DisproofLemma(p[1..], subgraph, p[1], goal, graph))

}

Now DisproofLemma verifies, and with the removal of the testing pre-conditions, we see thatClosedLemma verifies as well. We have thus proven that there cannot be a path from inside a closed sub-graph to outside.

Function lemmas are useful when a lemma is required inside of a quantifier, or when it is needed inside a function, which cannot call method lemmas. Because they always return true, a function lemma can be put in the pre-conditions of a function without changing the actual allowed inputs. The inability to use assertions and loops, as well as the un-intuitive control flow make method lemmas the better choice when the ubiquity of function lemmas is not required. In either case, inductive reasoning and unwrapping functions in the same way are the primary means of pushing through a difficult lemma. Always remember to check that your lemma is sufficient to prove what you need. Nothing is more frustrating than spending a while making a lemma verify, only to find out you need something stronger. This also lets you avoid creating a lemma with a pre-condition that is so restrictive that you cannot call it where you need to.

Termination

Dafny proves that all programs terminate. There are two potential sources of non-terminating (divergent) behavior: loops, and recursive functions and methods. Dafny employs a single technique for handling either case, decreases annotations.

A decreases annotation specifies a value, called the termination measure, that becomes strictly smaller each time a loop is traversed or each time a recursive function or method is called. This value is also bounded so that it cannot decrease forever. This way, if the value starts at any arbitrary finite value, the loop or recursion must stop. To prove this, Dafny proves that the termination measure gets smaller on each iteration. If Dafny cannot prove this, it says there is a failure to decrease termination measure. Because each kind of termination measure comes with a built-in lower bound, this is all Dafny needs to do to prove termination.

There are several kinds of values that Dafny can use in decreases annotations, but the most common are integers. Integers have a natural lower bound, zero, and it is usually quite easy to prove that they decrease. Since many loops iterate through indices, these kinds of termination proofs are very common. For example, we may have the following loop:

edit

while(i < n)