Contracts that capture properties of data structures require understanding of additional subtleties for the In(...) and Modifies constructs and for the use of quantification. Consider the following method that takes a sequence of integers and squares each element of the sequence::

  def square(a: ZS): Unit = {
    Contract(
      Modifies(a),
      Case(
        "empty",
        Requires(a.size == 0),  // this case applies when input array is empty
        Ensures(
          a == In(a) // In(a) gives the input value of a in the pre-state of square
        )
      ),
      Case(
        "non-empty",
        Requires(a.size > 0),   // this case applies when input array not is empty
        Ensures(
          a.size == In(a).size, // nothing is added or removed from array (elements are only transformed)
          ∀(a.indices)(i => a(i) == In(a(i)) * In(a(i)))
          // a.indices returns a Slang "range" representing indices of a
          // can use All instead of ∀
          // In(a(i)) desugars to (In(a))(i)
        )
      )
    )

    for (i <- 0 until a.size) { // iterate with i,  0 <= i <= a.size
      Invariant(
        Modifies(a),           // a is modified by the loop
        a.size == In(a).size,  // a's size always equals its size at input
        ∀(0 until i)(j => a(j) == In(a(j)) * In(a(j))), // applies to part that has been processed
        ∀(i until a.size)(j => a(j) == In(a(j)))        // applies to part to be processed
      )
      a(i) = a(i) * a(i)
    }
  }

The above contract provides an additional example of Slang’s contract cases notation: one case addresses the situation where the sequence is empty, the second case addresses the non-empty case.

Before the cases, the Modifies clause indicates that parameter a may be modified by the method. Note that this is clearly a “may” as opposed to a “must” modality since, while the non-empty case modifies the sequence elements, the empty case does not. In other terms, the Modifies clause can be understood as being “conservative” and an “over-approximation” of what is actually modified.

In the “empty” case, In construct is used in the Ensure clause to indicate that the value of a in the post-state is equal to the value of a in the pre-state (indicated by In(a)). Recall that Slang’s equality == is value-based equality.

In the “non-empty” case, In is used within an object access expression ... . size to indicate that the field access applies to the value of the object in the pre-state. This clause of the contract captures a common idiom where one wants to indicate that the size of the data structure has not changed, even though the contents may be changed. This type of constraint is often necessary to ensure that reasoning about bounds violations proceeds as expected (if it is omitted, then Logika will consider that the size of the structure may have changed and so it is possible that sequence accesses that should be within bounds cannot be proven to be in bounds).

The other Ensures clause specifies how the sequence contents have been transformed: for each index i of the sequence, the sequence value at that position in the post-state is equal the square of the value at that position in the pre-state. Note that the use of In(a(i)) around the sequence indexing expression a(i) raises the question: can arbitrary forms of expressions be surrounded by In to indicate the given expression (not just a single variable) should be evaluated in the pre-state. The answer is “no”: technically, Slang Contracts In clause can only be applied to variables – in the example above, the syntactic sugar In(a(i)) is introduced as a convenience for (In(a))(i). In the desugared expression, Slang’s rule of “only apply In to variables” is followed. See Section insert reference to sequences/quantification section for an explanation of Slang’s quantification notation.

In the method body, the Invariant contract indicates properties that should hold true at the beginning and end of the loop body

Modifies(a) indicates that the sequence may be modified during the execution of the loop body. The next invariant constraint indicates that the size of the sequence is not changed: the sequence size is always equal to its size in the pre-state. The next constraint indicates what has been accomplished in the loop up to the present iteration: the value of each element of the sequence up to (but not including) the present index has been squared. The final constraint indicates that nothing has “messed with” the other elements in the sequence – they still match their values in the pre-state.