From 277d9bacd6f5c9c1698809b3138d8eac7187e1bd Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?R=C3=A9gis=20Blanc?= <regwblanc@gmail.com>
Date: Thu, 21 Jun 2012 18:41:35 +0200
Subject: [PATCH] examples of epsilon
---
.../master-thesis-regis/Constraints.scala | 26 ++++++++++++++++++-
1 file changed, 25 insertions(+), 1 deletion(-)
diff --git a/testcases/master-thesis-regis/Constraints.scala b/testcases/master-thesis-regis/Constraints.scala
index 6fdd96392..d7dcb696d 100644
--- a/testcases/master-thesis-regis/Constraints.scala
+++ b/testcases/master-thesis-regis/Constraints.scala
@@ -21,6 +21,30 @@ object Epsilon4 {
MyCons(elem, toList(set -- Set[Int](elem)))
}
- def property(lst: MyList): Boolean = (size(toList(toSet(lst))) <= size(lst)) holds
+ def sizeToListEq(lst: MyList): Boolean = (size(toList(toSet(lst))) == size(lst)) holds
+
+ def sizeToListLessEq(lst: MyList): Boolean = (size(toList(toSet(lst))) <= size(lst)) holds
+
+ def toListEq(lst: MyList): Boolean = (toList(toSet(lst)) == lst) holds
+
+ def positiveNum(): Int = epsilon((x: Int) => x > 0) ensuring(_ > 0)
+
+
+ def linearEquation(): (Int, Int) = {
+ val sol = epsilon((t: (Int, Int)) => 2*t._1 + 3*t._2 == 10 && t._1 >= 0 && t._2 >= 0)
+ sol
+ } ensuring(res => res == (2, 2) || res == (5, 0))
+
+
+ def nonDeterminsticExecution(): Int = {
+ var i = 0
+ var b = epsilon((x: Boolean) => i == i)
+ while(b) {
+ i = i + 1
+ b = epsilon((x: Boolean) => i == i)
+ }
+ i
+ } ensuring(_ <= 10)
+
}
--
GitLab