From acb2f8d38bcab702c63b8d641b36e1562efdf6f3 Mon Sep 17 00:00:00 2001
From: Viktor Kuncak <viktor.kuncak@epfl.ch>
Date: Mon, 27 Apr 2015 16:54:46 -0700
Subject: [PATCH] Added a web tutorial that expands on Sort and is listed on
0th position
---
testcases/web/demos/00_Tutorial.scala | 177 ++++++++++++++++++++++++++
1 file changed, 177 insertions(+)
create mode 100644 testcases/web/demos/00_Tutorial.scala
diff --git a/testcases/web/demos/00_Tutorial.scala b/testcases/web/demos/00_Tutorial.scala
new file mode 100644
index 000000000..dc8734368
--- /dev/null
+++ b/testcases/web/demos/00_Tutorial.scala
@@ -0,0 +1,177 @@
+import leon.lang._
+import leon.lang.synthesis._
+import leon.annotation._
+object Sort {
+// ==================================================================
+// 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 max(x: BigInt, y: BigInt): BigInt = {
+ val d = x - y
+ if (d > 0) x
+ else y
+} ensuring(res => res==rmax(x,y))
+
+def rmax(x: BigInt, y: BigInt) =
+ if (x <= y) x else 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))
+ */
+
+// ==================================================================
+// Sort 2-3 ELements
+// ==================================================================
+
+/*
+ def sort2(x : BigInt, y : BigInt) = choose{(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
+ */
+
+// ==================================================================
+// Sort a List
+// ==================================================================
+
+/*
+ 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 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 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
+*/
+
+/*
+ def insertMagic(x: BigInt, l: List): List = {
+ require(isSorted(l))
+ choose {(res: List) =>
+ isSorted(res) && content(res) == content(l) ++ Set[BigInt](x)
+ }
+ }
+*/
+
+ //def m = insertMagic(17, Cons(10, Cons(15, Cons(20, 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)))))
+
+}
--
GitLab