Example of using loop invariants plus assert, ensure, require in Scala.

Quick.scala

object Quick {

  def sort(xs: Array[Int]): Unit = {
    def go(lo: Int, hi: Int): Unit = {
      if (lo < hi) {
        val p = partition(xs, lo, hi)
        go(lo, p - 1)
        go(p + 1, hi)
      }
    }
    go(0, xs.length - 1)
  } ensuring(isSorted(xs))

  def partition(xs: Array[Int], lo: Int, hi: Int): Int = {
    require(lo <= hi, "Doesn't make sense to partition an empty (sub)array.")

    val pivot = xs(lo)
    var l = lo
    var r = hi

    def checkInvariant(stage: String): Unit = {
      assert(xs.slice(lo, l).forall(_ <= pivot), s"$stage: everything to the left of l = $l should be <= pivot = $pivot.")
      assert(xs.slice(r + 1, hi + 1).forall(_ > pivot), s"$stage: everything to the right of r = $r should be > pivot = $pivot.")
    }

    checkInvariant("initialization")
    while (l < r) {
      while (l < hi && xs(l) <= pivot) l += 1
      while (r > lo && xs(r) > pivot) r -= 1
      if (l < r) swap(xs, l, r)
      checkInvariant("maintenance")
    }
    swap(xs, lo, r)
    r
  }
}