From 98cef5e9a772602d42acfcf233838c760424db9a Mon Sep 17 00:00:00 2001
From: Nicolas James <Eele1Ephe7uZahRie@tutanota.com>
Date: Thu, 13 Feb 2025 18:00:17 +1100
Subject: initial commit

---
 seng2011/1/ex4.dfy | 15 +++++++++++++++
 1 file changed, 15 insertions(+)
 create mode 100644 seng2011/1/ex4.dfy

(limited to 'seng2011/1/ex4.dfy')

diff --git a/seng2011/1/ex4.dfy b/seng2011/1/ex4.dfy
new file mode 100644
index 0000000..900ac48
--- /dev/null
+++ b/seng2011/1/ex4.dfy
@@ -0,0 +1,15 @@
+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;
+}
-- 
cgit v1.2.3