// In the previous class, we used well-founded orders on non-negative integers and on datatypes. // Now, we define a well-founded order on all types, see slides. // As the slides show, we also consider compositions of well-founded orders: union, adding // a top element, and lexicographic tuples of various lengths. // In this class, we'll show many useful examples of how to prove termination. // Here is an example that uses the well-founded order on Booleans, where `false` is smaller // than `true`. function x(c: bool): int decreases c { if c then y(c) else 0 } function y(c: bool): int decreases !c { if c then 1 else x(c) } // The Ackermann function is a famous function that grows very quickly. Evaluating the // function can take a long time, but it's easy to prove that it does indeed terminate. // We do that using a lexicographic pair. function Ack(m: nat, n: nat): nat decreases m, n { if m == 0 then n + 1 else if n == 0 then Ack(m - 1, 1) else Ack(m - 1, Ack(m, n - 1)) } // The next example counts the number of integers `i`, where `0 <= i < n`, that satify `P(i)`. // For this example, the precise definition of `P` does not matter, so we omit its body. // Here is the straightforward way to define function `CountPs`, and proving termination of // this function is also simple. predicate P(x: int) function CountPs(n: nat): int decreases n { if n == 0 then 0 else if P(n - 1) then 1 + CountPs(n - 1) else CountPs(n - 1) } // Suppose the recursive cases of `CountPs` were more complicated. Then, we may want to // refactor those cases into a separate function: function CountPs2(n: nat): int decreases 2 * n + 1 { if n == 0 then 0 else if P(n - 1) then AddAndCountTheRest(n, 1) else AddAndCountTheRest(n, 0) } function AddAndCountTheRest(n: nat, x: int): int requires n != 0 decreases 2 * n { x + CountPs2(n - 1) } // To prove termination of these mutually recursive functions, we can't just use // `decreases n` for both functions, because the call from `CountPs2` to `AddAndCountTheRest` // does not cause a decrease in parameter `n`. Instead, these two functions use the // `decreases` clauses `2 * n + 1` and `2 * n`, respectively. // An easier way to prove termination is to use a lexicographic pair rather than // multiplying by 2 and adding, as shown here: function CountPs3(n: nat): int decreases n, 1 { if n == 0 then 0 else if P(n - 1) then AddAndCountTheRest3(n, 1) else AddAndCountTheRest3(n, 0) } function AddAndCountTheRest3(n: nat, x: int): int requires n != 0 decreases n, 0 { x + CountPs3(n - 1) } // The choice of `1` and `0` in these `decreases` clauses is arbitrary. Any two // expressions where the former is larger than the latter would work. For example, // decreases n, 496 // decreases n, 28 // would also work. Since Dafny pads `decreases` clauses with a "top" element at the // end, we can also omit the constant in the `decreases` clause of `CountPs3`. // Then, since "top" is larger than anything else, we can replace the constant // in the `decreases` clause of `AddAndCountTheRest3` with any expression, for // example, with `x`. We then get function CountPs4(n: nat): int decreases n { if n == 0 then 0 else if P(n - 1) then AddAndCountTheRest4(n, 1) else AddAndCountTheRest4(n, 0) } function AddAndCountTheRest4(n: nat, x: int): int requires n != 0 decreases n, x { x + CountPs4(n - 1) } // This choice is especially nice, because each of these `decreases` clauses // lists the respective function's parameters, which is what Dafny's default // `decreases` clauses do. Thus, we can omit these `decreases` clauses altogether // and rely on the defaults. function CountPs5(n: nat): int { if n == 0 then 0 else if P(n - 1) then AddAndCountTheRest5(n, 1) else AddAndCountTheRest5(n, 0) } function AddAndCountTheRest5(n: nat, x: int): int requires n != 0 { x + CountPs5(n - 1) } // In fact, the `decreases m, n` clause that we used for the Ackermann function // above also coincides with the default `decreases` clause for that function, so // the verifier will prove termination of that function even if we omit an explicit // `decreases` clause. This is often the case in practice, which is why we didn't have to // write any `decreases` clauses in the first many weeks of this class. // (Remember: If you want to find out what `decreases` clause Dafny uses as the default, // look at the function's hover text in the IDE.) // The next example is a function that illustrates what seems like a need to increment // the termination metric. That doesn't work, of course, because then we're not proving // termination, and such a function might not terminate at all. But if there's some // limit on how many times such increments can happen, then we can prove termination. // To set the stage, let's start with a function that has an easy termination proof: function Combine(a: nat, b: nat): (c: nat) ensures c == 100 * a + b decreases a, b { if a == 0 then b else if b == 0 then Combine(a - 1, b + 100) // else if 5000 <= b then // Combine(a + 1, b - 100) else Combine(a, b - 1) + 1 } // The `b == 0` branch of this function essentially trades 1 unit of `a` for 100 // units of `b`. That decreases the lexicographic pair `a, b` and maintains the // property in the function's postcondition. // // Now, suppose we want to go in the other direction, as indicated by the two lines // that are commented out above. That commented-out branch trades 100 units of `b` // for 1 unit of `a`, provided there is an ample supply of `b` units. If we included // those two lines, the function does not always terminate. // // Let's limit the number of times that we are willing to take that branch. To do so, // we'll introduce an extra parameter that holds a "budget" for how many times we're // willing to increment `a` in this way. Now, we can prove termination using a // lexicographic triple. function Combine2(a: nat, b: nat, incBudget: nat): (c: nat) ensures c == 100 * a + b decreases incBudget, a, b { if a == 0 then b else if b == 0 then Combine2(a - 1, b + 100, incBudget) else if 5000 <= b && incBudget != 0 then Combine2(a + 1, b - 100, incBudget - 1) else Combine2(a, b - 1, incBudget) + 1 } // In the next example, we define multiplication as a function that // performs repeated additions and we prove that our function is commutative, // that is, that `Mult(x, y)` is the same as `Mult(y, x)`. The proof makes // five calls to the induction hypothesis (that is, five recursive calls to the // lemma itself). Each of those calls show a decrease of the lexicographic // pair `x, y`, which proves termination. Two of the recursive calls are // creative and interesting. function Mult(x: nat, y: nat): nat { if y == 0 then 0 else x + Mult(x, y - 1) } lemma {:induction false} MultCommutative(x: nat, y: nat) ensures Mult(x, y) == Mult(y, x) decreases x, y { if x == y { } else if x == 0 { assert Mult(x, y) == Mult(x, y - 1); assert Mult(y, x) == 0 == Mult(y - 1, x); MultCommutative(x, y - 1); } else if y < x { // This is one of the two interesting uses of the induction hypothesis. // This recursive call takes care of all cases where `y` is less than `x`. // It works because the property we're trying to prove is symmetric in // `x` and `y` and because the recursive call terminates since we're giving // a first parameter that's smaller than the given `x`. MultCommutative(y, x); } else { calc { Mult(x, y); == // def. Mult x + Mult(x, y - 1); == { MultCommutative(x, y - 1); } x + Mult(y - 1, x); == // def. Mult x + y - 1 + Mult(y - 1, x - 1); // Here is the other interesting use of the induction hypothesis. Since the // line above has the term `Mult(y - 1, x - 1)`, our first attempt at calling // the lemma recursively might be `MultCommutative(y - 1, x - 1)`. However, // such a call may not terminate, because we can't prove that `y - 1, x - 1` // is below `x, y`. Luckily, because the property we're trying to prove is // symmetric in `x` and `y`, we can use the recursive call `MultCommutative(x - 1, y - 1)` // (note the order of the parameters) to obtain the information about // `Mult(y - 1, x - 1)` that we need. By ordering the parameters in this way, // we also decrease the lexicographic pair `x, y`, so we're able to prove termination. == { MultCommutative(x - 1, y - 1); } x + y - 1 + Mult(x - 1, y - 1); == // def. Mult y + Mult(x - 1, y); == { MultCommutative(x - 1, y); } y + Mult(y, x - 1); == // def. Mult Mult(y, x); } } } // The next example shows another common pattern of using the induction hypothesis. // The property proved by the `DropSame` lemma is that two different ways of defining // a "drop" function (which returns a given list, dropping its first `n` elements) // give the same result. datatype List = Nil | Cons(head: X, tail: List) function Length(xs: List): nat { if xs == Nil then 0 else 1 + Length(xs.tail) } function Drop(xs: List, n: nat): List requires n <= Length(xs) { if n == 0 then xs else Drop(xs.tail, n - 1) } function Drop'(xs: List, n: nat): (r: List) requires n <= Length(xs) ensures Length(r) == Length(xs) - n { // To take the `.tail` of `Drop'(xs, n - 1)` in the following line, we need // to know that this call returns a nonempty list. To obtain that piece of // information, we add a postcondition of `Drop'` that speaks about the length // of its result. if n == 0 then xs else Drop'(xs, n - 1).tail } lemma DropSame(xs: List, n: nat) requires n <= Length(xs) ensures Drop(xs, n) == Drop'(xs, n) { if n < 2 { // easy } else { calc { Drop(xs, n); == // def. Drop Drop(xs.tail, n - 1); == { DropSame(xs.tail, n - 1); } // I.H. Drop'(xs.tail, n - 1); == // def. Drop' Drop'(xs.tail, n - 2).tail; == { DropSame(xs.tail, n - 2); } // I.H. Drop(xs.tail, n - 2).tail; == // def. Drop Drop(xs, n - 1).tail; == { DropSame(xs, n - 1); } // I.H. Drop'(xs, n - 1).tail; == // def. Drop' Drop'(xs, n); } } } // An interesting aspect of this proof is that it makes three calls to the induction hypothesis. // Since one of those calls passes the argument `n - 2`, the `calc` statement in the proof // requires `2 <= n`. So, both `n == 0` and `n == 1` are handled separately (and both are // proved automatically, so we just need to spell out the `if n < 2` branch of the proof). // Problem set 4 did some optimization of queries. We had included a precondition `arg < p` // in one of the mutually recursive functions. It states that `arg` is structurally included // in `p`. This is needed in the termination proof, and we can now explain why: module QueryOptimization { type Name = string type Row = map datatype Expr = | Const(value: int) | Var(name: Name) | Plus(0: Expr, 1: Expr) datatype Pred = | Equal(e0: Expr, e1: Expr) | Leq(e0: Expr, e1: Expr) | And(p0: Pred, p1: Pred) datatype List = Nil | Cons(head: X, tail: List) type Table = List datatype Query = | Source(rows: Table) | Union(q0: Query, q1: Query) | Project(names: set, q: Query) | Select(cond: Pred, q: Query) function ProjectUnionOptimization(query: Query): Query decreases query { match query case Source(_) => query case Union(q0, q1) => Union(ProjectUnionOptimization(q0), ProjectUnionOptimization(q1)) case Project(_, q) => MoveProjectionInward(query, q) case Select(cond, q) => Select(cond, ProjectUnionOptimization(q)) } function MoveProjectionInward(p: Query, arg: Query): Query requires p.Project? && arg < p // the second conjunct says that `arg` is structurally included in `p` decreases p, arg { match arg case Union(q0, q1) => // The proofs of termination for these calls just need the facts that q0 and q1 // are structurally included in `arg.` var opt0 := MoveProjectionInward(p, q0); var opt1 := MoveProjectionInward(p, q1); Union(opt0, opt1) case _ => // To prove termination of the call `ProjectUnionOptimization(arg)`, we need to show that `arg` is // below the lexicographic pair `p, arg`. That's why we need `arg < p`. Project(p.names, ProjectUnionOptimization(arg)) } // If you were writing the two functions above without having to prove termination, then perhaps // you would have chosen to let `MoveProjectionInward` take `names: set` as its first parameter // instead of `p: Query`, which in our code above just acts like a wrapper around `p.names`. If you do // want the `set` parameter to be what's used at run time, then you can mark the `p` parameter // as `ghost`, that is, as specification-only. This gives us access to `p` so we can prove termination, // but `p` is then erased by the compiler and will not be part of the running program. function ProjectUnionOptimization'(query: Query): Query decreases query { match query case Source(_) => query case Union(q0, q1) => Union(ProjectUnionOptimization'(q0), ProjectUnionOptimization'(q1)) case Project(_, q) => MoveProjectionInward'(query, query.names, q) case Select(cond, q) => Select(cond, ProjectUnionOptimization'(q)) } function MoveProjectionInward'(ghost p: Query, names: set, arg: Query): Query requires p.Project? && arg < p decreases p, arg { match arg case Union(q0, q1) => var opt0 := MoveProjectionInward'(p, names, q0); var opt1 := MoveProjectionInward'(p, names, q1); Union(opt0, opt1) case _ => Project(names, ProjectUnionOptimization'(arg)) } } // Here is a final example that illustrates another useful pattern of writing termination // specifications. It uses a variation of the constants we've seen above. // The `Flatten` function takes a list of lists and puts their elements into a sequence. // // A straightforward way of doing that is to use two functions, one for converting // a list into a sequence and another for repeatedly calling the first and concatenating // the results. Each of those functions would be recursive, but the two functions are // not mutually recursive. // // The version we write here is different. It uses two mutually recursive functions and // passes a "continuation" from one to the other. This continuation says what to do // when the inner function has exhausted the given list `xs`. function Flatten(xss: List>): seq decreases xss, 0 { match xss case Nil => [] case Cons(s, tail) => FlattenInner(s, tail) } function FlattenInner(xs: List, continuation: List>): seq decreases continuation, 1, xs { match xs case Nil => Flatten(continuation) case Cons(x, xs') => [x] + FlattenInner(xs', continuation) } // The last piece of material in this class is an explanation of how all // functions/lemmas/methods, not just recursive ones, make use of one and the // same well-founded order. This is necessary to argue that an entire program // terminates, even though we're only proving that its recursive (and mutually // recursive) functions/lemmas/methods terminate. // // Consider a recursive function `Fib` for computing Fibonacci numbers and a // function `SumOfFibs` that calls `Fib` on each element of a list and adds up // the results. Termination of the recursive calls in these functions is // easy to prove, as we've seen before. But let's try to write `decreases` clauses // that could be used to show a decrease with every call, not just the recursive // ones. Here's a way to do that: function SumOfFibs(xs: List): nat decreases 1, xs { if xs == Nil then 0 else Fib(xs.head) + SumOfFibs(xs.tail) } function Fib(n: nat): nat decreases 0, n { if n < 2 then n else Fib(n-2) + Fib(n-1) } // The use of the constants 1 and 0 can be thought of as indicating how many // non-recursive calls can still be done. That is, you can think of functions // as being placed into strata, where a non-recursive call is one that goes from // one stratum to a lower stratum. This is illustrated using colors in this // class's slides. // // It would be tedious for a programmer to have to maintain these strata manually. // For example, if a helper function were added between `SumOfFibs` and `Fib`, then // the strata in the example would have to be renumbered. Dafny does this automatically // and completely hides this bookkeeping from the user. This is done by computing // a call graph for every module, grouping each _strongly connected component_ of // that call graph into a stratum of its own. // // Again, this explains why an entire program terminates, even though we're just // proving termination of recursive (and mutually recursive) functions/lemmas/methods. // You do not need to encode these strata yourself---just write `decreases` clauses // as we've seen (and you can omit those, too, when the default `decreases` clauses // fit the bill).