Mercurial > pysmcl

changeset 223:092189a2b2df

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
proof_burden: made it a stand-alone program
author Sigurd Meldgaard <stm@daimi.au.dk>
date Wed, 23 Dec 2009 14:41:29 +0100
parents 83996d1a8c4d
children f6a900294f62
files pysmcl/proof_burden.py
diffstat 1 files changed, 32 insertions(+), 19 deletions(-) [+]
line wrap: on
line diff
--- a/pysmcl/proof_burden.py	Wed Dec 23 14:40:26 2009 +0100
+++ b/pysmcl/proof_burden.py	Wed Dec 23 14:41:29 2009 +0100
@@ -17,36 +17,49 @@
         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", pysmcl.pretty_print.expr_string(node.test)
-        print "And this code is run:"
-        pysmcl.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(pysmcl.pretty_print.expr_string(node.args[0]))
+            if node.func.id == "output":
+                self.openings.append(node.args[0])
             if node.func.id == "result":
-                self.results.append(pysmcl.pretty_print.expr_string(node.args[0]))
+                self.results.append(node.args[0])
             elif node.func.id == "precondition":
-                print "You can assume: " + (node.args[0].s)
+                print "  You can assume: " + (node.args[0].s)
             elif node.func.id == "invariant":
-                print "Invariant"
+                print " Invariant"
                 print (node.args[0].s)
 
 
 def proof_burden(f):
     b = ProofBurden()
+    print "For the function: " + f.name
     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
+    if b.openings!=[]:
+        print (" Show that you can compute:")
+        for i in b.openings:
+            print("  The value of " + pysmcl.pretty_print.expr_string(i)
+                  + " in line " + str(i.lineno))
+        print (" From:")
+        for i in b.results:
+            print("  The value of " + pysmcl.pretty_print.expr_string(i)
+                  + " in line " + str(i.lineno))
+    else:
+        print " Nothing has to be proved"
+    return f
 
-    return f
+def main():
+    from optparse import OptionParser
+    parser = OptionParser(usage="Usage: %prog [options] pysmcl_program")
+    (options, args) = parser.parse_args()
+    if len(args) < 1:
+        parser.error("Not enough arguments")
+    module = ast.parse(file(args[0]).read())
+    for i in module.body:
+        if isinstance(i, ast.FunctionDef):
+            proof_burden(i)
+
+    
+if __name__ == "__main__":
+    main()