Mercurial > pysmcl
changeset 8:6fde853a56db
proof_burden.py
author | Sigurd Meldgaard <stm@daimi.au.dk> |
---|---|
date | Mon, 18 May 2009 09:57:00 +0200 |
parents | dc2f4211ed1b |
children | 663724fe2fb3 |
files | proof_burden.py |
diffstat | 1 files changed, 53 insertions(+), 0 deletions(-) [+] |
line wrap: on
line diff
--- /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