--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/proof_burden.py	Mon May 18 09:57:00 2009 +0200
@@ -0,0 +1,53 @@
+import ast
+import inspect
+import pretty_print
+
+
+class FindInvariant(ast.NodeVisitor):
+
+    def visit_Call(self, node):
+        if isinstance(node.func, ast.Name):
+            if node.func.id == "invariant":
+                print "Invariant: " + (node.args[0].s)
+
+
+class ProofBurden(ast.NodeVisitor):
+
+    def __init__(self):
+        self.openings = []
+        self.results = []
+
+    def visit_While(self, node):
+        print "Prove the invariant is true in the initial case"
+        FindInvariant().visit(node)
+        print "Prove the invariant still holds given:"
+        FindInvariant().visit(node)
+        print "And", pretty_print.expr_string(node.test)
+        print "And this code is run:"
+        pretty_print.pprint(node)
+        self.generic_visit(node)
+
+    def visit_Call(self, node):
+        if isinstance(node.func, ast.Name):
+            if node.func.id == "open":
+                self.openings.append(pretty_print.expr_string(node.args[0]))
+            if node.func.id == "result":
+                self.results.append(pretty_print.expr_string(node.args[0]))
+            elif node.func.id == "precondition":
+                print "You can assume: " + (node.args[0].s)
+            elif node.func.id == "invariant":
+                print "Invariant"
+                print (node.args[0].s)
+
+
+def proof_burden(f):
+    b = ProofBurden()
+    b.visit(f)
+    print ("Show that you can compute:")
+    for i in b.openings:
+        print i
+    print ("From:")
+    for i in b.results:
+        print i
+
+    return f