BubbleFun.scala

object BubbleFun {

    // --------------------- sort ----------------------

    def sort(a: Map[Int,Int], size: Int): Map[Int,Int] = ({
      require(isArray(a, size) && size < 5)

      val i = size - 1
      val t = sortWhile(0, a, i, size)
      t._2
    }) ensuring(res => isArray(res, size) && sorted(res, size, 0, size-1) /*&& content(res, size) == content(a, size)*/)

    def sortWhile(j: Int, sortedArray: Map[Int,Int], i: Int, size: Int) : (Int, Map[Int,Int], Int) = ({
      require(i >= 0 && i < size && isArray(sortedArray, size) && size < 5 &&
              sorted(sortedArray, size, i, size - 1) &&
              partitioned(sortedArray, size, 0, i, i+1, size-1))

      if (i > 0) {
        val t = sortNestedWhile(sortedArray, 0, i, size)
        sortWhile(t._2, t._1, i - 1, size)
      } else (j, sortedArray, i)
    }) ensuring(res => isArray(res._2, size) && 
                       sorted(res._2, size, res._3, size - 1) &&
                       partitioned(res._2, size, 0, res._3, res._3+1, size-1) &&
                       res._3 >= 0 && res._3 <= 0 /*&& content(res._2, size) == content(sortedArray, size)*/
               )


    def sortNestedWhile(sortedArray: Map[Int,Int], j: Int, i: Int, size: Int) : (Map[Int,Int], Int) = ({
      require(j >= 0 && j <= i && i < size && isArray(sortedArray, size) && size < 5 &&
              sorted(sortedArray, size, i, size - 1) &&
              partitioned(sortedArray, size, 0, i, i+1, size-1) &&
              partitioned(sortedArray, size, 0, j-1, j, j))
      if(j < i) {
        val newSortedArray = 
          if(sortedArray(j) > sortedArray(j + 1))
            sortedArray.updated(j, sortedArray(j + 1)).updated(j+1, sortedArray(j))
          else
            sortedArray
        sortNestedWhile(newSortedArray, j + 1, i, size)
      } else (sortedArray, j)
    }) ensuring(res => isArray(res._1, size) &&
                       sorted(res._1, size, i, size - 1) &&
                       partitioned(res._1, size, 0, i, i+1, size-1) &&
                       partitioned(res._1, size, 0, res._2-1, res._2, res._2) &&
                       res._2 >= i && res._2 >= 0 && res._2 <= i /*&& content(res._1, size) == content(sortedArray, size)*/)


    //some intermediate results
    def lemma1(a: Map[Int, Int], size: Int, i: Int): Boolean = ({
      require(isArray(a, size) && size < 5 && sorted(a, size, i, size-1) && partitioned(a, size, 0, i, i+1, size-1) && i >= 0 && i < size)
      val t = sortNestedWhile(a, 0, i, size)
      val newJ = t._2
      i == newJ
    }) ensuring(_ == true)
    def lemma2(a: Map[Int, Int], size: Int, i: Int): Boolean = ({
      require(isArray(a, size) && size < 5 && sorted(a, size, i, size-1) && partitioned(a, size, 0, i, i+1, size-1) && i >= 0 && i < size)
      val t = sortNestedWhile(a, 0, i, size)
      val newA = t._1
      val newJ = t._2
      partitioned(newA, size, 0, i-1, i, i)
    }) ensuring(_ == true)
    def lemma3(a: Map[Int, Int], size: Int, i: Int): Boolean = ({
      require(partitioned(a, size, 0, i, i+1, size-1) && partitioned(a, size, 0, i-1, i, i) && isArray(a, size) && size < 5 && i >= 0 && i < size)
      partitioned(a, size, 0, i-1, i, size-1)
    }) ensuring(_ == true)
    def lemma4(a: Map[Int, Int], size: Int, i: Int): Boolean = ({
      require(isArray(a, size) && size < 5 && sorted(a, size, i, size-1) && partitioned(a, size, 0, i, i+1, size-1) && i >= 0 && i < size)
      val t = sortNestedWhile(a, 0, i, size)
      val newA = t._1
      partitioned(newA, size, 0, i-1, i, size-1)
    }) ensuring(_ == true)


    //  --------------------- sorted --------------------
    def sorted(a: Map[Int,Int], size: Int, l: Int, u: Int) : Boolean = {
      require(isArray(a, size) && size < 5 && l >= 0 && l <= u && u < size)
      val t = sortedWhile(true, l, l, u, a, size)
      t._1
    }

    def sortedWhile(isSorted: Boolean, k: Int, l: Int, u: Int, a: Map[Int,Int], size: Int) : (Boolean, Int) = {
      require(isArray(a, size) && size < 5 && l >= 0 && l <= u && u < size && k >= l && k <= u)
      if(k < u) {
        sortedWhile(if(a(k) > a(k + 1)) false else isSorted, k + 1, l, u, a, size)
      } else (isSorted, k)
    }



    // ------------- partitioned ------------------
    def partitioned(a: Map[Int,Int], size: Int, l1: Int, u1: Int, l2: Int, u2: Int) : Boolean = {
      require(isArray(a, size) && size < 5 && l1 >= 0 && u1 < l2 && u2 < size)
      if(l2 > u2 || l1 > u1) 
        true
      else {
        val t = partitionedWhile(l2, true, l1, l1, size, u2, l2, u1, a)
        t._2
      }
    }
    def partitionedWhile(j: Int, isPartitionned: Boolean, i: Int, l1: Int, size: Int, u2: Int, l2: Int, u1: Int, a: Map[Int,Int]) : (Int, Boolean, Int) = {
      require(isArray(a, size) && size < 5 && l1 >= 0 && l1 <= u1 && u1 < l2 && l2 <= u2 && u2 < size && i >= l1)

      if(i <= u1) {
        val t = partitionedNestedWhile(isPartitionned, l2, i, l1, u1, size, u2, a, l2)
        partitionedWhile(t._2, t._1, i + 1, l1, size, u2, l2, u1, a)
      } else (j, isPartitionned, i)
    }
    def partitionedNestedWhile(isPartitionned: Boolean, j: Int, i: Int, l1: Int, u1: Int, size: Int, u2: Int, a: Map[Int,Int], l2: Int): (Boolean, Int) = {
      require(isArray(a, size) && size < 5 && l1 >= 0 && l1 <= u1 && u1 < l2 && l2 <= u2 && u2 < size && j >= l2 && i >= l1 && i <= u1)

      if (j <= u2) {
        partitionedNestedWhile(
          (if (a(i) > a(j))
            false
          else
            isPartitionned), 
          j + 1, i, l1, u1, size, u2, a, l2)
      } else (isPartitionned, j)
    }


    //------------ isArray -------------------
    def isArray(a: Map[Int,Int], size: Int): Boolean = 
      if(size <= 0)
        false
      else
        isArrayRec(0, size, a)

    def isArrayRec(i: Int, size: Int, a: Map[Int,Int]): Boolean = 
      if (i >= size)
        true
      else {
        if(a.isDefinedAt(i))
          isArrayRec(i + 1, size, a)
        else
          false
      }


    // ----------------- content ------------------
    def content(a: Map[Int, Int], size: Int): Set[Int] = {
      require(isArray(a, size) && size < 5)
      var i = 0
      var s = Set.empty[Int]
      while(i < size) {
        s = s ++ Set(a(i))
        i = i + 1
      }
      s
    }

}