initial commit

3 files changed, 108 insertions, 0 deletions

diff --git a/seng2011/1/ex4.dfy b/seng2011/1/ex4.dfy
new file mode 100644
index 0000000..900ac48
--- /dev/null
+++ b/seng2011/1/ex4.dfy
@@ -0,0 +1,15 @@
+method Eval(x:int) returns (r:int)
+requires x > 0;
+ensures r == x * x;
+{
+    var y:int := x;
+    var z:int := 0;
+    while (y >0)
+        decreases y
+        invariant (y >= 0 && y <= x && z == x * (x - y));
+    {
+        z := z + x;
+        y := y - 1;
+    }
+    return z;
+}
diff --git a/seng2011/1/ex5.dfy b/seng2011/1/ex5.dfy
new file mode 100644
index 0000000..4365042
--- /dev/null
+++ b/seng2011/1/ex5.dfy
@@ -0,0 +1,61 @@
+predicate exist1(a: array<int>, x:int) 
+    reads a;
+{
+    multiset(a[..])[x] == 1
+}
+
+predicate exist2(a: array<int>, x:int) 
+    reads a;
+{
+    multiset(a[..])[x] >= 2
+}
+
+predicate tail(a: array<int>) 
+    reads a;
+{
+    forall i : int :: 0 <= i < a.Length ==> 
+        (a[i] != 0 || multiset(a[i..])[0] == a.Length - i)
+}
+
+method test1() 
+{
+    var a := new int[3][1, 2, 2];
+    assert a[..] == [1, 2, 2];
+
+    assert !exist1(a, 0);
+    assert exist1(a, 1);
+    assert !exist1(a, 2);
+}
+
+method test2() 
+{
+    var a := new int[6][1, 2, 2, 3, 3, 3];
+    assert a[..] == [1, 2, 2, 3, 3, 3];
+
+    assert !exist2(a, 0);
+    assert !exist2(a, 1);
+    assert exist2(a, 2);
+    assert exist2(a, 3);
+}
+
+method test3()
+{
+    var a := new int[4][1, 2, 3, 0];
+    assert a[..] == [1, 2, 3, 0];
+    assert tail(a);
+
+    // "no zeros is vacuously true"
+    var b := new int[4][1, 2, 3, 4];
+    assert b[..] == [1, 2, 3, 4];
+    assert tail(b);
+
+    var c := new int[6][1, 2, 3, 0, 5, 6];
+    assert c[..] == [1, 2, 3, 0, 5, 6];
+    assert c[3..] == [0, 5, 6];
+    assert !tail(c);
+
+    var d := new int[6][1, 2, 0, 0, 5, 0];
+    assert d[..] == [1, 2, 0, 0, 5, 0];
+    assert d[2..] == [0, 0, 5, 0];
+    assert !tail(d);
+}
diff --git a/seng2011/1/ex6.dfy b/seng2011/1/ex6.dfy
new file mode 100644
index 0000000..3575315
--- /dev/null
+++ b/seng2011/1/ex6.dfy
@@ -0,0 +1,32 @@
+method Ceiling7(n:nat) returns (k:nat)
+requires n >= 0;
+ensures k == n - (n % 7);
+{
+    return n - (n % 7);
+}
+
+method test() {
+    var res := Ceiling7(0);
+    assert(res == 0);
+
+    res := Ceiling7(1);
+    assert(res == 0);
+
+    res := Ceiling7(6);
+    assert(res == 0);
+
+    res := Ceiling7(7);
+    assert(res == 7);
+
+    res := Ceiling7(8);
+    assert(res == 7);
+
+    res := Ceiling7(41);
+    assert(res == 35);
+
+    res := Ceiling7(42);
+    assert(res == 42);
+
+    res := Ceiling7(43);
+    assert(res == 42);
+}