diff options
| author |  Rustan Leino <leino@microsoft.com> | 2013-01-22 23:20:40 -0800 |
|---|---|---|
| committer | Rustan Leino <leino@microsoft.com> | 2013-01-22 23:20:40 -0800 |
| commit | d3e8fdae367e29bc9fae675b3befe5a3bbc5daa0 (patch) | |
| tree | c7b0992bbe1ff6fec231b3f34857201cbfa46a96 /Test/dafny3/SimpleInduction.dfy | |
| parent | 3934a2bf234377d26a199a3e7ae98c6eebf4a9ab (diff) | |
Examples from co-induction paper
Diffstat (limited to 'Test/dafny3/SimpleInduction.dfy')
| -rw-r--r-- | Test/dafny3/SimpleInduction.dfy | 85 |
1 files changed, 85 insertions, 0 deletions
diff --git a/Test/dafny3/SimpleInduction.dfy b/Test/dafny3/SimpleInduction.dfy new file mode 100644 index 00000000..5331b808 --- /dev/null +++ b/Test/dafny3/SimpleInduction.dfy @@ -0,0 +1,85 @@ +/*
+ The well-known Fibonacci function defined in Dafny. The postcondition of
+ method FibLemma states a property about Fib, and the body of the method is
+ code that convinces the program verifier that the postcondition does indeed
+ hold. Thus, effectively, the method states a lemma and its body gives the
+ proof.
+ */
+
+function Fib(n: nat): nat
+ decreases n;
+{ if n < 2 then n else Fib(n-2) + Fib(n-1) }
+
+ghost method FibLemma(n: nat)
+ ensures Fib(n) % 2 == 0 <==> n % 3 == 0;
+ decreases n;
+{
+ if (n < 2) {
+ } else {
+ FibLemma(n-2);
+ FibLemma(n-1);
+ }
+}
+
+/*
+ The 'parallel' statement has the effect of applying its body simultaneously
+ to all values of the bound variables---in the first example, to all k
+ satisfying 0 <= k < n, and in the second example, to all non-negative n.
+*/
+
+ghost method FibLemma_Alternative(n: nat)
+ ensures Fib(n) % 2 == 0 <==> n % 3 == 0;
+{
+ parallel (k | 0 <= k < n) {
+ FibLemma_Alternative(k);
+ }
+}
+
+ghost method FibLemma_All()
+ ensures forall n :: 0 <= n ==> (Fib(n) % 2 == 0 <==> n % 3 == 0);
+{
+ parallel (n | 0 <= n) {
+ FibLemma(n);
+ }
+}
+
+/*
+ A standard inductive definition of a generic List type and a function Append
+ that concatenates two lists. The ghost method states the lemma that Append
+ is associative, and its recursive body gives the inductive proof.
+
+ We omitted the explicit declaration and uses of the List type parameter in
+ the signature of the method, since in simple cases like this, Dafny is able
+ to fill these in automatically.
+ */
+
+datatype List<T> = Nil | Cons(head: T, tail: List<T>);
+
+function Append<T>(xs: List<T>, ys: List<T>): List<T>
+ decreases xs;
+{
+ match xs
+ case Nil => ys
+ case Cons(x, rest) => Cons(x, Append(rest, ys))
+}
+
+// The {:induction false} attribute disables automatic induction tactic,
+// so we can make the proof explicit.
+ghost method {:induction false} AppendIsAssociative(xs: List, ys: List, zs: List)
+ ensures Append(Append(xs, ys), zs) == Append(xs, Append(ys, zs));
+ decreases xs;
+{
+ match (xs) {
+ case Nil =>
+ case Cons(x, rest) =>
+ AppendIsAssociative(rest, ys, zs);
+ }
+}
+
+// Here the proof is fully automatic - the body of the method is empty,
+// yet still verifies.
+ghost method AppendIsAssociative_Auto(xs: List, ys: List, zs: List)
+ ensures Append(Append(xs, ys), zs) == Append(xs, Append(ys, zs));
+{
+}
+
|