Download the archive: labs06.tar.gz

In this lab, we have a verifier for a small imperative language with recursive procedures. In Verification.scala, we generate verification conditions for the post-conditions of each procedure, and invoke Z3 to know whether they are unsatisfiable (and the post-condition is valid) or satisfiable (and the post-condition has a counter-example). You must have a z3 binary in your path for this to work.

You task is to complete the relation function. This function takes a statement and generates an expression that represents the meaning of the statement (by using the original variables and their primed version). In the Compose case, we generate a fresh copy of the global variables, to represent the state in between the two statements.

To test your code, you can use sbt “run examples/valid/Fact.scala” (or other examples). Please make sure that your code passes all examples by using sbt test.

A few hints:

• Except for the Compose case, you should not generate fresh copies of the global variables, and you should not update the fresh variable.

• The arguments/parameters of procedures are immutable, the arguments of the procedure that we are verifying (and only those) can appear in the formula.

• When giving the meaning for procedure invocations, ignore the body of the invoked procedure and only use its postcondition. For instance, invoking a procedure with no postcondition will havoc all the variables.

• Old expressions refer to variables at the beginning of the function. In the ProcedureInvocation case, make sure that you replace the Old expressions that come from the postcondition with the appropriate variables.

• You are provided with helper functions such as replace and subst on expressions.