In general, method contracts capture properties that client code (code that calls the method) should understand to be able to invoke the method correctly and to correctly rely on its results.

Client Perspective

The following illustrates a call by a client of the incBy “service”. Comments have been added to code to indicate the verification obligations that met before calling the service as well as the knowledge that the client can rely on after the call::

  var a : Z = 4

  // V-OBLG: client must guarantee pre-condition is satisfied
  //   pre-condition interpreted in calling context:
  //     a > 0

  val z = incBy(a)

  // V-KNOW: client gets to assume that post-condition is satisfied
  //   post-condition interpreted in calling context:
  //     x == x_old + a
  //     x > x_old
  //     z == x

  // V-KNOW: client gets to assume that no variable in its context
  //   other than x is changed.  In particular, a has not changed,
  //   so any knowledge of a before the call is still valid after the
  //   call.

Before the call, the client must guarantee that the pre-condition is satisfied. The method’s precondition y > 0 is stated in terms of its formal parameter y. To understand how the precondition applies to the calling context, one instantiates the formal parameter y with the actual parameter a to obtain the condition a > 0 that must be met in the calling context immediately before the call.

After the call, the client gains knowledge based on what the service stated it would achieve in the post-condition. incBy has three clauses in its post-condition:

• x == In(x) + y
• x > In(x)
• Res == x

Instantiating these clauses to the client’s context gives the knowledge that the client can rely on after the call:

• x == x_old + a …replacing In(x) by x_old – the value of x after the call is equal to the value of x before the call plus a (which was passed as a parameter to the service).
• x > x_old …replacing In(x) by x_old – the value of x after the call is greater than the value of x before the call.
• z == x …replacing Res by z – the variable z which received the return value of the call is equal to the value of x after the call.

Service Perspective

We repeat the method code above, adding comments to indicate the reasoning principles for the Assume/Guarantee paradigm from the service’s perspective::

  var x: Z = 0

  def incBy(y: Z): Z = {
    Contract(
      Requires(y > 0),
      Modifies(x),
      Ensures(x == In(x) + y & x > In(x) & Res == x)
    )
    // V-KNOW: Service gets to assume pre-condition is satisfied
    //   y > 0
    x = x + y
    // V-OBLG: Service must guarantee only non-local variable modified is x
    // V-OBLG: Service must guarantee post-condition
    //   x == In(x) + y
    //   x > In(x)
    //   x == x  (substituting x for Res in the post-condition)
  return x
  }

At the beginning of the method body, because all calls of the method will be checked by Logika to ensure that the pre-condition is satisfied, the service gets to assume (i.e., has the knowledge) that y > 0.

At the end of the method body, the implementer of the service must guarantee that the post-condition has been met. In the third clause of the post-condition, the Res keyword stands for the result of the method. From the implementor’s perspective, Res is computed by the expression used in the return statement, in this case by the variable x from return x.

The implementer must also guarantee that the frame condition has been met (only x is modified). Conceptually, this is a property that is achieved throughout the method body’s execution, not just at the end of the method.