1 files changed, 15 insertions, 0 deletions
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;
+}