now it's not working. please do not use :)

src/purescala/Analysis.scala

@@ -24,6 +24,9 @@ class Analysis(val program: Program) {
   }
 
   val defaultTactic = new DefaultTactic(reporter)
+  defaultTactic.setProgram(program)
+  val inductionTactic = new InductionTactic(reporter)
+  inductionTactic.setProgram(program)
 
   // Calling this method will run all analyses on the program passed at
   // construction time. If at least one solver is loaded, verification
@@ -32,8 +35,13 @@ class Analysis(val program: Program) {
   def analyse : Unit = {
     if(solverExtensions.size > 0) {
       reporter.info("Running verification condition generation...")
-      checkVerificationConditions
-    } 
+      // checkVerificationConditions
+
+      val list = generateVerificationConditions
+      list.foreach(e => println(e.infoLine))
+    } else {
+      reporter.warning("No solver specified. Cannot test verification conditions.")
+    }
 
     analysisExtensions.foreach(ae => {
       reporter.info("Running analysis from extension: " + ae.description)
@@ -41,6 +49,28 @@ class Analysis(val program: Program) {
     })
   }
 
+  def generateVerificationConditions : List[VerificationCondition] = {
+    var allVCs: Seq[VerificationCondition] = Seq.empty
+
+    for(funDef <- program.definedFunctions.toList.sortWith((fd1, fd2) => fd1.id.name < fd2.id.name) if (Settings.functionsToAnalyse.isEmpty || Settings.functionsToAnalyse.contains(funDef.id.name))) {
+      val tactic: Tactic =
+        if(funDef.annotations.contains("induct")) {
+          inductionTactic
+        } else {
+          defaultTactic
+        }
+
+      if(funDef.body.isDefined) {
+        allVCs ++= tactic.generatePreconditions(funDef)
+        allVCs ++= tactic.generatePostconditions(funDef)
+        allVCs ++= tactic.generatePatternMatchingExhaustivenessChecks(funDef)
+        allVCs ++= tactic.generateMiscCorrectnessConditions(funDef)
+      }
+    }
+
+    allVCs.toList
+  }
+
   def checkVerificationConditions : Unit = {
     // just for the summary:
     var verificationConditionInfos: List[VerificationCondition] = Nil
@@ -52,8 +82,10 @@ class Analysis(val program: Program) {
     for(funDef <- program.definedFunctions.toList.sortWith((fd1,fd2) => fd1.id.name < fd2.id.name)) if (Settings.functionsToAnalyse.isEmpty || Settings.functionsToAnalyse.contains(funDef.id.name)) {
       analysedFunctions += funDef.id.name
       if(funDef.body.isDefined) {
-        val vc = postconditionVC(funDef)
-        val vcInfo = new VerificationCondition(vc, funDef, VCKind.Postcondition, defaultTactic)
+        val vcInfo = defaultTactic.generatePostconditions(funDef).head
+        val vc = vcInfo.condition
+        // val vc = postconditionVC(funDef)
+        // val vcInfo = new VerificationCondition(vc, funDef, VCKind.Postcondition, defaultTactic)
         verificationConditionInfos = vcInfo :: verificationConditionInfos
 
         if(vc == BooleanLiteral(false)) {

src/purescala/DefaultTactic.scala

 package purescala
 
+import purescala.Common._
 import purescala.Trees._
 import purescala.Definitions._
 import Extensions.Tactic
@@ -8,19 +9,88 @@ 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
+    var _prog : Option[Program] = None
+    def program : Program = _prog match {
+      case None => throw new Exception("Program never set in DefaultTactic.")
+      case Some(p) => p
+    }
+
+    override def setProgram(program: Program) : Unit = {
+      _prog = Some(program)
+    }
+
+    def generatePostconditions(functionDefinition: FunDef) : Seq[VerificationCondition] = {
+      assert(functionDefinition.body.isDefined)
+      val prec = functionDefinition.precondition
+      val post = functionDefinition.postcondition
+      val body = functionDefinition.body.get
+
+      val theExpr = if(post.isEmpty) {
+        BooleanLiteral(true)
+      } else {
+        val resFresh = FreshIdentifier("result", true).setType(body.getType)
+        val bodyAndPost = Let(resFresh, body, replace(Map(ResultVariable() -> Variable(resFresh)), post.get))
+        val withPrec = if(prec.isEmpty) {
+          bodyAndPost
+        } else {
+          Implies(prec.get, bodyAndPost)
+        }
+
+        import Analysis._
+      
+        if(Settings.experimental) {
+          reporter.info("Raw:")
+          reporter.info(withPrec)
+          reporter.info("Raw, expanded:")
+          reporter.info(expandLets(withPrec))
+        }
+        reporter.info(" - inlining...")
+        val expr0 = inlineNonRecursiveFunctions(program, withPrec)
+        if(Settings.experimental) {
+          reporter.info("Inlined:")
+          reporter.info(expr0)
+          reporter.info("Inlined, expanded:")
+          reporter.info(expandLets(expr0))
+        }
+        reporter.info(" - unrolling...")
+        val expr1 = unrollRecursiveFunctions(program, expr0, Settings.unrollingLevel)
+        if(Settings.experimental) {
+          reporter.info("Unrolled:")
+          reporter.info(expr1)
+          reporter.info("Unrolled, expanded:")
+          reporter.info(expandLets(expr1))
+        }
+        reporter.info(" - inlining contracts...")
+        val expr2 = inlineContracts(expr1)
+        if(Settings.experimental) {
+          reporter.info("Contract'ed:")
+          reporter.info(expr2)
+          reporter.info("Contract'ed, expanded:")
+          reporter.info(expandLets(expr2))
+        }
+        reporter.info(" - converting pattern-matching...")
+        val expr3 = rewriteSimplePatternMatching(expr2)
+        if(Settings.experimental) {
+          reporter.info("Pattern'ed:")
+          reporter.info(expr3)
+          reporter.info("Pattern'ed, expanded:")
+          reporter.info(expandLets(expr3))
+        }
+        expr3
+      }
+
+      Seq(new VerificationCondition(theExpr, functionDefinition, VCKind.Postcondition, this))
     }
 
-    def generatePreconditions(function: FunDef) : Seq[Expr] = {
+    def generatePreconditions(function: FunDef) : Seq[VerificationCondition] = {
       Seq.empty
     }
 
-    def generatePatternMatchingExhaustivenessChecks(function: FunDef) : Seq[Expr] = {
+    def generatePatternMatchingExhaustivenessChecks(function: FunDef) : Seq[VerificationCondition] = {
       Seq.empty
     }
 
-    def generateMiscCorrectnessConditions(function: FunDef) : Seq[Expr] = {
+    def generateMiscCorrectnessConditions(function: FunDef) : Seq[VerificationCondition] = {
       Seq.empty
     }
 }

src/purescala/Extensions.scala

@@ -30,10 +30,11 @@ 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]
+    def setProgram(program: Program) : Unit = {}
+    def generatePostconditions(function: FunDef) : Seq[VerificationCondition]
+    def generatePreconditions(function: FunDef) : Seq[VerificationCondition]
+    def generatePatternMatchingExhaustivenessChecks(function: FunDef) : Seq[VerificationCondition]
+    def generateMiscCorrectnessConditions(function: FunDef) : Seq[VerificationCondition]
   }
 
   // The rest of the code is for dynamically loading extensions

src/purescala/InductionTactic.scala

+package purescala
+
+import purescala.Common._
+import purescala.Trees._
+import purescala.Definitions._
+
+class InductionTactic(reporter: Reporter) extends DefaultTactic(reporter) {
+  override val description = "Induction tactic for suitable functions"
+  override val shortDescription = "induction"
+
+  override def generatePostconditions(funDef: FunDef) : Seq[VerificationCondition] = {
+    Seq(new VerificationCondition(BooleanLiteral(false), funDef, VCKind.Postcondition, this))
+  }
+}