aboutsummaryrefslogtreecommitdiff
path: root/seng2011/1/ex4.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/ex4.dfy
parent98cef5e9a772602d42acfcf233838c760424db9a (diff)
Remove seng2011 stuffHEADmain
Diffstat (limited to 'seng2011/1/ex4.dfy')
-rw-r--r--seng2011/1/ex4.dfy15
1 files changed, 0 insertions, 15 deletions
diff --git a/seng2011/1/ex4.dfy b/seng2011/1/ex4.dfy
deleted file mode 100644
index 900ac48..0000000
--- a/seng2011/1/ex4.dfy
+++ /dev/null
@@ -1,15 +0,0 @@
-method Eval(x:int) returns (r:int)
-requires x > 0;
-ensures r == x * x;
-{
- var y:int := x;
- var z:int := 0;
- while (y >0)
- decreases y
- invariant (y >= 0 && y <= x && z == x * (x - y));
- {
- z := z + x;
- y := y - 1;
- }
- return z;
-}