termination testcases

src/test/resources/regression/termination/looping/LambdaCalculus.scala

+import leon.lang._
+import leon.collection._
+import leon._
+
+object LambdaCalculus {
+  abstract class Term
+  case class Var(x: BigInt) extends Term
+  case class Abs(x: BigInt, body: Term) extends Term
+  case class App(func: Term, arg: Term) extends Term
+  
+  def fv(t: Term): Set[BigInt] = t match {
+    case Var(x) => Set(x)
+    case Abs(x, body) => fv(body) ++ Set(x)
+    case App(func, arg) => fv(func) ++ fv(arg)
+  }
+  
+  // [x->u]t
+  def subst(x: BigInt, u: Term, t: Term): Term = t match {
+    case Var(y) => if (x == y) u else t
+    case Abs(y, body) => if (x == y) t else Abs(y, subst(x, u, body))
+    case App(f, a) => App(subst(x, u, f), subst(x, u, a))
+  }
+  
+  /* Termination checker (LoopProcessor) says:
+  ✗ Non-terminating for call: eval(App(Abs(0, App(Var(0), Var(0))), Abs(0, App(Var(0), Var(0)))))
+  i.e.
+  (λx. x x)(λx. x x)
+  This is the well-known "omega".
+  */
+  // big step call-by-value evaluation
+  def eval(t: Term): Option[Term] = (t match {
+    case App(t1, t2) => eval(t1) match {
+      case Some(Abs(x, body)) => eval(t2) match {
+        case Some(v2) => eval(subst(x, v2, body))
+        case None() => None()
+      }
+      case _ => None() // stuck
+    }
+    case _ => Some(t) // Abs or Var, already a value
+  }) ensuring { res => res match {
+    case Some(t) => isValue(t)
+    case None() => true
+  }}
+
+  def isValue(t: Term): Boolean = t match {
+    case Var(x) => true
+    case Abs(x, body) => true
+    case App(f, a) => false
+  }
+
+}

src/test/resources/regression/termination/looping/OddEven.scala

+
+object Test {
+
+  def isOdd(n: BigInt): Boolean = {
+    isEven(n-1)
+  } ensuring { res => (n % 2 == 1) == res }
+  
+  def isEven(n: BigInt): Boolean = {
+    isOdd(n-1)
+  } ensuring { res => (n % 2 == 0) == res }
+  
+  
+}
\ No newline at end of file

src/test/resources/regression/termination/looping/UniversalEquality.scala

+import leon.lang._
+import leon.collection._
+import leon._
+
+object test {
+  
+  def universalEquality(e1: BigInt, e2: BigInt): Boolean = {
+    val b = proveEquality(e1, e2)
+    e1 == e2
+  }.holds
+  
+  def proveEquality(a: BigInt, b: BigInt): Boolean = {
+    proveEquality(a, b)
+  } ensuring { res => res == (a == b) && res }
+
+}

src/test/resources/regression/termination/looping/WrongFibonacci.scala

+
+object Test {
+  
+  def fib(n: BigInt): BigInt = {
+    fib(n-1) + fib(n-2)
+  } ensuring {res => res == (5*n + 1)*(5*n - 1)}
+  
+}

src/test/resources/regression/termination/valid/CountTowardsZero.scala

+
+object Test {
+  def f(x: BigInt): BigInt = {
+    if (x == 0) {
+      0
+    } else if (x > 0) {
+      f(x-1)+2
+    } else if (x < 0) {
+      f(x+1)-2
+    } else {
+      33
+    }
+  } ensuring (_ == x*2)
+}

testcases/termination/pending/McCarthy91.scala

+
+/*
+This function terminates for all inputs, see
+http://en.wikipedia.org/wiki/McCarthy_91_function
+
+But the termination checker returns NoGuarantee after 75s.
+*/
+object McCarthy91 {
+  def M(n: BigInt): BigInt = if (n > 100) n-10 else M(M(n+11))
+}

testcases/termination/pending/lambdaDot.scala

+/*
+A very much simplified implementation of the types in the
+Dependent Object Calculus (http://lampwww.epfl.ch/~amin/dot/fool.pdf).
+
+It's interesting because expansion calls itself recursively (through
+lookupInVar), and passes the results of this recursive call to another
+recursive call.
+
+The termination checker loops forever [or at least longer than several
+minutes ;-)] on this case.
+*/
+
+import leon.lang._
+import leon.collection._
+import leon._
+
+object lambdaDot {
+  abstract class Label
+  case class TypLabel(id: BigInt) extends Label
+  case class MtdLabel(id: BigInt) extends Label
+
+  abstract class Type
+  case class Top() extends Type
+  case class Bot() extends Type
+  case class Rcd(ds: List[Dec]) extends Type
+  case class TSel(x: BigInt, l: BigInt) extends Type
+  
+  abstract class Dec {
+    def label: Label = this match {
+      case TDec(l, _, _) => TypLabel(l)
+      case MDec(m, _, _) => MtdLabel(m)
+    }
+  }
+  case class TDec(l: BigInt, lowerBound: Type, upperBound: Type) extends Dec
+  case class MDec(m: BigInt, argType: Type, retType: Type) extends Dec
+
+  abstract class Decs
+  case class FiniteDecs(l: List[Dec]) extends Decs
+  case class BotDecs() extends Decs
+  
+  def lookupInEnv(x: BigInt, env: List[(BigInt, Type)]): Option[Type] = env match {
+    case Cons((y, t), rest) => if (x == y) Some(t) else lookupInEnv(x, rest)
+    case Nil() => None()
+  }
+  
+  def lookupInDecList(name: Label, l: List[Dec]): Option[Dec] = (l match {
+    case Cons(d, ds) => if (d.label == name) Some(d) else lookupInDecList(name, ds)
+    case Nil() => None()
+  }) ensuring { res => res match {
+    case Some(d) => d.label == name
+    case None() => true
+  }}
+  
+  def lookupInDecs(name: Label, l: Decs): Option[Dec] = (l match {
+    case FiniteDecs(l) => lookupInDecList(name, l)
+    case BotDecs() => name match {
+      case TypLabel(l) => Some(TDec(l, Top(), Bot()))
+      case MtdLabel(m) => Some(MDec(m, Top(), Bot()))
+    }
+  }) ensuring { res => res match {
+    case Some(d) => d.label == name
+    case None() => true
+  }}
+
+  def wfType(env: List[(BigInt, Type)], t: Type, shallow: Boolean): Boolean = t match {
+    case Top() => true
+    case Bot() => true
+    case Rcd(ds) => shallow || wfDecList(env, ds)
+    case TSel(x, l) => lookupInVar(env, x, TypLabel(l)) match {
+      case Some(TDec(l, lo, hi)) => wfType(env, lo, true) && wfType(env, hi, true)
+      case None() => false
+    }
+  }
+  
+  def wfDec(env: List[(BigInt, Type)], d: Dec): Boolean = d match {
+    case TDec(l, lo, hi) => wfType(env, lo, false) && wfType(env, hi, false)
+    case MDec(m, a, r) => wfType(env, a, false) && wfType(env, r, false)
+  }
+  
+  def wfDecList(env: List[(BigInt, Type)], ds: List[Dec]): Boolean = ds match {
+    case Cons(d, ds) => wfDec(env, d) && wfDecList(env, ds)
+    case Nil() => true
+  }
+
+  def expansion(env: List[(BigInt, Type)], t: Type): Option[Decs] = {
+    //require(wfType(env, t, false))
+    t match {
+      case Top() => Some(FiniteDecs(Nil()))
+      case Bot() => Some(FiniteDecs(Nil()))
+      case Rcd(ds) => Some(FiniteDecs(ds))
+      case TSel(x, l) => lookupInVar(env, x, TypLabel(l)) match {
+        case Some(TDec(l, lo, hi)) => expansion(env, hi)
+        case None() => None()
+      }
+    }
+  }
+  
+  def lookupInVar(env: List[(BigInt, Type)], x: BigInt, l: Label): Option[Dec] = {
+    lookupInEnv(x, env) match {
+      case Some(tx) => expansion(env, tx) match {
+        case Some(dsx) => lookupInDecs(l, dsx)
+        case None() => None()
+      }
+      case None() => None()
+    }
+  } ensuring { res => res match {
+    case Some(d) => d.label == l
+    case None() => true
+  }}
+  
+}
+