From 93747eaf7a97c2e443853b05c4e6519e8fc197e9 Mon Sep 17 00:00:00 2001 From: WGAVermeer Date: Tue, 17 Mar 2026 11:38:06 +0100 Subject: [PATCH] worked on chapter 5 --- chap_5/e5_1.dfy | 34 ++++++++++++ chap_5/e5_3.dfy | 83 ++++++++++++++++++++++++++++ chap_5/e5_5.dfy | 0 chap_5/e5_6.dfy | 65 ++++++++++++++++++++++ chap_5/e5_7.dfy | 90 +++++++++++++++++++++++++++++++ chap_5/e5_7_2.dfy | 134 ++++++++++++++++++++++++++++++++++++++++++++++ chap_5/e5_8.dfy | 0 7 files changed, 406 insertions(+) create mode 100644 chap_5/e5_1.dfy create mode 100644 chap_5/e5_3.dfy create mode 100644 chap_5/e5_5.dfy create mode 100644 chap_5/e5_6.dfy create mode 100644 chap_5/e5_7.dfy create mode 100644 chap_5/e5_7_2.dfy create mode 100644 chap_5/e5_8.dfy diff --git a/chap_5/e5_1.dfy b/chap_5/e5_1.dfy new file mode 100644 index 0000000..fda169e --- /dev/null +++ b/chap_5/e5_1.dfy @@ -0,0 +1,34 @@ +function More(x: int): int { +if x <= 0 then 1 else More(x - 2) + 3 +} + +lemma {:induction false} Increasing(x: int) + decreases x + ensures x < More(x) +{ // 0: + // x is an int, x can be any value. + if x <= 0 { // 1: x <= 0 Therefore More(x) == 1 => x <= 0 < 1 == More(x) => x < More(x) + } else { // 2: Work back to basecase, x > 0 ==> repeated x - 2 eventually enters basecase. + Increasing(x-2); + } +} + +method ExampleLemmaUse(a: int) { + // var b := More(a); + // Increasing(a); + // Increasing(b); + // var c := More(b); + // assert 2 <= c - a; + + Increasing(a); // this call is along all control paths + var b := More(a); + Increasing(b); + b := More(b); + // Increasing(b); + // if a < 1000 { + // Increasing(More(a)); // we learn More(a) < More(More(a)) + // // only here, i.e., when a < 1000 + // assert 2 <= b - a; // this verifies + // } + assert 2 <= b - a; // this does not verify +} diff --git a/chap_5/e5_3.dfy b/chap_5/e5_3.dfy new file mode 100644 index 0000000..f83b8af --- /dev/null +++ b/chap_5/e5_3.dfy @@ -0,0 +1,83 @@ +lemma ex_1a(x: int, y: int) + ensures 5*x - 3 * (y + x) == 2*x - 3*y +{ + calc { + 5 * x -3 * (y + x); + == // Distributivity of Multiplication + 5 * x -3 * y - 3 * x; + == // Commutativity + 5 * x - 3 * x - 3 * y; + == // Addition + 2 * x - 3*y; + } +} +lemma ex_1b(x: int, y: int) + ensures 2 * (x + 4*y + 7) - 10 == 2*x + 8*y + 4 +{ + calc { + 2 * (x + 4*y + 7) - 10; + == // Distributivity of Multiplication + 2 * x + 2 * 4 * y + 2 * 7 - 10; + == // Multiplication of integers + 2 * x + 8 * y + 14 - 10; + == // Addition of integers + 2*x + 8*y + 4; + } +} + +lemma ex_1c(x: int, y: int) + ensures 7*x + 5 < (x + 3) * (x + 4) + { + calc { + 7*x + 5; + < + 7*x + 12; + <= {assert x * x >= 0;} + 7*x + 12 + x * x; + == + x * x + 3 * x + 4 * x + 12; + == + (x + 3) * (x + 4); + } +} + +// E5.6 + +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)) +} + +lemma {:induction false} IncreasingAck(n: nat) + ensures Ack(1, n) == n + 2 +{ + if n == 0 { + calc { + Ack(1, n); + == + Ack(0, 1); + == + 2; + } + } else { + calc { + Ack(1, n); + == // last else branch of Ack + Ack(0, Ack(1, n - 1)); + == { IncreasingAck(n - 1);} + Ack(0, n - 1 + 2); + == + Ack(0, n + 1); + == + n + 1 + 1; + == + n + 2; + } + } +} diff --git a/chap_5/e5_5.dfy b/chap_5/e5_5.dfy new file mode 100644 index 0000000..e69de29 diff --git a/chap_5/e5_6.dfy b/chap_5/e5_6.dfy new file mode 100644 index 0000000..05a1c0d --- /dev/null +++ b/chap_5/e5_6.dfy @@ -0,0 +1,65 @@ +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) +{ + if x == y { + } else if x == 0 { + MultCommutative(x, y - 1); + } else if y < 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); + == + x + y - 1 + Mult(y - 1, x - 1); + == + x - 1 + y + Mult(y - 1, x - 1); + == {MultCommutative(x - 1, y - 1);} + x - 1 + y + Mult(x - 1, y - 1); + == + y + Mult(x - 1, y); + == {MultCommutative(x - 1, y);} + y + Mult(y, x - 1); + == + Mult(y, x); + + } + } +} + +lemma {:induction false} MultCommutative'(x: nat, y: nat) + ensures Mult(x, y) == Mult(y, x) + decreases x + y +{ + if x == y {// Trivial + } else if x == 0 { + MultCommutative'(x, y - 1); + } else if y == 0 { + MultCommutative'(y, x - 1); + } else { // x < y + calc { + Mult(x, y); + == // def. Mult + x + Mult(x, y - 1); + == {MultCommutative'(y - 1, x);} + x + Mult(y - 1, x) ; + == // def. Mult + x + y - 1 + Mult(y - 1, x - 1); + == {MultCommutative'(y - 1, x -1);} + y + x - 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); + } + } +} \ No newline at end of file diff --git a/chap_5/e5_7.dfy b/chap_5/e5_7.dfy new file mode 100644 index 0000000..a6cbc37 --- /dev/null +++ b/chap_5/e5_7.dfy @@ -0,0 +1,90 @@ +datatype Tree = Leaf(data: T) + | Node(left: Tree, right: Tree) + +function Mirror(t: Tree): Tree { + match t + case Leaf(_) => t + case Node(left, right) + => Node(Mirror(right), Mirror(left)) +} + +lemma {:induction false} MirrorMirror(t: Tree) + ensures Mirror(Mirror(t)) == t +{ + match t + case Leaf(_) => + // trivial + case Node(left, right) => + calc { + Mirror(Mirror(Node(left, right))); + == + Mirror(Node(Mirror(right), Mirror(left))); + == + Node(Mirror(Mirror(left)),Mirror(Mirror(right))); + == {MirrorMirror(left); MirrorMirror(right);} + Node(left, right); + } +} + +function Size(t: Tree): nat { + match t + case Leaf(_) => 1 + case Node(left, right) => Size(left) + Size(right) +} + +lemma {:induction false} MirrorSize(t: Tree) + ensures Size(Mirror(t)) == Size(t) +{ + match t + case Leaf(_) => + case Node(left, right) => + calc { + Size(Mirror(Node(left, right))); + == // def. Mirror + Size(Node(Mirror(right), Mirror(left))); + == // def. Size + Size(Mirror(right)) + Size(Mirror(left)); + == {MirrorSize(right); MirrorSize(left);} + Size(right) + Size(left); + == // arithmatic + Size(left) + Size(right); + == // def. size + Size(Node(left, right)); + } +} + +method test() { + assert multiset([1, 2]) == multiset([2, 1]); +} + +// method Seperate(a: array, key: int) returns (pivot: nat) +// requires a.Length >= 1 +// modifies a +// ensures multiset(a[..]) == multiset(old(a[..])) +// ensures 0 <= pivot <= a.Length +// ensures forall i | 0 <= i < pivot :: a[i] <= key +// ensures forall i | pivot <= i < a.Length :: key < a[i] +// { +// var lo: nat, hi: nat := 0, a.Length - 1; +// while lo < hi +// decreases hi - lo +// invariant 0 <= lo <= hi < a.Length +// invariant forall i | 0 <= i < lo :: a[i] <= key +// invariant forall i | hi < i < a.Length :: key < a[i] +// invariant multiset(a[..]) == multiset(old(a[..])) +// { +// if a[lo] <= key { +// lo := lo + 1; +// } else if key < a[hi] { +// hi := hi - 1; +// } else { +// assert a[lo] in multiset(a[..]); +// assert a[hi] in multiset(a[..]); +// a[lo], a[hi] := a[hi], a[lo]; +// assert a[lo] in multiset(a[..]); +// assert a[hi] in multiset(a[..]); +// lo := lo + 1; +// } +// } +// pivot := lo; +// } diff --git a/chap_5/e5_7_2.dfy b/chap_5/e5_7_2.dfy new file mode 100644 index 0000000..6aa5add --- /dev/null +++ b/chap_5/e5_7_2.dfy @@ -0,0 +1,134 @@ +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)) +} + +lemma {:induction false} ReverseColorsInvolution(t: BYTree) + ensures ReverseColors(ReverseColors(t)) == t +{ + match t + case BlueLeaf => + case YellowLeaf => + case Node(left, right) => + calc { + ReverseColors(ReverseColors(Node(left,right))); + == + ReverseColors(Node(ReverseColors(left), ReverseColors(right))); + == + Node(ReverseColors(ReverseColors(left)), ReverseColors(ReverseColors(right))); + == {ReverseColorsInvolution(left); ReverseColorsInvolution(right);} + Node(left, right); + } +} + +function LeafCount(t: BYTree): nat +{ + match t + case BlueLeaf | YellowLeaf => 1 + case Node(left, right) => LeafCount(left) + LeafCount(right) +} + +lemma {:induction false} ReversePreserveLeafCount(t: BYTree) + ensures LeafCount(ReverseColors(t)) == LeafCount(t) + decreases t +{ + match t + case BlueLeaf => + case YellowLeaf => + case Node(left, right) => + calc { + LeafCount(ReverseColors(Node(left, right))); + == + LeafCount(Node(ReverseColors(left), ReverseColors(right))); + == + LeafCount(ReverseColors(left)) + LeafCount(ReverseColors(right)); + == {ReversePreserveLeafCount(left); ReversePreserveLeafCount(right);} + LeafCount(left) + LeafCount(right); + == + LeafCount(Node(left, right)); + } +} + +function Oceanize(t: BYTree): BYTree { + match t + case BlueLeaf | YellowLeaf => BlueLeaf + case Node(left, right) => Node(Oceanize(left), Oceanize(right)) +} + +lemma {:induction false} IdempotentOceanize(t: BYTree) + ensures Oceanize(t) == Oceanize(Oceanize(t)) + decreases t +{ + match t + case BlueLeaf => + calc { + Oceanize(Oceanize(BlueLeaf)); + == + Oceanize(BlueLeaf); + == + BlueLeaf; + } + case YellowLeaf => + calc { + Oceanize(Oceanize(YellowLeaf)); + == + Oceanize(BlueLeaf); + == + BlueLeaf; + == + Oceanize(YellowLeaf); + } + + case Node(left, right) => + calc { + Oceanize(Node(left, right)); + == + Node(Oceanize(left), Oceanize(right)); + == {IdempotentOceanize(left); IdempotentOceanize(right);} + Node(Oceanize(Oceanize(left)), Oceanize(Oceanize(right))); + == + Oceanize(Node(Oceanize(left), Oceanize(right))); + == + Oceanize(Oceanize(Node(left,right))); + } +} + +function BlueCount(t: BYTree): nat { + match t + case BlueLeaf => 1 + case YellowLeaf => 0 + case Node(left, right) => + BlueCount(left) + BlueCount(right) +} + +lemma {:induction false} BlueCountBound(t: BYTree) + ensures BlueCount(t) <= BlueCount(Oceanize(t)) +{ + match t + case BlueLeaf => + calc { + BlueCount(BlueLeaf); + == + BlueCount(Oceanize(BlueLeaf)); + } + case YellowLeaf => + calc { + BlueCount(YellowLeaf); + < + BlueCount(BlueLeaf); + == + BlueCount(Oceanize(YellowLeaf)); + } + case Node(left, right) => + calc { + BlueCount(Node(left, right)); + == + BlueCount(left) + BlueCount(right); + <= {BlueCountBound(left); BlueCountBound(right);} + BlueCount(Oceanize(left)) + BlueCount(Oceanize(right)); + } +} \ No newline at end of file diff --git a/chap_5/e5_8.dfy b/chap_5/e5_8.dfy new file mode 100644 index 0000000..e69de29