diff options
| author | Nicolas James <Eele1Ephe7uZahRie@tutanota.com> | 2025-02-13 18:01:32 +1100 |
|---|---|---|
| committer | Nicolas James <Eele1Ephe7uZahRie@tutanota.com> | 2025-02-13 18:01:32 +1100 |
| commit | e346bf051fac4ea6b2ad2fa34948029c741bab5e (patch) | |
| tree | e04502c4aaf8a2e84448b21d34eebe211132eeb2 /seng2011/1/ex6.dfy | |
| parent | 98cef5e9a772602d42acfcf233838c760424db9a (diff) | |
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); -} |
