Chapter: Sequences

This chapter introduces Slang sequences and principles for reasoning about them.

def swapZS(s: ZS, i: Z, j: Z): Unit = {
  Contract(
    Requires(0 <= i, i < s.size, 0 <= j, j < s.size),
    Modifies(s),
    Ensures(
      s.size == In(s).size,
      s(i) == In(s)(j),
      s(j) == In(s)(i),
      All(s.indices)(k => (k != i & k != j) ->: (s(k) == In(s)(k)))
    )
  )
  val t: Z = s(i)
  s(i) = s(j)
  s(j) = t
}