diff options
Diffstat (limited to 'Test/dafny4/Ackermann.dfy')
| -rw-r--r-- | Test/dafny4/Ackermann.dfy | 235 |
1 files changed, 235 insertions, 0 deletions
diff --git a/Test/dafny4/Ackermann.dfy b/Test/dafny4/Ackermann.dfy new file mode 100644 index 00000000..7ab686e0 --- /dev/null +++ b/Test/dafny4/Ackermann.dfy @@ -0,0 +1,235 @@ +// RUN: %dafny /compile:3 /rprint:"%t.rprint" /autoTriggers:1 "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+// Rustan Leino, 8 Sep 2015.
+// This file proves that the Ackermann function is monotonic in each argument
+
+method Main() {
+ // Note, don't try much larger numbers unless you're prepared to wait!
+ print "Ack(3, 4) = ", Ack(3, 4), "\n";
+}
+
+// Here is the definition of the Ackermann function:
+function method Ack(m: nat, n: nat): nat
+{
+ if m == 0 then
+ n + 1
+ else if n == 0 then
+ Ack(m - 1, 1)
+ else
+ Ack(m - 1, Ack(m, n - 1))
+}
+
+// And here is the theorem that proves the desired result:
+lemma AckermannIsMonotonic(m: nat, n: nat, m': nat, n': nat)
+ requires m <= m' && n <= n'
+ ensures Ack(m, n) <= Ack(m', n')
+{
+ // This is the proof. It calls two lemmas, stated and proved below.
+ MonotonicN(m, n, n');
+ MonotonicM(m, n, m');
+}
+
+// --------------------------------------------------------
+// What follows are the supporting lemmas and their proofs.
+// --------------------------------------------------------
+
+// Proving that Ackermann is monotonic in its second argument is easy.
+lemma MonotonicN(m: nat, n: nat, n': nat)
+ requires n <= n'
+ ensures Ack(m, n) <= Ack(m, n')
+{
+ // In fact, Dafny completes this proof automatically.
+}
+
+// To prove the other direction, we consider an alternative formulation
+// of the Ackermann function, namely a curried form:
+function CurriedAckermann(m: int, n: int): int
+{
+ A(m)(n)
+}
+
+function A(m: int): int -> int
+{
+ if m <= 0 then
+ n => n + 1
+ else
+ n => Iter(A(m-1), n)
+}
+
+function Iter(f: int -> int, n: int): int
+ requires IsTotal(f)
+ decreases n
+{
+ if n <= 0 then
+ f(1)
+ else
+ f(Iter(f, n-1))
+}
+
+// In the 3-part definition above, function Iter needs to know that it can
+// apply its function parameter "f". Therefore, Iter's precondition says that
+// "f" must be total. We define totality of "f" by saying that its precondition
+// holds for any n and that it never reads the heap:
+predicate IsTotal(f: int -> int)
+ reads f.reads
+{
+ forall n :: f.requires(n) && f.reads(n) == {}
+}
+
+// Now, we can prove certain things about CurriedAckermann. The first thing we
+// prove is that it gives the same result as the Ack function above.
+
+lemma CurriedIsTheSame(m: nat, n: nat)
+ ensures CurriedAckermann(m, n) == Ack(m, n)
+{
+ // The proof considers 3 cases, following the 3 cases in the definition of Ack
+ if m == 0 {
+ // trivial
+ } else if n == 0 {
+ // trivial
+ } else {
+ // we help Dafny out with the following lemma:
+ assert A(m)(n) == A(m-1)(Iter(A(m-1), n-1));
+ }
+}
+
+// Monotonicity in the first argument of Ackermann now follows from the fact that,
+// for m <= m', A(m) is a function that is always below A(m')
+lemma MonotonicM(m: nat, n: nat, m': nat)
+ requires m <= m'
+ ensures Ack(m, n) <= Ack(m', n)
+{
+ CurriedIsTheSame(m, n);
+ CurriedIsTheSame(m', n);
+ ABelow(m, m');
+}
+
+// We must now prove ABelow. To do that, we will prove some properties of A and of
+// Iter. Let us define the three properties we will reason about.
+
+// The first property is a relation on functions. It is the property that above was referred
+// to as "f is a function that is always below g". The lemma ABelow(m, m') used above establishes
+// FunctionBelow(A(m), A(m')).
+predicate FunctionBelow(f: int -> int, g: int -> int)
+ requires IsTotal(f) && IsTotal(g)
+{
+ forall n :: f(n) <= g(n)
+}
+
+// The next property says that a function is monotonic.
+predicate FunctionMonotonic(f: int -> int)
+ requires IsTotal(f)
+{
+ forall n,n' :: n <= n' ==> f(n) <= f(n')
+}
+
+// The third property says that a function's return value is strictly greater than its argument.
+predicate Expanding(f: int -> int)
+ requires IsTotal(f)
+{
+ forall n :: n < f(n)
+}
+
+// We will prove that A(_) satisfies the properties FunctionBelow, FunctionMonotonic, and
+// FunctionExpanding. But first we prove three properties of Iter.
+
+// Provided that "f" is monotonic and expanding, Iter(f, _) is monotonic.
+lemma IterIsMonotonicN(f: int -> int, n: int, n': int)
+ requires IsTotal(f) && Expanding(f) && FunctionMonotonic(f) && n <= n'
+ ensures Iter(f, n) <= Iter(f, n')
+{
+ // This proof is a simple induction over n' and Dafny completes the proof automatically.
+}
+
+// Next, we prove that Iter(_, n) is monotonic. That is, given functions "f" and "g"
+// such that FunctionBelow(f, g), we have Iter(f, n) <= Iter(g, n). The lemma requires
+// "f" to be monotonic, but we don't have to state the same property for g.
+lemma IterIsMonotonicF(f: int -> int, g: int -> int, n: int)
+ requires IsTotal(f) && IsTotal(g) && FunctionMonotonic(f) && FunctionBelow(f, g)
+ ensures Iter(f, n) <= Iter(g, n)
+{
+ // This proof is a simple induction over n and Dafny completes the proof automatically.
+}
+
+// Finally, we shows that for any expanding function "f", Iter(f, _) is also expanding.
+lemma IterExpanding(f: int -> int, n: int)
+ requires IsTotal(f) && Expanding(f)
+ ensures n < Iter(f, n)
+{
+ // Here, too, the proof is a simple induction of n and Dafny completes it automatically.
+}
+
+// We complete the proof by showing that A(_) has the three properties we need.
+
+// Of the three properties we prove about A(_), we start by showing that A(m) returns a
+// function that is expanding.
+lemma AExp(m: int)
+ ensures Expanding(A(m))
+{
+ if m <= 0 {
+ // trivial
+ } else {
+ // This branch of the proof follows from the fact that Iter(A(m-1), _) is expanding.
+ forall n {
+ // The following lemma requires A(m-1) to be expanding, which is something that
+ // following from our induction hypothesis.
+ IterExpanding(A(m-1), n);
+ }
+ }
+}
+
+// Next, we show that A(m) returns a monotonic function.
+lemma Am(m: int)
+ ensures FunctionMonotonic(A(m))
+{
+ if m <= 0 {
+ // trivial
+ } else {
+ // We make use of the fact that A(m-1) is expanding:
+ AExp(m-1);
+ // and the fact that Iter(A(m-1), _) is monotonic:
+ forall n,n' | n <= n' {
+ // The following lemma requires A(m-1) to be expanding and monotonic.
+ // The former comes from the invocation of AExp(m-1) above, and the
+ // latter comes from our induction hypothesis.
+ IterIsMonotonicN(A(m-1), n, n');
+ }
+ }
+}
+
+// Our final property about A, which is the lemma we had used above to prove
+// that Ackermann is monotonic in its first argument, is stated and proved here:
+lemma ABelow(m: int, m': int)
+ requires m <= m'
+ ensures FunctionBelow(A(m), A(m'))
+{
+ if m' <= 0 {
+ // trivial
+ } else if m <= 0 {
+ forall n {
+ calc {
+ A(m)(n);
+ ==
+ n + 1;
+ <= { AExp(m'-1); IterExpanding(A(m'-1), n); }
+ Iter(A(m'-1), n);
+ ==
+ A(m')(n);
+ }
+ }
+ } else {
+ forall n {
+ calc {
+ A(m)(n);
+ ==
+ Iter(A(m-1), n);
+ <= { Am(m-1); ABelow(m-1, m'-1);
+ IterIsMonotonicF(A(m-1), A(m'-1), n); }
+ Iter(A(m'-1), n);
+ ==
+ A(m')(n);
+ }
+ }
+ }
+}
|