changeset 340:2aef103ea501

test_proof_burden: make some basic tests af the proof_burden functionality
author Sigurd Meldgaard <stm@daimi.au.dk>
date Wed, 07 Jul 2010 13:22:52 +0200
parents a7d868a5577a
children f02368b0944e
files pysmcl/test/unit/test_proof_burden.py
diffstat 1 files changed, 57 insertions(+), 0 deletions(-) [+]
line wrap: on
line diff
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/pysmcl/test/unit/test_proof_burden.py	Wed Jul 07 13:22:52 2010 +0200
@@ -0,0 +1,57 @@
+import unittest
+import StringIO
+
+from pysmcl.proof_burden import proof_burden
+
+from pysmcl.ast_wrapper import parse
+
+
+def do_proof_burden(program_string):
+    prog = parse(program_string)
+    output = StringIO.StringIO()
+    proof_burden(prog.body[0], output)
+    return output.getvalue()
+
+
+class ProofBurdenTest(unittest.TestCase):
+
+    def test_simple_proof(self):
+        r = do_proof_burden(\
+"""def f():
+    x = input("x",1,0,1)
+    y = output(x)
+    result(y)
+""")
+        expected = """For the function: f
+ Show that you can compute:
+  The value of x in line 3
+ From:
+  The value of y in line 4
+"""
+        self.assertEquals(r, expected)
+
+    def test_nothing(self):
+        r = do_proof_burden(\
+"""def f():
+    y = input("x",1,0,1)
+    result(y)
+""")
+        expected = """For the function: f
+ Nothing has to be proved
+"""
+        self.assertEquals(r, expected)
+
+    def test_input(self):
+        r = do_proof_burden(\
+"""def f():
+    y = input("x",1,0,1)
+    y = output(x)
+    z = input("a",1,0,1)
+    result(y)
+""")
+        expected = """For the function: f
+ Show that you can compute:
+  The value of x in line 3
+ From:
+"""
+        self.assertEquals(r, expected)