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/ex4.dfy | |
| parent | 98cef5e9a772602d42acfcf233838c760424db9a (diff) | |
Diffstat (limited to 'seng2011/1/ex4.dfy')
| -rw-r--r-- | seng2011/1/ex4.dfy | 15 |
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; -} |
