Skip to content
Snippets Groups Projects
Commit cba3b360 authored by Etienne Kneuss's avatar Etienne Kneuss
Browse files

Add some testcases, focus gitignore

parent 019e5db7
No related branches found
No related tags found
No related merge requests found
......@@ -21,12 +21,14 @@ target
derivation*.dot
# leon
last.log
*.last
*.table
*.log
smt-sessions/
leon.out/
/last.log
/*.last
/*.table
/*.log
/smt-sessions/
/leon.out/
/repairs.dat
/tmp
#eclipse
.cache
......@@ -41,13 +43,13 @@ Leon.eml
Leon.iml
#scripts
out-classes
/out-classes
#z3
.z3-trace
#travis
travis/builds
/travis/builds
# Isabelle
contrib
object Test {
def focusCond(a: BigInt) = {
if (a < 0) {
-a + 1
} else {
a
}
} ensuring {
_ > 0
}
}
object Test {
def focusCond(a: BigInt) = {
if (a > 0) {
a
} else {
BigInt(-1)
}
} ensuring {
_ > 0
}
}
object Test {
def focusCond(a: BigInt) = {
if (a <= 0) {
BigInt(-1)
} else {
a
}
} ensuring {
_ > 0
}
}
object Test {
def focusCond(a: BigInt) = {
val tmp = -a
tmp
} ensuring {
_ > 0
}
}
import leon.lang._
object Test {
def focusMatch(a: BigInt, b: BigInt) = {
(a, b) match {
case (otherA, BigInt(0)) => otherA
case _ => a+1
}
} ensuring {
res => if (b == 0) {
res == 0
} else {
res == a+1
}
}
}
object Test {
def focusCond(a: BigInt) = {
if (a <= 0) {
(a, BigInt(0))
} else {
(a, BigInt(0))
}
} ensuring {
res => res._1 == a && res._2 > 1
}
}
import leon.lang._
object Test {
def focusCond(a: BigInt) = {
a match {
case BigInt(1) => (BigInt(2), BigInt(0))
case BigInt(2) => (BigInt(2), BigInt(0))
case _ => (BigInt(0), BigInt(0))
}
} ensuring {
res => res._1 == a && res._2 > 1
}
}
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment