Inductive tactic performs induction on first argument with abstract type....

Inductive tactic performs induction on first argument with abstract type. Corresponding modification to ListWithSize to prove associativity of append automatically.

pldi2011-testcases/MergeSort.scala

@@ -2,30 +2,31 @@ import scala.collection.immutable.Set
 
 object MergeSort {
   sealed abstract class List
-  case class Cons(head:Int,tail:List) extends List
+  case class Cons(head : Int, tail : List) extends List
   case class Nil() extends List
 
-  case class Pair(fst:List,snd:List)
+  sealed abstract class PairAbs
+  case class Pair(fst : List, snd : List) extends PairAbs
 
-  def contents(l: List): Set[Int] = l match {
+  def contents(l : List) : Set[Int] = l match {
     case Nil() => Set.empty
     case Cons(x,xs) => contents(xs) ++ Set(x)
   }
 
-  def is_sorted(l: List): Boolean = l match {
+  def isSorted(l : List) : Boolean = l match {
     case Nil() => true
     case Cons(x,xs) => xs match {
       case Nil() => true
-      case Cons(y, ys) => x <= y && is_sorted(Cons(y, ys))
+      case Cons(y, ys) => x <= y && isSorted(Cons(y, ys))
     }
   }    
 
-  def length(list:List): Int = list match {
+  def size(list : List) : Int = list match {
     case Nil() => 0
-    case Cons(x,xs) => 1 + length(xs)
+    case Cons(x,xs) => 1 + size(xs)
   }
 
-  def splithelper(aList:List,bList:List,n:Int): Pair = 
+  def splithelper(aList : List, bList : List, n : Int) : Pair = 
     if (n <= 0) Pair(aList,bList)
     else
 	bList match {
@@ -33,28 +34,30 @@ object MergeSort {
     	      case Cons(x,xs) => splithelper(Cons(x,aList),xs,n-1)
 	}
 
-  def split(list:List,n:Int): Pair = splithelper(Nil(),list,n)
+  def split(list : List, n : Int): Pair = splithelper(Nil(),list,n)
 
-  def merge(aList:List, bList:List):List = (bList match {       
-    case Nil() => aList
-    case Cons(x,xs) =>
-    	 aList match {
-   	       case Nil() => bList
-   	       case Cons(y,ys) =>
-    	        if (y < x)
-    		   Cons(y,merge(ys, bList))
-     		else
-		   Cons(x,merge(aList, xs))               
-   	 }   
-  }) ensuring(res => contents(res) == contents(aList) ++ contents(bList))
+  def merge(aList : List, bList : List) : List = {
+    bList match {       
+      case Nil() => aList
+      case Cons(x,xs) =>
+        aList match {
+              case Nil() => bList
+              case Cons(y,ys) =>
+               if (y < x)
+                  Cons(y,merge(ys, bList))
+               else
+                  Cons(x,merge(aList, xs))               
+        }   
+    }
+  } ensuring(res => contents(res) == contents(aList) ++ contents(bList))
 
-  def mergeSort(list:List):List = (list match {
+  def mergeSort(list : List) : List = (list match {
     case Nil() => list
     case Cons(x,Nil()) => list
     case _ =>
-    	 val p = split(list,length(list)/2)
+    	 val p = split(list,size(list)/2)
    	 merge(mergeSort(p.fst), mergeSort(p.snd))     
-  }) ensuring(res => contents(res) == contents(list) && is_sorted(res))
+  }) ensuring(res => contents(res) == contents(list) && isSorted(res))
  
 
   def main(args: Array[String]): Unit = {

src/purescala/InductionTactic.scala

@@ -21,6 +21,18 @@ class InductionTactic(reporter: Reporter) extends DefaultTactic(reporter) {
     })
   } 
 
+  private def firstAbsClassDef(args: VarDecls) : Option[(AbstractClassDef, VarDecl)] = {
+    val filtered = args.filter(arg =>
+      arg.getType match {
+        case AbstractClassType(_) => true
+        case _ => false
+      })
+    if (filtered.size == 0) None else (filtered.head.getType match {
+      case AbstractClassType(classDef) => Some((classDef, filtered.head))
+      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 {
@@ -31,12 +43,11 @@ class InductionTactic(reporter: Reporter) extends DefaultTactic(reporter) {
   override def generatePostconditions(funDef: FunDef) : Seq[VerificationCondition] = {
     assert(funDef.body.isDefined)
     val defaultPost = super.generatePostconditions(funDef)
-    singleAbsClassDef(funDef.args) match {
-      case Some(classDef) =>
+    firstAbsClassDef(funDef.args) match {
+      case Some((classDef, arg)) =>
         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) {

testcases/ListWithSize.scala

@@ -59,12 +59,16 @@ object ListWithSize {
     } ensuring (res => res && Cons(x,append(xs, ys)) == append(Cons(x,xs), ys))
 
     def appendAssoc(xs : List, ys : List, zs : List) : Boolean = (xs match {
-      case Nil() => (nilAppend(append(ys,zs)) && nilAppend(ys))
+      case Nil() => (nilAppendInductive(append(ys,zs)) && nilAppendInductive(ys))
       case Cons(x,xs1) => appendAssoc(xs1, ys, zs)
     }) ensuring (res => res && append(xs, append(ys, zs)) == append(append(xs,ys), zs))
 
+    @induct
+    def appendAssocInductive(xs : List, ys : List, zs : List) : Boolean =
+      (append(append(xs, ys), zs) == append(xs, append(ys, zs))) holds
+
     def sizeAppend(l1 : List, l2 : List) : Boolean = (l1 match {
-      case Nil() => nilAppend(l2)
+      case Nil() => nilAppendInductive(l2)
       case Cons(x,xs) => sizeAppend(xs, l2)
     }) ensuring(res => res && size(append(l1,l2)) == size(l1) + size(l2))