From e346bf051fac4ea6b2ad2fa34948029c741bab5e Mon Sep 17 00:00:00 2001
From: Nicolas James <Eele1Ephe7uZahRie@tutanota.com>
Date: Thu, 13 Feb 2025 18:01:32 +1100
Subject: Remove seng2011 stuff

---
 seng2011/1/ex5.dfy | 61 ------------------------------------------------------
 1 file changed, 61 deletions(-)
 delete mode 100644 seng2011/1/ex5.dfy

(limited to 'seng2011/1/ex5.dfy')

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);
-}
-- 
cgit v1.2.3