From 98cef5e9a772602d42acfcf233838c760424db9a Mon Sep 17 00:00:00 2001 From: Nicolas James Date: Thu, 13 Feb 2025 18:00:17 +1100 Subject: initial commit --- seng2011/1/ex6.dfy | 32 ++++++++++++++++++++++++++++++++ 1 file changed, 32 insertions(+) create mode 100644 seng2011/1/ex6.dfy (limited to 'seng2011/1/ex6.dfy') 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); +} -- cgit v1.2.3