initial commit

1 files changed, 61 insertions, 0 deletions

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);
+}