The following example captures the most fundamental aspects of Slang Contracts::

  var x: Z = 0

  def incBy(y: Z): Z = {
    Contract(
      Requires(y > 0),                                // pre-condition
      Modifies(x),                                    // frame-condition
      Ensures(x == In(x) + y & x > In(x) & Res == x)  // post-condition
    )
    x = x + y
    return x
  }

In this example (contrived for the purpose of illustration), a “global” variable x is defined, and an incBy method is defined to increment x by the value supplied via parameter y. As a conveniece the method returns the value of x after the increment.

The method has a contract made up of several parts:

• a pre-condition stated using the Requires keyword that indicates properties that must hold when the method is called. In this case, the method should always be called with the parameter y having a value greater than 0. The Logika verifier will automatically check that all calls to the method fulfill this property.
• a post-condition stated using the Ensures keyword indicates properties that must hold when the the method completes and control returns to the caller. In this case, the method should ensure that the value of x in the post-state is equal to the value of x in the pre-state plus the value of y. Slang provides the In notation to enable expressions in the post-condition and other proof contexts to reference the value of x in the pre-state (In is not used in the pre-condition because pre-condition expressions are always/only interpreted in terms of the pre-state). The method should also ensure that the resulting value of the method is equal to the value of x in the post-state. Slang provides the Res notation to refer to method’s return value. The Logika verifier will automatically check that the method implementation fulfills this property (guaranteeing that all possible calls/executions of the method that satisfy the pre-condition will lead to the post-condition being satisfied).
• a frame condition stated using the Modifies keyword indicates the variables “outside” of the method that may be modified due to the method’s execution (it implicitly indicates that the method must not modify any other variables outside the method). This is useful for clients of the method to know because if they were depending on properties of variables listed in the modifies clause, the clause indicates that those properties may be invalidated due to changes in the variables. Contract elements like modifies (different names/keywords are used in different contract languages) have historically been called frame conditions because they “frame” the state of the program that (a) the method may change and (b) the method must not change.