From 9d4b0279c75a75b5b6a492e8939687d41cecc109 Mon Sep 17 00:00:00 2001
From: Viktor Kuncak <viktor.kuncak@epfl.ch>
Date: Tue, 28 Apr 2015 19:56:06 -0700
Subject: [PATCH] demo: split tutorial files into three
---
testcases/web/demos/001_Tutorial-Max.scala | 58 +++++++++++++
.../web/demos/002_Tutorial-TwoSort.scala | 52 ++++++++++++
testcases/web/demos/003_Tutorial-Sort.scala | 83 +++++++++++++++++++
3 files changed, 193 insertions(+)
create mode 100644 testcases/web/demos/001_Tutorial-Max.scala
create mode 100644 testcases/web/demos/002_Tutorial-TwoSort.scala
create mode 100644 testcases/web/demos/003_Tutorial-Sort.scala
diff --git a/testcases/web/demos/001_Tutorial-Max.scala b/testcases/web/demos/001_Tutorial-Max.scala
new file mode 100644
index 000000000..c013d1b9f
--- /dev/null
+++ b/testcases/web/demos/001_Tutorial-Max.scala
@@ -0,0 +1,58 @@
+import leon.lang._
+import leon.lang.synthesis._
+import leon.annotation._
+object Max {
+/*
+ def max(x: Int, y: Int): Int = {
+ val d = x - y
+ if (d > 0) x
+ else y
+ } ensuring(res =>
+ x <= res && y <= res && (res == x || res == y))
+*/
+
+ //def test1 = max(10, 5)
+ //def test2 = max(-5, 5)
+ //def test3 = max(-5, -7)
+
+ //def test4 = max(-1639624704, 1879048192)
+
+/*
+ def max(x: BigInt, y: BigInt): BigInt = {
+ val d = x - y
+ if (d > 0) x
+ else y
+ } ensuring(res =>
+ x <= res && y <= res && (res == x || res == y))
+ */
+
+/*
+ def rmax(x: BigInt, y: BigInt) =
+ if (x <= y) x else y
+
+ def max(x: BigInt, y: BigInt): BigInt = {
+ val d = x - y
+ if (d > 0) x
+ else y
+ } ensuring(res => res==rmax(x,y))
+*/
+
+/*
+ def max_lemma(x: BigInt, y: BigInt, z: BigInt): Boolean = {
+ max(x,x) == x &&
+ max(x,y) == max(y,x) &&
+ max(x,max(y,z)) == max(max(x,y), z) &&
+ max(x,y) + z == max(x + z, y + z)
+ } holds
+*/
+
+/*
+ def max(x: Int, y: Int): Int = {
+ require(0 <= x && 0 <= y)
+ val d = x - y
+ if (d > 0) x
+ else y
+ } ensuring (res =>
+ x <= res && y <= res && (res == x || res == y))
+*/
+}
diff --git a/testcases/web/demos/002_Tutorial-TwoSort.scala b/testcases/web/demos/002_Tutorial-TwoSort.scala
new file mode 100644
index 000000000..5a20fc6e6
--- /dev/null
+++ b/testcases/web/demos/002_Tutorial-TwoSort.scala
@@ -0,0 +1,52 @@
+import leon.lang._
+import leon.lang.synthesis._
+import leon.annotation._
+object TwoSort {
+/*
+ def sort2(x : BigInt, y : BigInt) = choose{(res: (BigInt,BigInt)) =>
+ Set(x,y) == Set(res._1, res._2) && res._1 <= res._2
+ }
+*/
+
+/*
+ def sort2(x : BigInt, y : BigInt) = {
+ ???[(BigInt, BigInt)]
+ } ensuring{(res: (BigInt,BigInt)) =>
+ Set(x,y) == Set(res._1, res._2) && res._1 <= res._2
+ }
+*/
+
+
+// def testSort2 = sort2(30, 4)
+
+/*
+ def sort2(x: BigInt, y: BigInt) = choose{(res: (BigInt,BigInt)) =>
+ sort2spec(x,y,res)
+ }
+
+ def sort2spec(x: BigInt, y: BigInt, res: (BigInt, BigInt)): Boolean = {
+ Set(x,y) == Set(res._1, res._2) && res._1 <= res._2
+ }
+
+ def unique2(x: BigInt, y: BigInt,
+ res1: (BigInt, BigInt),
+ res2: (BigInt, BigInt)): Boolean = {
+ require(sort2spec(x,y,res1) && sort2spec(x,y,res2))
+ res1 == res2
+ } holds
+ */
+
+/*
+ def sort3spec(x: BigInt, y: BigInt, z: BigInt, res: (BigInt,BigInt,BigInt)): Boolean = {
+ Set(x,y,z) == Set(res._1, res._2, res._3) &&
+ res._1 <= res._2 && res._2 <= res._3
+ }
+
+ def unique3(x: BigInt, y: BigInt, z: BigInt,
+ res1: (BigInt,BigInt,BigInt),
+ res2: (BigInt,BigInt,BigInt)): Boolean = {
+ require(sort3spec(x,y,z,res1) && sort3spec(x,y,z,res2))
+ res1 == res2
+ }.holds
+ */
+}
diff --git a/testcases/web/demos/003_Tutorial-Sort.scala b/testcases/web/demos/003_Tutorial-Sort.scala
new file mode 100644
index 000000000..f665aecc5
--- /dev/null
+++ b/testcases/web/demos/003_Tutorial-Sort.scala
@@ -0,0 +1,83 @@
+import leon.lang._
+import leon.lang.synthesis._
+import leon.annotation._
+object Sort {
+ sealed abstract class List
+ case object Nil 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 {
+ case Nil => Set()
+ case Cons(i, t) => Set(i) ++ content(t)
+ }
+ def c1 = content(Cons(15, Cons(5, Cons(15, Nil))))
+
+ def isSorted(l: List): Boolean = l match {
+ case Nil => true
+ case Cons(_,Nil) => true
+ case Cons(x1, Cons(x2, rest)) =>
+ x1 < x2 && isSorted(Cons(x2,rest))
+ }
+ def t1 = isSorted(Cons(10, Cons(20, Nil)))
+ def t2 = isSorted(Cons(15, Cons(15, Nil)))
+
+/*
+ def sortMagic(l: List) = {
+ ???[List]
+ } ensuring((res:List) =>
+ isSorted(res) && content(res) == content(l))
+*/
+
+ // def mm = sortMagic(Cons(20, Cons(5, Cons(50, Cons(2, Nil)))))
+ // try replacing 50 with 5
+
+
+
+
+
+/*
+ def sInsert(x: BigInt, l: List): List = {
+ require(isSorted(l))
+ l match {
+ case Nil => Cons(x, Nil)
+ case Cons(e, rest) if (x == e) => l
+ case Cons(e, rest) if (x < e) => Cons(x, Cons(e,rest))
+ case Cons(e, rest) if (x > e) => Cons(e, sInsert(x,rest))
+ }
+ } ensuring {(res:List) =>
+ isSorted(res) && content(res) == content(l) ++ Set(x)}
+ // size(res) == size(l) + 1
+*/
+
+ // We can also synthesize the body of sInsert interactively
+
+/*
+ def sInsert(x: BigInt, l: List): List = {
+ require(isSorted(l))
+ ???[List]
+ } ensuring {(res:List) =>
+ isSorted(res) && content(res) == content(l) ++ Set(x)}
+ */
+
+ // Fully automatic synthesis of sInsert also works
+
+/*
+ // Or, we can repair an incorrect (overly simplified) program
+ def sInsert(x: BigInt, l: List): List = {
+ require(isSorted(l))
+ l match {
+ case Nil => Cons(x, Nil)
+ case Cons(e, rest) => Cons(e, sInsert(x,rest))
+ }
+ } ensuring {(res:List) =>
+ isSorted(res) && content(res) == content(l) ++ Set(x)}
+ */
+
+}
--
GitLab