We say that a program is sufficiently annotated if every loop is cut by at least one assert annotation. Your task is to implement an automated verifier for sufficiently annotated programs.

In the archive below we added support for annotating any statement in a program with an assert by writting @assert(formula) immediately before the statement one wants to annotate. Please have a look at trait “Annotated” to see how syntax trees are annotated. Also have a look at the example programs in the archive.

Whereas “assert(formula)” calls denote runtime asserts that may crash the program, “@assert(formula)” annotations are just there for program verification. Hence an @assert annotation does not give rise to an edge toward the error state in the CFG.

The CFG class has been modified for the needs of verification condition generation (VCG). It now includes assert annotations and the set of all variables declared in the program. The graph drawer now also includes annotations.

The archive contains code that translates an AST with assert annotations to a CFG with assert annotations. You can use this code or modify your own, as long as you are able to produce correctly annotated CFGs. Note that “assert(formula)” also generates an assert annotation in the given code.

Your task is to modify the file vcg/VCG.scala in order to implement a compositional verification condition generator that runs in polynomial time and that produces formulas with polynomially many disjunctions (with respect to the number of nodes of the CFG). Note that the rules given in the link above need to be adapted to CFGs.

Archive

You will find two folders named test/example1 and test/example2 in the archive. Both contain a program, a representation of its CFG (with asserts in square boxes), and representations of the basic paths of the program. For these examples, your code should generate verification conditions corresponding to the given basic paths.

Both examples are sufficiently annotated and correct.