Sections of a method contract may be omitted. The following abstract value example abs does not include a pre-condition since it does not need to make any assumptions about its inputs (i.e., it “works” for all possible inputs of the argument type). And, since the the method does not modify a non-local variable, the modifies section can be omitted::

  def absValue(y: Z): Z = {
    Contract(
      Ensures(Res >= 0)
    )
    var ans: Z = 0
    if (x < 0) {
      ans = -y
    } else {
      ans = y
    }
    return ans
  }

Omitting a pre-condition is semantically equivalent to stating that the pre-condition is always satisfied, no matter how the method is called. To emphasize this point, one can explicitly include a Requires clause with a body T::

  Contract(
    Requires(T),
    Ensures(Res >= 0)
  )

A trivial Modifies clause (one with no entries) can also be included if one wishes to make a visually explicit indication that “nothing” is modified::

  Contract(
    Requires(T),
    Modifies(),
    Ensures(Res >= 0)
  )

Post-conditions can also be omitted. This is common early on in the development process where one is prototyping and only using contracts to indicate situations where bad inputs could cause problems like run-time exceptions or where the input domain for which the method is defined is limited. For example, one might want to rule out negative inputs for a square root or factorial function without saying anything about the result::

  def factorial(y : Z): Z = {
      Contract(
      Requires(y >= 0)
    )
    ...
  }

In such situations, the service contract is making no “promises” to clients about what the service will do. However, it is still provides valuable information by indicating that the function is only defined for non-negative values.