changeset 354:4f48ec3417bb

Added a test for proof burdens generated from while-loops
author Sigurd Meldgaard <stm@daimi.au.dk>
date Wed, 15 Dec 2010 12:03:21 +0100
parents 31ce799dec84
children 3d0f96c49ec5
files pysmcl/test/unit/test_proof_burden.py
diffstat 1 files changed, 16 insertions(+), 0 deletions(-) [+]
line wrap: on
line diff
--- a/pysmcl/test/unit/test_proof_burden.py	Tue Jul 20 14:54:28 2010 +0200
+++ b/pysmcl/test/unit/test_proof_burden.py	Wed Dec 15 12:03:21 2010 +0100
@@ -90,3 +90,19 @@
  From:
 """
         self.assertEquals(r, expected)
+
+    def test_while(self):
+        r = do_proof_burden(\
+"""def f(c):
+    x = input("x", 1, 0, 1)
+    while(c):
+        y = output(x)
+    result(y)
+""")
+        expected = """For the function: f
+ Show that you can compute:
+  The value of x in line 4
+ From:
+  The value of y in line 5
+"""
+        self.assertEquals(r, expected)