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 visible “outside” of the method (e.g., “global” variables) 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.

Assume / Guarantee Reasoning

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 (note: we use the special symbol x_old after the call to incBy to refer to the value of x before 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. For some intuition about how the precondition applies to the calling context, we can view the formal parameter y to be instantiated with the actual parameter a in the contract precondition to obtain the verification obligation a > 0 that must be met in the calling context immediately before the call.

Assume/Guarantee - Client - Pre-condition

Logika marks this verification obligation with a bolt at the call site at Line 26 as shown in the figure above. The verification obligation sequent shown in the right pane indicates that the Logika process is actually a bit less direct than the intuition presented above.

; x@5 === 0,     // initialization of x
; x === 5,       // assignment to x
; temp === x,    // assignment to temp
; a === 4,       // assignment to a
; y === a        // bind caller's actual parameter a to formal parameter y of called method
; ⊢
; y > 0          // check that pre-condition of called procedure is satisfied

In particular, as illustrated in the comments in the sequent above, the sequent antecedents include known facts resulting from assignment statements. The effect of a substitution of the actual parameter for the formal parameter described in the “intuition” above is realized as an equality constraint between the formal parameter y and the actual parameter a. Given this equality constraint, the constraint y > 0 to be verified is equivalent to a > 0.

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

Clicking on the light bulb for the assertion at Line 28 reveals known facts that include constraints from the called methods contract (excerpts are shown below). Note that the identifiers for logic variables generated from the message contract are prefixed by “incBy. ..”.

...
At[Z]("incBy.y", 0) == a;   // binding of formal parameter ``y`` to actual parameter ``a``
At[Z]("incBy.y", 0) > 0;    // pre-condition
x == At(x, 1) + At[Z]("incBy.y", 0) & x > At(x, 1) &  
     At[Z]("incBy.Res", 0) == x; // post-condition
z == At[Z]("incBy.Res", 0)  // binding of return value to context variable ``z`` receiving 
                            //   result of called method

These facts, resulting from called method’s contract, gives knowledge that the client can rely on after the call.

Assume/Guarantee - Client - Assertion

As shown in the bolt information for the assertion at Line 28 in the figure above, this is sufficient information to verify that the updated value of x is greater than the value of x before the call (as reflected by the value of temp).

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. Corresponding to the idea of “getting to assume”, within the Logika verification process, the presence of the pre-condition Requires(y > 0) causes y > 0 to be added to the set of known facts at the beginning of the method body.

Assume/Guarantee - Service - Pre-condition

In the figure above, the developer has clicked on the lightbulb at the first line in the method (Line 13), and y > 0 appears in the known facts.

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. Corresponding to the idea of “must guarantee”, within the verification process, Logika will generate a verification obligation (corresponding to the presence of the lightning bolt at Line 11).

Assume/Guarantee - Service - Post-condition

In the figure above, the developer has clicked on the bolt at the contract post-condition, the the Logika output panel shows the sequent that needs to be proven. Essentially, it needs to be shown that from the known facts at the end of the method that the post-condition can be established. The listing below presents an annotated version of the sequent.

; Sequent:
;
; y > 0,           // from pre-condition
; x === x@10 + y,  // from method body code
; Res === x        // setting the 'Res' identifier to the value of the return expression
; ⊢
; (x == x@10 + y & x > x@10) & Res == x  // post-condition

Even though our example method is trivial, the sequent reflects that general structure that one sees in Logika post-condition verification obligations for all methods.

Sequent Antecedent (accumulated knowledge)

  • known facts from pre-condition: the first fact corresponds to the constraint that one gets to assume from the pre-condition,
  • known facts from method body code: the second fact corresponds to the knowledge that Logika accumulates when processing the method body,
  • binding ‘Res’ to result expression: the final fact introduces an equality constraint between (a) the keyword ‘Res’ that the developer can use in contracts to refer to the methods return value and the (b) a logical expression corresponding to the return expression in the code (in this case, the single variable x),

Sequent Consequent (constraint to prove)

  • the post-condition clause to be proven: the expression in the current post-condition clause is presented in terms of the logical variables of the method. Note that the In(x) expressions from the post-condition are translated to a logic variable that identifies the value of x at the beginning of the method.

For the contract frame condition (Modifies clause), the method implementation must also guarantee that only externally visible variables modified in the method are listed in the Modifies clause (in this case, 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. Logika will check this property holds as part of its automated verification process.

Assume/Guarantee - Concepts

The figure above summarizes the key concepts associated with the assume/guarantee pattern, including how the called method’s (service’s) contract gives rise to verification obligation and verification knowledge for both the service and client.

TBD: Insert exercises at this point

Omitting Sections of a Method Contract

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.

Using Contracts to Capture Important Properties Rather Than Full Behavior

The previous section illustrates an important point about the contract paradigm: contracts do not always need to completely specify the behavior of a method or system to be useful. For example, the absValue method contract did not completely specify the functional behavior (e.g., indicating given a negative value -v that the corresponding positive value v would be returned). It simply indicated that the result would be non-negative.

Eventually say more here with additional examples

Contract Cases

Sometimes contracts can be specified (and even verified) more easily when they are organized according to different cases of input – and Slang Contracts provides a special notation to support that. Reference intuition for breaking proofs into cases from the math world.

The following example illustrates a variant of the absValue method/contract above that uses Slang’s contract cases::

  def absValueCases(y: Z): Z = {
    Contract(
      Modifies(),
      // case for negative input
      Case("Negative",          // optional string label
           Requires(y < 0),     // condition on input for this case to apply
           Ensures(Res == -y)   // post-condition for this case
      ),
      // case for non-negative input
      Case("Non-negative",      // optional string label
        Requires(y >= 0),       // condition on input for this case to apply
        Ensures(Res == y))      // post-condition for this case
    )

    var ans: Z = 0
    if (x < 0) {
      ans = -y
    } else {
      ans = y
    }
    return ans
  }

There must be a single Modifies clause for contract cases (or the clause can be omitted when no non-local is modified) because Logika does not support a notion of conditional modification (this makes the rest of the verification framework more challenging).

One or more [Robby is “one or more correct”?] Case clauses are used, where each Case typically includes both a Requires stating some condition on the input (the case pre-condition) and an Ensures clause indicating the properties (the case post-condition) that must hold in the post-state when the case pre-condition is true.

Address the following: overlapping requires, non-exhaustive requires, ordering of cases (e.g., when overlapping), omitting requires, omitting ensures.