aboutsummaryrefslogtreecommitdiff
path: root/seng2011/1/ex6.dfy
diff options
context:
space:
mode:
authorNicolas James <Eele1Ephe7uZahRie@tutanota.com>2025-02-13 18:01:32 +1100
committerNicolas James <Eele1Ephe7uZahRie@tutanota.com>2025-02-13 18:01:32 +1100
commite346bf051fac4ea6b2ad2fa34948029c741bab5e (patch)
treee04502c4aaf8a2e84448b21d34eebe211132eeb2 /seng2011/1/ex6.dfy
parent98cef5e9a772602d42acfcf233838c760424db9a (diff)
Remove seng2011 stuffHEADmain
Diffstat (limited to 'seng2011/1/ex6.dfy')
-rw-r--r--seng2011/1/ex6.dfy32
1 files changed, 0 insertions, 32 deletions
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);
-}