Remove seng2011 stuffHEADmain

3 files changed, 0 insertions, 108 deletions

diff --git a/seng2011/1/ex4.dfy b/seng2011/1/ex4.dfy
deleted file mode 100644
index 900ac48..0000000
--- a/seng2011/1/ex4.dfy
+++ /dev/null
@@ -1,15 +0,0 @@
-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
deleted file mode 100644
index 4365042..0000000
--- a/seng2011/1/ex5.dfy
+++ /dev/null
@@ -1,61 +0,0 @@
-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
deleted file mode 100644
index 3575315..0000000
--- a/seng2011/1/ex6.dfy
+++ /dev/null
@@ -1,32 +0,0 @@
-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);
-}