Program 1: Verification Condition Generator
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 put antlr-4.7.1-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 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.
1
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
;
boolterm
: boolterm2
| boolterm ¡¯or¡¯ boolterm2
;
boolterm2
: boolfactor
| boolterm2 ¡¯and¡¯ boolfactor
;
boolfactor
: ¡¯true¡¯
| ¡¯false¡¯
| compexp
| ¡¯forall¡¯ id ¡¯.¡¯ boolexp
| ¡¯exists¡¯ id ¡¯.¡¯ boolexp
| ¡¯not¡¯ boolfactor
| ¡¯(¡¯ boolexp ¡¯)¡¯
;
compexp
: arithexp ¡¯<¡¯ arithexp
| arithexp ¡¯<=¡¯ arithexp
2
| 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
;
3
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, forall, and exists, 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 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
x>=0 and y>0 => x=0*y+x and 0<=x and y>0
Administrative Stuff
Put your files into directory ~/prog1 in your cs7101xx account on classes.csc.lsu.edu, make sure that you have a Makefile so that your code can be compiled and run using the commands
cd ~/prog1
make clean
make
java VCG test.vcg
(assuming that the CLASSPATH is set appropriately) and provide a file README.txt with anything that you want me or the grader to know about your project.
For submitting the code, simply use
cd ~/prog1
make clean
~cs7101_bau/bin/p_copy 1
Do not put the files into a ZIP file.
4