This is a pen and paper exercise. Homework 4 - part 1

Your task is to implement compositional VCG for a simple programming language. You will need to modify and extend the code provided in the following archive.

The archive contains a parser, classes representing formulas, code to call the Z3 SMT solver, and skeleton code that you have to complete. Moreover the file demo.while gives examples of all the constructs available in the language.

You need to generate verification conditions as follows:

• First transform the program into an equivalent program in the guarded command language augmented with the loop construct (i.e using only assume, assert, [], havoc, and loop)
• Then apply loop unrolling up to a chosen depth.
• Then generate verification conditions according to the compositional method.
• Finally pass the obtained verification conditions to Z3 and report on their validity.

You will be using the Z3 SMT solver to prove the validity of the verification conditions that you generate. You may download and install Z3 from this webpage. Make sure to put the executable in your path.

You can check that the installation worked by running the following Scala code:

package whilelang
 
object FormulasDemo {
  def main(args: Array[String]): Unit = {
    // You may not want to do the following import if names collide with your other classes       
    import Formulas._
 
    // These implicit conversions can be useful to avoid writing        
    // Var("a") or Const(42) for each variable and numerical constant.  
    implicit def numToConst(n: Int): Const = Const(n)
    implicit def strToVar(s: String): Var = Var(s)
 
    // checks whether 6 * 7 is always equal to 42. In other words,
    // checks that:                                                     
    //                                                                  
    //   !(a = 6 --> 7 * a = 42)                                        
    //                                                                  
    // ...is unsatisfiable.                                             
    val formula = Not(Implies(Equals("a", 6), Equals(Times(7, "a"), 42)))
 
    val result = isSat(formula) match {                                 
      case Some(false) => "unsat"
      case Some(true) => "sat"
      case None => "unknown"
    }
 
    println("The formula:")                                             
    // Prints the formula in SMT format.                                
    println(benchmarkString(formula))
    println("...has the status: " + result + ".")                       
  } 
} 

It should say unsat. If an error is reported (for instance, “Z3 complained with: null”), chances are that your Z3 installation was not done correctly.