diff options
Diffstat (limited to 'Test/dafny1/Rippling.dfy')
| -rw-r--r-- | Test/dafny1/Rippling.dfy | 617 |
1 files changed, 0 insertions, 617 deletions
diff --git a/Test/dafny1/Rippling.dfy b/Test/dafny1/Rippling.dfy deleted file mode 100644 index 835c3043..00000000 --- a/Test/dafny1/Rippling.dfy +++ /dev/null @@ -1,617 +0,0 @@ -// Datatypes
-
-datatype Bool = False | True;
-
-datatype Nat = Zero | Suc(Nat);
-
-datatype List = Nil | Cons(Nat, List);
-
-datatype Pair = Pair(Nat, Nat);
-
-datatype PList = PNil | PCons(Pair, PList);
-
-datatype Tree = Leaf | Node(Tree, Nat, Tree);
-
-// Boolean functions
-
-function not(b: Bool): Bool
-{
- match b
- case False => True
- case True => False
-}
-
-function and(a: Bool, b: Bool): Bool
-{
- if a == True && b == True then True else False
-}
-
-// Natural number functions
-
-function add(x: Nat, y: Nat): Nat
-{
- match x
- case Zero => y
- case Suc(w) => Suc(add(w, y))
-}
-
-function minus(x: Nat, y: Nat): Nat
-{
- match x
- case Zero => Zero
- case Suc(a) => match y
- case Zero => x
- case Suc(b) => minus(a, b)
-}
-
-function eq(x: Nat, y: Nat): Bool
-{
- match x
- case Zero => (match y
- case Zero => True
- case Suc(b) => False)
- case Suc(a) => (match y
- case Zero => False
- case Suc(b) => eq(a, b))
-}
-
-function leq(x: Nat, y: Nat): Bool
-{
- match x
- case Zero => True
- case Suc(a) => match y
- case Zero => False
- case Suc(b) => leq(a, b)
-}
-
-function less(x: Nat, y: Nat): Bool
-{
- match y
- case Zero => False
- case Suc(b) => match x
- case Zero => True
- case Suc(a) => less(a, b)
-}
-
-function min(x: Nat, y: Nat): Nat
-{
- match x
- case Zero => Zero
- case Suc(a) => match y
- case Zero => Zero
- case Suc(b) => Suc(min(a, b))
-}
-
-function max(x: Nat, y: Nat): Nat
-{
- match x
- case Zero => y
- case Suc(a) => match y
- case Zero => x
- case Suc(b) => Suc(max(a, b))
-}
-
-// List functions
-
-function concat(xs: List, ys: List): List
-{
- match xs
- case Nil => ys
- case Cons(x,tail) => Cons(x, concat(tail, ys))
-}
-
-function mem(x: Nat, xs: List): Bool
-{
- match xs
- case Nil => False
- case Cons(y, ys) => if x == y then True else mem(x, ys)
-}
-
-function delete(n: Nat, xs: List): List
-{
- match xs
- case Nil => Nil
- case Cons(y, ys) =>
- if y == n then delete(n, ys) else Cons(y, delete(n, ys))
-}
-
-function drop(n: Nat, xs: List): List
-{
- match n
- case Zero => xs
- case Suc(m) => match xs
- case Nil => Nil
- case Cons(x, tail) => drop(m, tail)
-}
-
-function take(n: Nat, xs: List): List
-{
- match n
- case Zero => Nil
- case Suc(m) => match xs
- case Nil => Nil
- case Cons(x, tail) => Cons(x, take(m, tail))
-}
-
-function len(xs: List): Nat
-{
- match xs
- case Nil => Zero
- case Cons(y, ys) => Suc(len(ys))
-}
-
-function count(x: Nat, xs: List): Nat
-{
- match xs
- case Nil => Zero
- case Cons(y, ys) =>
- if x == y then Suc(count(x, ys)) else count(x, ys)
-}
-
-function last(xs: List): Nat
-{
- match xs
- case Nil => Zero
- case Cons(y, ys) => match ys
- case Nil => y
- case Cons(z, zs) => last(ys)
-}
-
-function apply(f: FunctionValue, xs: List): List
-{
- match xs
- case Nil => Nil
- case Cons(y, ys) => Cons(Apply(f, y), apply(f, ys))
-}
-
-// In the following two functions, parameter "p" stands for a predicate: applying p and
-// getting Zero means "false" and getting anything else means "true".
-
-function takeWhileAlways(p: FunctionValue, xs: List): List
-{
- match xs
- case Nil => Nil
- case Cons(y, ys) =>
- if Apply(p, y) != Zero
- then Cons(y, takeWhileAlways(p, ys))
- else Nil
-}
-
-function dropWhileAlways(p: FunctionValue, xs: List): List
-{
- match xs
- case Nil => Nil
- case Cons(y, ys) =>
- if Apply(p, y) != Zero
- then dropWhileAlways(p, ys)
- else Cons(y, ys)
-}
-
-function filter(p: FunctionValue, xs: List): List
-{
- match xs
- case Nil => Nil
- case Cons(y, ys) =>
- if Apply(p, y) != Zero
- then Cons(y, filter(p, ys))
- else filter(p, ys)
-}
-
-function insort(n: Nat, xs: List): List
-{
- match xs
- case Nil => Cons(n, Nil)
- case Cons(y, ys) =>
- if leq(n, y) == True
- then Cons(n, Cons(y, ys))
- else Cons(y, ins(n, ys))
-}
-
-function ins(n: Nat, xs: List): List
-{
- match xs
- case Nil => Cons(n, Nil)
- case Cons(y, ys) =>
- if less(n, y) == True
- then Cons(n, Cons(y, ys))
- else Cons(y, ins(n, ys))
-}
-
-function ins1(n: Nat, xs: List): List
-{
- match xs
- case Nil => Cons(n, Nil)
- case Cons(y, ys) =>
- if n == y
- then Cons(y, ys)
- else Cons(y, ins1(n, ys))
-}
-
-function sort(xs: List): List
-{
- match xs
- case Nil => Nil
- case Cons(y, ys) => insort(y, sort(ys))
-}
-
-function reverse(xs: List): List
-{
- match xs
- case Nil => Nil
- case Cons(t, rest) => concat(reverse(rest), Cons(t, Nil))
-}
-
-// Pair list functions
-
-function zip(a: List, b: List): PList
-{
- match a
- case Nil => PNil
- case Cons(x, xs) => match b
- case Nil => PNil
- case Cons(y, ys) => PCons(Pair.Pair(x, y), zip(xs, ys))
-}
-
-function zipConcat(x: Nat, xs: List, more: List): PList
-{
- match more
- case Nil => PNil
- case Cons(y, ys) => PCons(Pair.Pair(x, y), zip(xs, ys))
-}
-
-// Binary tree functions
-
-function height(t: Tree): Nat
-{
- match t
- case Leaf => Zero
- case Node(l, x, r) => Suc(max(height(l), height(r)))
-}
-
-function mirror(t: Tree): Tree
-{
- match t
- case Leaf => Leaf
- case Node(l, x, r) => Node(mirror(r), x, mirror(l))
-}
-
-// Function parameters
-
-// Dafny currently does not support passing functions as arguments. To simulate
-// arbitrary functions, the following type and Apply function play the role of
-// applying some prescribed function (here, a value of the type)
-// to some argument.
-
-type FunctionValue;
-function Apply(f: FunctionValue, x: Nat): Nat // this function is left uninterpreted
-
-// The following functions stand for the constant "false" and "true" functions,
-// respectively.
-
-function AlwaysFalseFunction(): FunctionValue
- ensures forall n :: Apply(AlwaysFalseFunction(), n) == Zero;
-function AlwaysTrueFunction(): FunctionValue
- ensures forall n :: Apply(AlwaysTrueFunction(), n) != Zero;
-
-// -----------------------------------------------------------------------------------
-// The theorems to be proved
-// -----------------------------------------------------------------------------------
-
-ghost method P1()
- ensures forall n, xs :: concat(take(n, xs), drop(n, xs)) == xs;
-{
-}
-
-ghost method P2()
- ensures forall n, xs, ys :: add(count(n, xs), count(n, ys)) == count(n, concat(xs, ys));
-{
-}
-
-ghost method P3()
- ensures forall n, xs, ys :: leq(count(n, xs), count(n, concat(xs, ys))) == True;
-{
-}
-
-ghost method P4()
- ensures forall n, xs :: add(Suc(Zero), count(n, xs)) == count(n, Cons(n, xs));
-{
-}
-
-ghost method P5()
- ensures forall n, xs, x ::
- add(Suc(Zero), count(n, xs)) == count(n, Cons(x, xs))
- ==> n == x;
-{
-}
-
-ghost method P6()
- ensures forall m, n :: minus(n, add(n, m)) == Zero;
-{
-}
-
-ghost method P7()
- ensures forall m, n :: minus(add(n, m), n) == m;
-{
-}
-
-ghost method P8()
- ensures forall k, m, n :: minus(add(k, m), add(k, n)) == minus(m, n);
-{
-}
-
-ghost method P9()
- ensures forall i, j, k :: minus(minus(i, j), k) == minus(i, add(j, k));
-{
-}
-
-ghost method P10()
- ensures forall m :: minus(m, m) == Zero;
-{
-}
-
-ghost method P11()
- ensures forall xs :: drop(Zero, xs) == xs;
-{
-}
-
-ghost method P12()
- ensures forall n, xs, f :: drop(n, apply(f, xs)) == apply(f, drop(n, xs));
-{
-}
-
-ghost method P13()
- ensures forall n, x, xs :: drop(Suc(n), Cons(x, xs)) == drop(n, xs);
-{
-}
-
-ghost method P14()
- ensures forall xs, ys, p :: filter(p, concat(xs, ys)) == concat(filter(p, xs), filter(p, ys));
-{
-}
-
-ghost method P15()
- ensures forall x, xs :: len(ins(x, xs)) == Suc(len(xs));
-{
-}
-
-ghost method P16()
- ensures forall x, xs :: xs == Nil ==> last(Cons(x, xs)) == x;
-{
-}
-
-ghost method P17()
- ensures forall n :: leq(n, Zero) == True <==> n == Zero;
-{
-}
-
-ghost method P18()
- ensures forall i, m :: less(i, Suc(add(i, m))) == True;
-{
-}
-
-ghost method P19()
- ensures forall n, xs :: len(drop(n, xs)) == minus(len(xs), n);
-{
-}
-
-ghost method P20()
- ensures forall xs :: len(sort(xs)) == len(xs);
-{
- P15(); // use the statement of problem 15 as a lemma
- // ... and manually introduce a case distinction:
- assert forall ys ::
- sort(ys) == Nil ||
- exists z, zs :: sort(ys) == Cons(z, zs);
-}
-
-ghost method P21()
- ensures forall n, m :: leq(n, add(n, m)) == True;
-{
-}
-
-ghost method P22()
- ensures forall a, b, c :: max(max(a, b), c) == max(a, max(b, c));
-{
-}
-
-ghost method P23()
- ensures forall a, b :: max(a, b) == max(b, a);
-{
-}
-
-ghost method P24()
- ensures forall a, b :: max(a, b) == a <==> leq(b, a) == True;
-{
-}
-
-ghost method P25()
- ensures forall a, b :: max(a, b) == b <==> leq(a, b) == True;
-{
-}
-
-ghost method P26()
- ensures forall x, xs, ys :: mem(x, xs) == True ==> mem(x, concat(xs, ys)) == True;
-{
-}
-
-ghost method P27()
- ensures forall x, xs, ys :: mem(x, ys) == True ==> mem(x, concat(xs, ys)) == True;
-{
-}
-
-ghost method P28()
- ensures forall x, xs :: mem(x, concat(xs, Cons(x, Nil))) == True;
-{
-}
-
-ghost method P29()
- ensures forall x, xs :: mem(x, ins1(x, xs)) == True;
-{
-}
-
-ghost method P30()
- ensures forall x, xs :: mem(x, ins(x, xs)) == True;
-{
-}
-
-ghost method P31()
- ensures forall a, b, c :: min(min(a, b), c) == min(a, min(b, c));
-{
-}
-
-ghost method P32()
- ensures forall a, b :: min(a, b) == min(b, a);
-{
-}
-
-ghost method P33()
- ensures forall a, b :: min(a, b) == a <==> leq(a, b) == True;
-{
-}
-
-ghost method P34()
- ensures forall a, b :: min(a, b) == b <==> leq(b, a) == True;
-{
-}
-
-ghost method P35()
- ensures forall xs :: dropWhileAlways(AlwaysFalseFunction(), xs) == xs;
-{
-}
-
-ghost method P36()
- ensures forall xs :: takeWhileAlways(AlwaysTrueFunction(), xs) == xs;
-{
-}
-
-ghost method P37()
- ensures forall x, xs :: not(mem(x, delete(x, xs))) == True;
-{
-}
-
-ghost method P38()
- ensures forall n, xs :: count(n, concat(xs, Cons(n, Nil))) == Suc(count(n, xs));
-{
-}
-
-ghost method P39()
- ensures forall n, x, xs ::
- add(count(n, Cons(x, Nil)), count(n, xs)) == count(n, Cons(x, xs));
-{
-}
-
-ghost method P40()
- ensures forall xs :: take(Zero, xs) == Nil;
-{
-}
-
-ghost method P41()
- ensures forall n, xs, f :: take(n, apply(f, xs)) == apply(f, take(n, xs));
-{
-}
-
-ghost method P42()
- ensures forall n, x, xs :: take(Suc(n), Cons(x, xs)) == Cons(x, take(n, xs));
-{
-}
-
-ghost method P43(p: FunctionValue)
- ensures forall xs :: concat(takeWhileAlways(p, xs), dropWhileAlways(p, xs)) == xs;
-{
-}
-
-ghost method P44()
- ensures forall x, xs, ys :: zip(Cons(x, xs), ys) == zipConcat(x, xs, ys);
-{
-}
-
-ghost method P45()
- ensures forall x, xs, y, ys ::
- zip(Cons(x, xs), Cons(y, ys)) ==
- PCons(Pair.Pair(x, y), zip(xs, ys));
-{
-}
-
-ghost method P46()
- ensures forall ys :: zip(Nil, ys) == PNil;
-{
-}
-
-ghost method P47()
- ensures forall a :: height(mirror(a)) == height(a);
-{
- // proving this theorem requires a previously proved lemma:
- P23();
-}
-
-// ...
-
-ghost method P54()
- ensures forall m, n :: minus(add(m, n), n) == m;
-{
- // the proof of this theorem follows from two lemmas:
- assert forall m, n :: minus(add(n, m), n) == m;
- assert forall m, n :: add(m, n) == add(n, m);
-}
-
-ghost method P65()
- ensures forall i, m :: less(i, Suc(add(m, i))) == True;
-{
- if (*) {
- // the proof of this theorem follows from two lemmas:
- assert forall i, m :: less(i, Suc(add(i, m))) == True;
- assert forall m, n :: add(m, n) == add(n, m);
- } else {
- // a different way to prove it uses the following lemma:
- assert forall x,y :: add(x, Suc(y)) == Suc(add(x,y));
- }
-}
-
-ghost method P67()
- ensures forall m, n :: leq(n, add(m, n)) == True;
-{
- if (*) {
- // the proof of this theorem follows from two lemmas:
- assert forall m, n :: leq(n, add(n, m)) == True;
- assert forall m, n :: add(m, n) == add(n, m);
- } else {
- // a different way to prove it uses the following lemma:
- assert forall x,y :: add(x, Suc(y)) == Suc(add(x,y));
- }
-}
-
-// ---------
-// Here is a alternate way of writing down the proof obligations:
-
-ghost method P1_alt(n: Nat, xs: List)
- ensures concat(take(n, xs), drop(n, xs)) == xs;
-{
-}
-
-ghost method P2_alt(n: Nat, xs: List, ys: List)
- ensures add(count(n, xs), count(n, ys)) == count(n, (concat(xs, ys)));
-{
-}
-
-// ---------
-
-ghost method Lemma_RevConcat(xs: List, ys: List)
- ensures reverse(concat(xs, ys)) == concat(reverse(ys), reverse(xs));
-{
- match (xs) {
- case Nil =>
- assert forall ws :: concat(ws, Nil) == ws;
- case Cons(t, rest) =>
- assert forall a, b, c :: concat(a, concat(b, c)) == concat(concat(a, b), c);
- }
-}
-
-ghost method Theorem(xs: List)
- ensures reverse(reverse(xs)) == xs;
-{
- match (xs) {
- case Nil =>
- case Cons(t, rest) =>
- Lemma_RevConcat(reverse(rest), Cons(t, Nil));
- }
-}
|