Skip to content
Snippets Groups Projects
Commit fa1fbd18 authored by Viktor Kuncak's avatar Viktor Kuncak
Browse files

small changes to demo

parent 87907e45
No related branches found
No related tags found
No related merge requests found
import leon.lang._
import leon.lang.synthesis._ import leon.lang.synthesis._
import leon.annotation._ import leon.annotation._
object Max { object Max {
...@@ -42,7 +41,8 @@ object Max { ...@@ -42,7 +41,8 @@ object Max {
max(x,y) == max(y,x) && max(x,y) == max(y,x) &&
max(x,max(y,z)) == max(max(x,y), z) && max(x,max(y,z)) == max(max(x,y), z) &&
max(x,y) + z == max(x + z, y + z) max(x,y) + z == max(x + z, y + z)
} holds } ensuring(_ == true)
// holds
*/ */
/* /*
...@@ -54,4 +54,10 @@ object Max { ...@@ -54,4 +54,10 @@ object Max {
} ensuring (res => } ensuring (res =>
x <= res && y <= res && (res == x || res == y)) x <= res && y <= res && (res == x || res == y))
*/ */
/*
def max(x: BigInt, y: BigInt): BigInt = {
???[BigInt]
} ensuring(res => (res == x || res == y) && x <= res && y <= res)
*/
} }
import leon.lang._ import leon.lang.Set
import leon.lang.synthesis._ import leon.lang.synthesis._
import leon.annotation._
object Sort { object Sort {
sealed abstract class List sealed abstract class List
case object Nil extends List case object Nil extends List
case class Cons(head: BigInt, tail: List) extends List case class Cons(head: BigInt, tail: List) extends List
def size(l: List): BigInt = (l match {
case Nil => 0
case Cons(x, rest) => x + size(rest)
}) ensuring(res => res > 0)
def s1 = size(Cons(10, Cons(1000, Nil)))
def content(l: List): Set[BigInt] = l match { def content(l: List): Set[BigInt] = l match {
case Nil => Set() case Nil => Set()
case Cons(i, t) => Set(i) ++ content(t) case Cons(i, t) => Set(i) ++ content(t)
...@@ -53,7 +45,6 @@ object Sort { ...@@ -53,7 +45,6 @@ object Sort {
} }
} ensuring {(res:List) => } ensuring {(res:List) =>
isSorted(res) && content(res) == content(l) ++ Set(x)} isSorted(res) && content(res) == content(l) ++ Set(x)}
// size(res) == size(l) + 1
*/ */
// We can also synthesize the body of sInsert interactively // We can also synthesize the body of sInsert interactively
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment