From 2a590b8d62e87a64113e5f9f93e8b95f7832fa95 Mon Sep 17 00:00:00 2001
From: Samuel Gruetter <samuel.gruetter@epfl.ch>
Date: Wed, 3 Jun 2015 19:44:52 +0200
Subject: [PATCH] prefix the looping functions with "looping" so that
the TerminationRegression test checks if counterexamples are found
---
.../termination/looping/LambdaCalculus.scala | 12 ++++++------
.../regression/termination/looping/OddEven.scala | 8 ++++----
.../termination/looping/UniversalEquality.scala | 6 +++---
.../termination/looping/WrongFibonacci.scala | 4 ++--
4 files changed, 15 insertions(+), 15 deletions(-)
diff --git a/src/test/resources/regression/termination/looping/LambdaCalculus.scala b/src/test/resources/regression/termination/looping/LambdaCalculus.scala
index 16e10bb62..884e5dee5 100644
--- a/src/test/resources/regression/termination/looping/LambdaCalculus.scala
+++ b/src/test/resources/regression/termination/looping/LambdaCalculus.scala
@@ -22,16 +22,16 @@ object LambdaCalculus {
}
/* Termination checker (LoopProcessor) says:
- ✗ Non-terminating for call: eval(App(Abs(0, App(Var(0), Var(0))), Abs(0, App(Var(0), Var(0)))))
+ ✗ Non-terminating for call: looping_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))
+ // big step call-by-value looping_evaluation
+ def looping_eval(t: Term): Option[Term] = (t match {
+ case App(t1, t2) => looping_eval(t1) match {
+ case Some(Abs(x, body)) => looping_eval(t2) match {
+ case Some(v2) => looping_eval(subst(x, v2, body))
case None() => None()
}
case _ => None() // stuck
diff --git a/src/test/resources/regression/termination/looping/OddEven.scala b/src/test/resources/regression/termination/looping/OddEven.scala
index e26e45555..078b4c258 100644
--- a/src/test/resources/regression/termination/looping/OddEven.scala
+++ b/src/test/resources/regression/termination/looping/OddEven.scala
@@ -1,12 +1,12 @@
object Test {
- def isOdd(n: BigInt): Boolean = {
- isEven(n-1)
+ def looping_isOdd(n: BigInt): Boolean = {
+ looping_isEven(n-1)
} ensuring { res => (n % 2 == 1) == res }
- def isEven(n: BigInt): Boolean = {
- isOdd(n-1)
+ def looping_isEven(n: BigInt): Boolean = {
+ looping_isOdd(n-1)
} ensuring { res => (n % 2 == 0) == res }
diff --git a/src/test/resources/regression/termination/looping/UniversalEquality.scala b/src/test/resources/regression/termination/looping/UniversalEquality.scala
index fbfd76d27..7b7181a6f 100644
--- a/src/test/resources/regression/termination/looping/UniversalEquality.scala
+++ b/src/test/resources/regression/termination/looping/UniversalEquality.scala
@@ -5,12 +5,12 @@ import leon._
object test {
def universalEquality(e1: BigInt, e2: BigInt): Boolean = {
- val b = proveEquality(e1, e2)
+ val b = looping_proveEquality(e1, e2)
e1 == e2
}.holds
- def proveEquality(a: BigInt, b: BigInt): Boolean = {
- proveEquality(a, b)
+ def looping_proveEquality(a: BigInt, b: BigInt): Boolean = {
+ looping_proveEquality(a, b)
} ensuring { res => res == (a == b) && res }
}
diff --git a/src/test/resources/regression/termination/looping/WrongFibonacci.scala b/src/test/resources/regression/termination/looping/WrongFibonacci.scala
index 2b53eaaef..9911ee76d 100644
--- a/src/test/resources/regression/termination/looping/WrongFibonacci.scala
+++ b/src/test/resources/regression/termination/looping/WrongFibonacci.scala
@@ -1,8 +1,8 @@
object Test {
- def fib(n: BigInt): BigInt = {
- fib(n-1) + fib(n-2)
+ def looping_fib(n: BigInt): BigInt = {
+ looping_fib(n-1) + looping_fib(n-2)
} ensuring {res => res == (5*n + 1)*(5*n - 1)}
}
--
GitLab