From 03c85557a99e28f0bad3017563f3d88234148dc8 Mon Sep 17 00:00:00 2001
From: Terry Agapitos <terry@agapitos.com.au>
Date: Mon, 10 Dec 2018 23:46:32 +1100
Subject: [PATCH] Added e.dfy - Dafny. Verifies that the code given is correct.

---
 e.dfy | 10 ++++++++++
 1 file changed, 10 insertions(+)
 create mode 100644 e.dfy

diff --git a/e.dfy b/e.dfy
new file mode 100644
index 0000000..914be8c
--- /dev/null
+++ b/e.dfy
@@ -0,0 +1,10 @@
+method Main() {
+  var e := 9999;
+  while e > 0
+    decreases e
+    invariant e >= 0
+    {
+      print "e";
+      e := e - 1;
+    }
+}
\ No newline at end of file