Finished Chapter 4

chap_3/e3_2.dfy

@@ -0,0 +1,17 @@
+function M(x: int, b: bool): int 
+    decreases !b
+{
+    if b then x else M(x + 25, true) 
+}
+
+function N(x: int, y: int, b: bool): int 
+    decreases x, b
+{
+    if x <= 0 || y <= 0 then
+        x + y
+    else if b then
+        N(x, y + 3, !b)
+    else
+        N(x - 1, y, true)
+}
+

chap_3/e3_3.dfy

@@ -0,0 +1,105 @@
+method Study(n: nat, h: nat)
+decreases n * 201 + h
+{
+    if h != 0 {
+        // first, study for an hour, and then:
+        Study(n, h - 1);
+    } else if n == 0 {
+        // you just finished course 0 - woot woot, graduation time!
+    } else {
+        // find out how much studying is needed for the next course
+        
+        var hours := RequiredStudyTime(n - 1);
+        // get started with course n-1:
+        Study(n - 1, hours);
+    }
+}
+
+method RequiredStudyTime(c: nat) returns (hours: nat)
+ensures hours <= 200
+
+method Outer(a: nat)
+    decreases a
+{
+    if a != 0 {
+        var b := RequiredStudyTime(a - 1);
+        Inner(a, b);
+    }
+}
+
+method Inner(a: nat, b: nat)
+    requires 1 <= a
+    decreases a, b
+{
+    if b == 0 {
+        Outer(a - 1);
+    } else {
+        Inner(a, b - 1);
+    }
+}
+
+method Outer'(a: nat)
+    decreases a, 0, 0
+{
+    if a != 0 {
+        var b := RequiredStudyTime(a - 1);
+        Inner'(a - 1, b);
+    }
+}
+method Inner'(a: nat, b: nat) 
+    decreases a, b, 1
+{
+    if b == 0 {
+        Outer'(a);
+    } else {
+        Inner'(a, b - 1);
+    }
+}
+
+function F(n: nat): nat 
+decreases n, 1
+{
+    if n == 0 then 1 else n - M(F(n - 1))
+}
+
+function M(n: nat): nat 
+decreases n, 0
+{
+    if n == 0 then 0 else n - F(M(n - 1))
+}
+
+method StudyPlan(n: nat)
+    requires n <= 40
+    decreases 40 - n, 201
+{
+    if n == 40 {
+        // done
+    } else {
+        var hours := RequiredStudyTime(n);
+        Learn(n, hours);
+    }
+}
+
+method Learn(n: nat, h: nat)
+    requires n < 40
+    decreases 40 - n, h
+{
+    if h == 0 {
+        StudyPlan(n + 1);
+    } else {
+        Learn(n, h - 1);
+    }
+}
+
+function F'(x: nat, y: nat): int 
+    decreases x % 2, if x % 2 == 0 then 1000 - x else x
+{
+    if 1000 <= x then
+        x + y
+    else if x % 2 == 0 then
+        F'(x + 2, y + 1)
+    else if x < 6 then
+        F'(2 * y, y)
+    else
+        F'(x - 4, y + 3)
+}

chap_4/e4_1.dfy

@@ -0,0 +1,96 @@
+datatype BYTree = BlueLeaf | YellowLeaf | Node(left: BYTree, right: BYTree)
+
+function ReverseColors(t: BYTree): BYTree {
+    match t
+    case BlueLeaf => YellowLeaf
+    case YellowLeaf => BlueLeaf 
+    case Node(left, right) => BYTree.Node(ReverseColors(left), ReverseColors(right))
+}
+
+method TestReverseColors() {
+    var a := BYTree.Node(BlueLeaf, BYTree.Node(BlueLeaf, YellowLeaf));
+    var b := BYTree.Node(YellowLeaf, BYTree.Node(YellowLeaf, BlueLeaf));
+    assert ReverseColors(a) == b;
+    assert ReverseColors(b) == a;
+
+    var c := BYTree.Node(BYTree.Node(YellowLeaf, BlueLeaf), BlueLeaf);
+    var d := BYTree.Node(BYTree.Node(BlueLeaf, YellowLeaf), YellowLeaf);
+    assert ReverseColors(c) == d;
+    assert ReverseColors(d) == c;
+
+    var e := BlueLeaf;
+    assert ReverseColors(e) != e;
+}
+
+function Oceanize(t: BYTree): BYTree {
+    match t
+        case BlueLeaf | YellowLeaf => BlueLeaf
+        case Node(left, right) => BYTree.Node(Oceanize(left), Oceanize(right))
+}
+
+method testOceanize() {
+    var a := BYTree.Node(BlueLeaf, YellowLeaf);
+    var b := BYTree.Node(BlueLeaf, BlueLeaf);
+    assert Oceanize(a) == b; 
+}
+
+function LeftDepth(t: BYTree): nat {
+    if t.BlueLeaf? || t.YellowLeaf? then 1
+    else 1 + LeftDepth(t.left)
+}
+
+predicate HasLeftTreeMatch(t: BYTree, u: BYTree) {
+    match t
+    case Node(left, right) => left == u // || HasLeftTree(left, u) || HasLeftTree(right, u)
+    case BlueLeaf => false
+    case YellowLeaf => false
+}
+
+predicate HasLeftTreeCon(t: BYTree, u: BYTree) {
+    if t.BlueLeaf? then false
+    else if t.YellowLeaf? then false
+    else t.left == u
+}
+
+predicate HLT(t: BYTree, u: BYTree) {
+    HasLeftTreeMatch(t, u) && HasLeftTreeCon(t, u)
+}
+
+method testHasLeftTree() {
+    var a := BYTree.Node(BlueLeaf, YellowLeaf);
+    var b := BlueLeaf;
+    var c := BYTree.Node(a, b);
+
+    assert HLT(a, b);
+    assert !HLT(b, a);
+    assert HLT(c, a);
+    assert !HLT(c, b);
+}
+
+datatype Color = Blue | Yellow | Green | Red
+
+datatype ColoredTree = Leaf(Color) | Node(ColoredTree, ColoredTree)
+
+predicate IsSwedishColoredTree(t: ColoredTree) {
+    match t {
+    case Leaf(Color) => 
+        match Color {
+        case Blue => true
+        case Yellow => true
+        case Green => false
+        case Red => false
+        }
+    case Node(left, right) => IsSwedishColoredTree(left) && IsSwedishColoredTree(right)
+    }
+}
+
+method testIsSwedischColoredTree() {
+    var a := ColoredTree.Node(Leaf(Blue), Leaf(Green));
+    assert !IsSwedishColoredTree(a);
+
+    var b := ColoredTree.Node(Leaf(Blue), Leaf(Yellow));
+    assert IsSwedishColoredTree(b);
+}
+
+
+

chap_4/e4_5.dfy

@@ -0,0 +1,9 @@
+datatype Tree<T> = Leaf(data: T)
+| Node(left: Tree<T>, right: Tree<T>)
+
+function Mirror<T>(t: Tree<T>): Tree<T> {
+    match t
+    case Leaf(_) => t
+    case Node(left, right) => Node(Mirror(right), Mirror(left))
+}
+

chap_4/e4_6.dfy

@@ -0,0 +1,137 @@
+datatype Expr = Const(nat) | Var(string) | Node(op: Op, args: List<Expr>)
+
+datatype Op = Add | Mul
+
+datatype List<T> = Nil | Cons(head: T, tail: List<T>)
+
+function Eval(e: Expr, env: map<string, nat>): nat 
+    requires GoodEnv(e, env)
+{
+    match e
+    case Const(c) => c
+    case Var(s) => env[s]
+    case Node(op, args) => EvalList(op, args, env)
+}
+
+/* E.4.9 => The default decreases clause use lexicographical ordering of the arguments.
+This implies the following decreases clause:
+    decreases op, args, env
+
+But as "op" is either Add or Mul which and does not have fixed order in a list<Expr>
+it jumps around.
+for example 10 * 5 + 3 * 10. 
+=> Node(Mul, Cons(Const(10), Cons()))
+
+*/
+
+function EvalList(op: Op, args: List<Expr>,
+env: map<string, nat>): nat
+decreases args
+requires GoodEnvList(args, env)
+{
+match args
+    case Nil =>
+    (match op case Add => 0 case Mul => 1)
+    case Cons(e, tail) =>
+        var v0, v1 := Eval(e, env), EvalList(op, tail, env);
+        match op
+            case Add => v0 + v1
+            case Mul => v0 * v1
+}
+
+predicate GoodEnv(e: Expr, env: map<string, nat>) {
+    match e
+    case Const(_) => true
+    case Var(s) => s in env.Keys
+    case Node(_, args) => GoodEnvList(args, env)
+}
+
+predicate GoodEnvList(args: List<Expr>, env: map<string, nat>)
+{
+    match args
+    case Nil => true
+    case Cons(e, tail) => GoodEnv(e, env) && GoodEnvList(tail, env)
+}
+
+
+ghost method TestGoodEnvExtensive() {
+
+    // ---------- Simple constants ----------
+    var c1 := Const(5);
+    assert GoodEnv(c1, map[]);
+
+    // ---------- Single variable ----------
+    var v1 := Var("x");
+    var env1 := map["x" := 10];
+    assert GoodEnv(v1, env1);
+
+    var env2 := map["y" := 10];
+    assert !GoodEnv(v1, env2);
+
+    // ---------- Simple Node ----------
+    var e1 := Node(Add, Cons(Const(2), Cons(Const(3), Nil)));
+    assert GoodEnv(e1, map[]);
+
+    // ---------- Node with variable ----------
+    var e2 := Node(Add, Cons(Var("x"), Cons(Const(4), Nil)));
+    var env3 := map["x" := 7];
+    assert GoodEnv(e2, env3);
+
+    var env4 := map["y" := 7];
+    assert !GoodEnv(e2, env4);
+
+    // ---------- Multiple variables ----------
+    var e3 :=
+        Node(Mul,
+            Cons(Var("x"),
+            Cons(Var("y"),
+            Cons(Const(5), Nil))));
+
+    var env5 := map["x" := 1, "y" := 2];
+    assert GoodEnv(e3, env5);
+
+    var env6 := map["x" := 1];
+    assert !GoodEnv(e3, env6);
+
+    // ---------- Nested nodes ----------
+    var nested :=
+        Node(Add,
+            Cons(
+                Node(Mul,
+                    Cons(Var("x"),
+                    Cons(Const(3), Nil))),
+            Cons(
+                Node(Add,
+                    Cons(Const(1),
+                    Cons(Var("y"), Nil))),
+            Nil)));
+
+    var env7 := map["x" := 2, "y" := 4];
+    assert GoodEnv(nested, env7);
+
+    var env8 := map["x" := 2];
+    assert !GoodEnv(nested, env8);
+
+    // ---------- Deep tree ----------
+    var deep :=
+        Node(Add,
+            Cons(
+                Node(Add,
+                    Cons(
+                        Node(Mul,
+                            Cons(Var("a"),
+                            Cons(Const(2), Nil))),
+                    Cons(Const(3), Nil))),
+            Cons(
+                Node(Mul,
+                    Cons(Const(4),
+                    Cons(Var("b"), Nil))),
+            Nil)));
+
+    var env9 := map["a" := 1, "b" := 5];
+    assert GoodEnv(deep, env9);
+
+    var env10 := map["a" := 1];
+    assert !GoodEnv(deep, env10);
+
+}