Added a web tutorial that expands on Sort and is listed on 0th position

testcases/web/demos/00_Tutorial.scala

+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)))))
+
+}