diff options
Diffstat (limited to 'seng2011/1/ex6.dfy')
| -rw-r--r-- | seng2011/1/ex6.dfy | 32 |
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); -} |
