CS计算机代考程序代写 Java data structure python compiler Project 1

Project 1
Verification Condition Generator
Write a Verification Condition Generator (VCG) for our simple imperative language, IMP, using the parser generator ANTLR. Use the Weakest (Liberal) Precondition Predicate Transformer semantics. This allows you to use backward substitution over if-statements. For while-loops, simply print intermediate verification conditions instead of combining them into a single verification condition using universal quantification. Use the ANTLR attribute grammar mechanism as far as possible for generating the verification conditions.
Reading Material
For information on ANTLR and the weakest precondition semantics see:
http://www.antlr.org/ http://en.wikipedia.org/wiki/Predicate_transformer_semantics
ANTLR is written in Java, but can interface with multiple languages. For this project, we will use Python3. For learning how ANTLR works with Java, you can see the Quick Start and Samples instructions on the ANTLR web page. The Makefile I provided contains the commands for running ANTLR and for compiling the Python3 code.
Code Structure
For constructing the verification conditions, you need to build a parse tree data structure representing the verification conditions. Since expressions may be be substituted for variables, and since Boolean expressions are used in assertions, you need to build parse trees for all expressions in the program. When traversing statements, you will then construct the verification conditions using the weakest precondition predicate transformer. This will require building a parse tree for statements as well.
For building parse trees, use the Composite Design Pattern, i.e., use a class hierarchy with an abstract superclass and subclasses corresponding to the different language constructs. E.g., in Java we would define
abstract class Exp { … }
class Ident extends Exp { … }
class IntLit extends Exp { … }
class OpExp extends Exp { … }
// etc.
1

When adding statements, it would be easiest to design expressions and statements as two disjoint class hierarchy as below:
abstract class Exp { … }
class Ident extends Exp { … }
class IntLit extends Exp { … }
class OpExp extends Exp { … }
// etc.
abstract class Stmt { … }
class Assign extends Stmt { … }
// etc.
In a compiler, there would typically be a common superclass on top of these two class hierarchies. This is not necessary for this project, however, since we have different traversals in the two hierarchies. For expressions, you will need traversal methods for printing an expression and for performing a substitution. For statements, you will need a method for the weakest precondition traversal.
Grammar
Use the following grammar for the language IMP (in ANTLR syntax) with start symbol program as a starting point. You may need to restructure the grammar based on how you propagate information using attributes.
program
: assertion statementlist assertion
;
statementlist
: statement
| statement ‘;’ statementlist
;
statement
: ‘skip’
| id ‘:=’ arithexp
| ‘begin’ statementlist ‘end’
| ‘if’ boolterm ‘then’ statement ‘else’ statement
| assertion ‘while’ boolterm ‘do’ statement
| ‘assert’ assertion
;
assertion
: ‘{‘ boolexp ‘}’
;
boolexp
: boolterm
| boolterm ‘=>’ boolterm
| boolterm ‘<=>‘ boolterm
2

| id ‘(‘ arithexplist ‘)’
;
arithexplist
: arithexp
| arithexp ‘,’ arithexplist
;
id
: IDENT
;
integer
: INT
;
IDENT
: [A-Za-z][A-Za-z0-9_]*
;
INT
: [0]|[1-9][0-9]*
;
WS
: [ \r\n\t] -> skip
;
Examples
The input to the VCG is a single Hoare triple. The output is a list of verification conditions, without formatting, one VC per line. E.g., for the input
{ true } x := (2 * 3) * (3 + 4) { x = 42 }
The VCG should print
true => 2*3*(3+4)=42
Surround only the operators =>, <=>, and, and or with one space on each side, print a single space after not, forall, and exists, and print parentheses only if the parent operator has higher precedence (or for right-associative subtractions).
For loops, first print the loop exit condition, then the condition for the loop body, followed by the condition for the code before the loop. E.g., for the input
{ x >= 0 and y > 0 }
q := 0;
r := x;
{ x = q*y + r and 0 <= r and y > 0 }
while r-y >= 0 do begin
4

q := q + 1;
r := r – y end
{ x = q*y + r and 0 <= r and r < y } the output should be: x=q*y+r and 0<=r and y>0 and not r-y>=0 => x=q*y+r and 0<=r and r0 and r-y>=0 => x=(q+1)*y+r-y and y>0 and r-y>=0
x>=0 and y>0 => x=0*y+x and 0<=x and y>0
5

Related Posts