Java代写：CS4103 Verification Condition Generator

使用ANTLR代写一个Verification Condition Generator，实现语法的解析校验。

Requirement

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 verfication conditions.

Reading Material

For information on ANTLR and the weakest precondition semantics see:
http://www.antlr.org/
https://en.wikipedia.org/wiki/Predicate_transformer_semantics

For using ANTLR, make sue you put antlr-4.6-complete.jar onto your CLASSPATH. For details, see the Quick Start and Samples instructions on the ANTLR web page or read the Makefile I provided.

Code Structure

For constructing the verifications 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 also 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 may or may not require building the parse trees 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.,

abstract class Node { ... }
class Ident extends Node { ... }
class IntLit extends Node { ... }
class BinOp extends Node { ... }
// etc.

For expressions, you will need methods for printing the expression and for performing a substitution. If you decide to represent statements using parse tree nodes as well, it would be best to group expressions and statements as two separate parts of the class hierarchy, since you will likely need different methods, e.g.,

abstract class Node { ... }
abstract class Exp extends Node { ... }
abstract class Stm extends Node { ... }
class Ident extends Exp { ... }
class IntLit extends Exp { ... }
class BinOp extends Exp { ... }
// etc.
class Assign extends Stm { ... }
// etc.

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
    | statementlist ';' statement
    ;

statement
    : 'skip'
    | id ':=' arithexp
    | 'begin' statementlist 'end'
    | 'if' boolterm 'then' statement 'else' statement
    | assertion 'while' boolterm 'do' statement
    | 'assert' assertion
    ;

assertion
    : '{' quantexp '}'
    ;

quantexp
    : boolexp
    | 'forall' id '.' boolexp
    | 'exists' id '.' boolexp
    ;

boolexp
    : boolterm
    | boolterm '=>' boolterm
    | boolterm '<=>' boolterm
    ;

boolterm
    : boolterm2
    | boolterm 'or' boolterm2
    ;

boolterm2
    : boolfactor
    | boolterm2 'and' boolfactor
    ;

boolfactor
    : 'true'
    | 'false'
    | compexp
    | 'not' quantexp
    | '(' quantexp ')'
    ;

compexp
    : arithexp '<' arithexp
    | arithexp '<=' arithexp
    | arithexp '=' arithexp
    | arithexp '!=' arithexp
    | arithexp '>=' arithexp
    | arithexp '>' arithexp
    ;

arithexp
    : arithterm
    | arithexp '+' arithterm
    | arithexp '-' arithterm
    ;

arithterm
    : arithfactor
    | arithterm '*' arithfactor
    | arithterm '/' arithfactor
    ;

arithfactor
    : id
    | integer
    | '-' arithexp
    | '(' arithexp ')'
    | id '(' arithexplist ')'
    ;

arithexplist
    : arithexp
    | arithexplist ',' arithexp
    ;

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 spaces, print a space after not, and print parentheses only if the parent operator has higher precedence.

For loops, first print the 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
  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 r<y
x=q*y+r and 0<=r and y>0 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