initial use of Eclipse Java AST
some initial CoqOutputter for JavaAST
use more functional approach than visitor pattern (only for method defs now)
find Statement, not any ASTNode
some fixes: return variable, program defs, ... -- factorial parses fine and produces definitions coq like
build class/program (single-class programs so far)
fewer debug output
move method defs up to visitNode of method
slight modifications here
clarify assertion
add method spec output
fix output for reverse - after slight confusion that FieldAccess and QualifiedName are both field reads
emit proof script; add 'this' to arglist if non-static method
fix hardcoded bottoms
emit prog on top level, rather than at the end of each class definition
fewer debug output, umn
fewer debug print, not recording proof directly (different design)
initial cleanup after removal
fix findASTNode to locate either a statement, spec or methoddeclaration
more work on output... slowly getting somewhere