Added e.dfy - Dafny. Verifies that the code given is correct.

2018-12-10 23:46:32 +11:00 · 2018-12-10 23:46:32 +11:00 · 03c85557a9
parent d2f145bc00
commit 03c85557a9
1 changed files with 10 additions and 0 deletions
--- a/e.dfy
+++ 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;
+    }
+}