cosmetic.

src/purescala/Analysis.scala

@@ -17,6 +17,14 @@ class Analysis(val program: Program) {
   val analysisExtensions: Seq[Analyser] = loadedAnalysisExtensions
   val solverExtensions: Seq[Solver] = loadedSolverExtensions
 
+  val trivialSolver = new Solver(reporter) {
+    val description = "Trivial"
+    override val shortDescription = "trivial"
+    def solve(e: Expr) = throw new Exception("trivial solver should not be called.")
+  }
+
+  val defaultTactic = new DefaultTactic(reporter)
+
   // Calling this method will run all analyses on the program passed at
   // construction time. If at least one solver is loaded, verification
   // conditions are generated and passed to all solvers. Otherwise, only the
@@ -35,7 +43,8 @@ class Analysis(val program: Program) {
 
   def checkVerificationConditions : Unit = {
     // just for the summary:
-    var verifiedVCs: List[(String,String,String,String,String)] = Nil
+    var verificationConditionInfos: List[VerificationCondition] = Nil
+
     var analysedFunctions: MutableSet[String] = MutableSet.empty
 
     solverExtensions.foreach(_.setProgram(program))
@@ -44,11 +53,18 @@ class Analysis(val program: Program) {
       analysedFunctions += funDef.id.name
       if(funDef.body.isDefined) {
         val vc = postconditionVC(funDef)
+        val vcInfo = new VerificationCondition(vc, funDef, VCKind.Postcondition, defaultTactic)
+        verificationConditionInfos = vcInfo :: verificationConditionInfos
+
         if(vc == BooleanLiteral(false)) {
-          verifiedVCs = (funDef.id.toString, "postcondition", "invalid", "trivial", "--") :: verifiedVCs
+          vcInfo.value = Some(false)
+          vcInfo.solvedWith = Some(trivialSolver)
+          vcInfo.time = Some(0L)
         } else if(vc == BooleanLiteral(true)) {
           if(funDef.hasPostcondition) {
-            verifiedVCs = (funDef.id.toString, "postcondition", "valid", "tautology", "--") :: verifiedVCs
+          vcInfo.value = Some(true)
+          vcInfo.solvedWith = Some(trivialSolver)
+          vcInfo.time = Some(0L)
           }
         } else {
           reporter.info("Verification condition (post) for ==== " + funDef.id + " ====")
@@ -57,11 +73,6 @@ class Analysis(val program: Program) {
           } else {
             reporter.info("(not showing unrolled VCs)")
           }
-          // reporter.info("Negated:")
-          // reporter.info(negate(vc))
-          // reporter.info("Negated, expanded:")
-          // val exp = expandLets(negate(vc))
-          // reporter.info(exp)
 
           // try all solvers until one returns a meaningful answer
           var superseeded : Set[String] = Set.empty[String]
@@ -82,12 +93,20 @@ class Analysis(val program: Program) {
                 case None => false
                 case Some(true) => {
                   reporter.info("==== VALID ====")
-                  verifiedVCs = (funDef.id.toString, "postcondition", "valid", se.shortDescription, dt + "s.") :: verifiedVCs
+
+                  vcInfo.value = Some(true)
+                  vcInfo.solvedWith = Some(se)
+                  vcInfo.time = Some(dt)
+
                   true
                 }
                 case Some(false) => {
                   reporter.error("==== INVALID ====")
-                  verifiedVCs = (funDef.id.toString, "postcondition", "invalid", se.shortDescription, dt + "s.") :: verifiedVCs
+
+                  vcInfo.value = Some(false)
+                  vcInfo.solvedWith = Some(se)
+                  vcInfo.time = Some(dt)
+
                   true
                 }
               }
@@ -95,7 +114,6 @@ class Analysis(val program: Program) {
           }) match {
             case None => {
               reporter.warning("No solver could prove or disprove the verification condition.")
-              verifiedVCs = (funDef.id.toString, "postcondition", "unknown", "--", "--") :: verifiedVCs
             }
             case _ => 
           } 
@@ -103,27 +121,18 @@ class Analysis(val program: Program) {
       } else {
         if(funDef.postcondition.isDefined) {
           reporter.warning(funDef, "Could not verify postcondition: function implementation is unknown.")
-          verifiedVCs = (funDef.id.toString, "postcondition", "unknown", "no body", "--") :: verifiedVCs
         }
       }
     } 
 
-    if(verifiedVCs.size > 0) {
-      verifiedVCs = verifiedVCs.reverse
-      val col1wdth  = verifiedVCs.map(_._1).map(_.length).max + 2
-      val col2wdth  = verifiedVCs.map(_._2).map(_.length).max + 2
-      val col3wdth  = verifiedVCs.map(_._3).map(_.length).max + 2
-      val col4wdth  = verifiedVCs.map(_._4).map(_.length).max + 2
-      val col5wdth  = verifiedVCs.map(_._5).map(_.length).max
-      def mk1line(line: (String,String,String,String,String)) : String = {
-        line._1 + (" " * (col1wdth - line._1.length)) +
-        line._2 + (" " * (col2wdth - line._2.length)) +
-        line._3 + (" " * (col3wdth - line._3.length)) +
-        line._4 + (" " * (col4wdth - line._4.length)) +
-        line._5
-      }
-      val dashes : String = "=" * (col1wdth + col2wdth + col3wdth + col4wdth + col5wdth)
-      reporter.info("Summary:\n" + dashes + "\n" + verifiedVCs.sortWith(_._1 < _._1).map(mk1line(_)).mkString("\n") + "\n" + dashes)
+    if(verificationConditionInfos.size > 0) {
+      verificationConditionInfos = verificationConditionInfos.reverse
+      val summaryString = (
+        VerificationCondition.infoHeader +
+        verificationConditionInfos.map(_.infoLine).mkString("\n", "\n", "\n") +
+        VerificationCondition.infoFooter
+      )
+      reporter.info(summaryString)
     } else {
       reporter.info("No verification conditions were generated.")
     }

src/purescala/DefaultTactic.scala

+package purescala
+
+import purescala.Trees._
+import purescala.Definitions._
+import Extensions.Tactic
+
+class DefaultTactic(reporter: Reporter) extends Tactic(reporter) {
+    val description = "Default verification condition generation approach"
+    override val shortDescription = "default"
+
+    def generatePostconditions(function: FunDef) : Seq[Expr] = {
+      Seq.empty
+    }
+
+    def generatePreconditions(function: FunDef) : Seq[Expr] = {
+      Seq.empty
+    }
+
+    def generatePatternMatchingExhaustivenessChecks(function: FunDef) : Seq[Expr] = {
+      Seq.empty
+    }
+
+    def generateMiscCorrectnessConditions(function: FunDef) : Seq[Expr] = {
+      Seq.empty
+    }
+}

src/purescala/Extensions.scala

@@ -32,6 +32,8 @@ object Extensions {
   abstract class Tactic(reporter: Reporter) extends Extension(reporter) {
     def generatePostconditions(function: FunDef) : Seq[Expr]
     def generatePreconditions(function: FunDef) : Seq[Expr]
+    def generatePatternMatchingExhaustivenessChecks(function: FunDef) : Seq[Expr]
+    def generateMiscCorrectnessConditions(function: FunDef) : Seq[Expr]
   }
 
   // The rest of the code is for dynamically loading extensions

src/purescala/VerificationCondition.scala

+package purescala
+
+import purescala.Extensions._
+import purescala.Trees._
+import purescala.Definitions._
+
+/** This is just to hold some history information. */
+class VerificationCondition(val condition: Expr, val funDef: FunDef, val kind: VCKind.Value, val tactic: Tactic, val info: String = "") {
+  // None = still unknown
+  // Some(true) = valid
+  // Some(false) = valid
+  var value : Option[Boolean] = None
+  var solvedWith : Option[Solver] = None
+  var time : Option[Double] = None
+
+  def status : String = value match {
+    case None => "unknown"
+    case Some(true) => "valid"
+    case Some(false) => "invalid"
+  }
+
+  private def tacticStr = tactic.shortDescription match {
+    case "default" => ""
+    case s => s
+  }
+
+  private def solverStr = solvedWith match {
+    case Some(s) => s.shortDescription
+    case None => ""
+  }
+
+  private def timeStr = time.map(t => "%-3.3f".format(t)).getOrElse("")
+
+  def infoLine : String = {
+    "║ %-15s %-10s %-8s %-10s %-10s %7s ║" format (funDef.id.toString, kind, status, tacticStr, solverStr, timeStr)
+  }
+}
+
+object VerificationCondition {
+  val infoFooter : String = "╚" + ("═" * 67) + "╝"
+  val infoHeader : String = "╔══ Summary " + ("═" * 56) + "╗"
+}
+
+object VCKind extends Enumeration {
+  val Precondition = Value("precond.")
+  val Postcondition = Value("postcond.")
+  val ExhaustiveMatch = Value("match.")
+}