From 4cc65ae34e663b4f8d1bbad8953fc03c213d3620 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Ali=20Sinan=20K=C3=B6ksal?= <alisinan@gmail.com>
Date: Thu, 18 Nov 2010 12:21:26 +0000
Subject: [PATCH] An implementation of InductionTactic and its example use in
ListWithSize
---
src/purescala/InductionTactic.scala | 64 ++++++++++++++++++++++++++++-
testcases/ListWithSize.scala | 4 ++
2 files changed, 67 insertions(+), 1 deletion(-)
diff --git a/src/purescala/InductionTactic.scala b/src/purescala/InductionTactic.scala
index dc4616a2f..d0567d4a4 100644
--- a/src/purescala/InductionTactic.scala
+++ b/src/purescala/InductionTactic.scala
@@ -2,13 +2,75 @@ package purescala
import purescala.Common._
import purescala.Trees._
+import purescala.TypeTrees._
import purescala.Definitions._
class InductionTactic(reporter: Reporter) extends DefaultTactic(reporter) {
override val description = "Induction tactic for suitable functions"
override val shortDescription = "induction"
+ private def singleAbsClassDef(args: VarDecls) : Option[AbstractClassDef] = {
+ val filtered = args.filter(arg =>
+ arg.getType match {
+ case AbstractClassType(_) => true
+ case _ => false
+ })
+ if (filtered.size != 1) None else (filtered.head.getType match {
+ case AbstractClassType(classDef) => Some(classDef)
+ case _ => scala.Predef.error("This should not happen.")
+ })
+ }
+
+ private def selectorsOfParentType(parentType: ClassType, ccd: CaseClassDef, expr: Expr) : Seq[Expr] = {
+ val childrenOfSameType = ccd.fields.filter(field => field.getType == parentType)
+ for (field <- childrenOfSameType) yield {
+ CaseClassSelector(ccd, expr, field.id).setType(parentType)
+ }
+ }
+
override def generatePostconditions(funDef: FunDef) : Seq[VerificationCondition] = {
- Seq(new VerificationCondition(BooleanLiteral(false), funDef, VCKind.Postcondition, this))
+ assert(funDef.body.isDefined)
+ val defaultPost = super.generatePostconditions(funDef)
+ singleAbsClassDef(funDef.args) match {
+ case Some(classDef) =>
+ val prec = funDef.precondition
+ val post = funDef.postcondition
+ val body = matchToIfThenElse(funDef.body.get)
+ val arg = funDef.args.head
+ val argAsVar = arg.toVariable
+
+ if (post.isEmpty) {
+ Seq.empty
+ } else {
+ val children = classDef.knownChildren
+ val conditionsForEachChild = (for (child <- classDef.knownChildren) yield (child match {
+ case ccd @ CaseClassDef(id, prnt, vds) =>
+ val selectors = selectorsOfParentType(classDefToClassType(classDef), ccd, argAsVar)
+ // if no subtrees of parent type, assert property for base case
+ val resFresh = FreshIdentifier("result", true).setType(body.getType)
+ val bodyAndPostForArg = Let(resFresh, body, replace(Map(ResultVariable() -> Variable(resFresh)), matchToIfThenElse(post.get)))
+
+ val conditionForChild =
+ if (selectors.size == 0)
+ bodyAndPostForArg
+ else {
+ val inductiveHypothesis = (for (sel <- selectors) yield {
+ val resFresh = FreshIdentifier("result", true).setType(body.getType)
+ val bodyAndPost = Let(resFresh, replace(Map(argAsVar -> sel), body), replace(Map(ResultVariable() -> Variable(resFresh), argAsVar -> sel), matchToIfThenElse(post.get)))
+ bodyAndPost
+ })
+ Implies(And(inductiveHypothesis), bodyAndPostForArg)
+ }
+ Implies(CaseClassInstanceOf(ccd, argAsVar), conditionForChild)
+ case _ => error("Abstract class has non-case class subtype.")
+ }))
+ println("Induction tactic yields the following vc:")
+ println(And(conditionsForEachChild))
+ Seq(new VerificationCondition(And(conditionsForEachChild), funDef, VCKind.Postcondition, this))
+ }
+ case None =>
+ reporter.warning("Induction tactic currently supports exactly one argument of abstract class type")
+ defaultPost
+ }
}
}
diff --git a/testcases/ListWithSize.scala b/testcases/ListWithSize.scala
index 70f1291ca..7e3523bb5 100644
--- a/testcases/ListWithSize.scala
+++ b/testcases/ListWithSize.scala
@@ -1,5 +1,6 @@
import scala.collection.immutable.Set
import funcheck.Annotations._
+import funcheck.Utils._
object ListWithSize {
sealed abstract class List
@@ -49,6 +50,9 @@ object ListWithSize {
case Cons(x,xs) => nilAppend(xs)
}) ensuring(res => res && append(l, Nil()) == l)
+ @induct
+ def nilAppendInductive(l : List) : Boolean = (append(l, Nil()) == l) holds
+
// unclear if we needed this--it was meant to force folding
def appendFold(x : Int, xs : List, ys : List) : Boolean = {
true
--
GitLab