1 files changed, 32 insertions, 0 deletions
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);
+}