web代做 | Data structure代做 | java | 作业oop – Program 1: Verification Condition Generator

Program 1: Verification Condition Generator

web代做 | Data structure代做 | java | 作业oop – 这是一个web面向对象设计的practice, 考察web的理解, 是有一定代表意义的web/Data structure/java/oop等代写方向

OOP代写 代写oop

CSC 7101, Spring 2019

Due: 2 March 2019

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 verifi- cation 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 sure you putantlr-4.7.1-complete.jaronto your CLASSPATH. For details, see the Quick Start and Samples instructions on the ANTLR web page or read theMakefileI 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 will 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 Exp { ... }
class Ident extends Exp { ... }
class IntLit extends Exp { ... }
class OpExp extends Exp { ... }
// etc.

For expressions, you will need methods for printing the expression and for performing a substitution. For adding statements, it would be best to group expressions and statements as two separate parts of the class hierarchy or as two disjoint class hierarchies, since you will need different methods, e.g.,

abstract class Node { ... }
abstract class Exp extends Node { ... }
abstract class Stmt extends Node { ... }
class Ident extends Exp { ... }
class IntLit extends Exp { ... }
class OpExp extends Exp { ... }
// etc.
class Assign extends Stmt { ... }
// etc.

Grammar

Use the following grammar for the language IMP (in ANTLR syntax) with start symbolprogramas 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
;
boolterm
: boolterm
| boolterm or boolterm
;
boolterm
: boolfactor
| boolterm2 and boolfactor
;
boolfactor
: true
| false
| compexp
| forall id . boolexp
| exists id . boolexp
| not boolfactor
| ( boolexp )
;
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 | – arithfactor | ( arithexp ) | 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)=

Surround only the operators=>,<=>,and, andorwith spaces, print a space afternot,forall, andexists, and print parentheses only if the parent operator has higher precedence (or for right-associative subtractions). For loops, first print the exit condition, then the condition for the l oop 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>=
x>=0 and y>0 => x=0*y+x and 0<=x and y>

Administrative Stuff

Put your files into directory~/prog1in yourcs7101xxaccount onclasses.csc.lsu.edu, make sure that you have aMakefileso that your code can be compiled and run using the commands

cd ~/prog
make clean
make
 java VCG test.vcg

(assuming that the CLASSPATH is set appropriately) and provide a fileREADME.txtwith anything that you want me or the grader to know about your project. For submitting the code, simply use

cd ~/prog
make clean
~cs7101_bau/bin/p_copy 1

Do not put the files into a ZIP file.