# Contract Semantics¶

## Assume-guarantee contracts¶

This section discusses the semantics of contracts, and in particular modes, in Kind 2. For details regarding the syntax, please see the Contracts section.

An *assume-guarantee contract* `(A,G)`

for a node `n`

is a set of *assumptions*
`A`

and a set of *guarantees* `G`

. Assumptions describe how `n`

**must** be
used, while guarantees specify how `n`

behaves.

More formally, `n`

respects its contract `(A,G)`

if all of its executions
satisfy the temporal LTL formula

That is, if the assumptions always hold then the guarantees hold. Contracts are
interesting when a node `top`

calls a node `sub`

, where `sub`

has a contract
`(A,G)`

.

From the point of view of `sub`

, a contract
`({a_1, ..., a_n}, {g_1, ..., g_m})`

represents the same verification
challenge as if `sub`

had been written

```
node sub (...) returns (...) ;
let
...
assert a_1 ;
...
assert a_n ;
--%PROPERTY g_1 ;
...
--%PROPERTY g_m ;
tel
```

The guarantees must be invariant of `sub`

when the assumptions are forced.

For the caller however, the call `sub(<params>)`

is legal **if and only if**
the assumptions of `sub`

are invariants of `top`

at call-site. The verification
challenge for `top`

is therefore the same as

```
node top (...) returns (...) ;
let
... sub(<params>) ...
--%PROPERTY a_1(<call_site>) ;
...
--%PROPERTY a_n(<call_site>) ;
tel
```

## Modes¶

Kind 2 augments traditional assume-guarantee contracts with the notion of
*mode*. A mode `(R,E)`

is a set `R`

or *requires* and a set `E`

of *ensures*.
A Kind 2 contract is therefore a triplet `(A,G,M)`

where `M`

is a set of modes.
If `M`

is empty then the semantics of the contract is exactly that of an
assume-guarantee contract.

### Semantics¶

A mode represents a *situation* / *reaction* implication. A contract `(A,G,M)`

can be re-written as an assume-guarantee contract `(A,G')`

where

For instance, a (linear) contract for non-linear multiplication could be

```
node abs (in: real) returns (res: real) ;
let res = if in < 0.0 then - in else in ; tel
node times (lhs, rhs: real) returns (res: real) ;
(*@contract
mode absorbing (
require lhs = 0.0 or rhs = 0.0 ;
ensure res = 0.0 ;
) ;
mode lhs_neutral (
require not absorbing ;
require abs(lhs) = 1.0 ;
ensure abs(res) = abs(rhs) ;
) ;
mode rhs_neutral (
require not absorbing ;
require abs(rhs) = 1.0 ;
ensure abs(res) = abs(lhs) ;
) ;
mode positive (
require (
rhs > 0.0 and lhs > 0.0
) or (
rhs < 0.0 and lhs < 0.0
) ;
ensure res > 0.0 ;
) ;
mode pos_neg (
require (
rhs > 0.0 and lhs < 0.0
) or (
rhs < 0.0 and lhs > 0.0
) ;
ensure res < 0.0 ;
) ;
*)
let
res = lhs * rhs ;
tel
```

**Motivation:** modes were introduced in the contract language of Kind 2 to
account for the fact that most requirements found in specification documents
are actually implications between a situation and a behavior.
In a traditional assume-guarantee contract, such requirements have to be
written as `situation => behavior`

guarantees. We find this cumbersome,
error-prone, but most importantly we think some information is lost in this
encoding.
Modes make writing specification more straightforward and user-friendly, and
allow Kind 2 to keep the mode information around to

improve feedback for counterexamples,

generate mode-based test-cases, and

adopt a defensive approach to guard against typos and specification oversights to a certain extent. This defensive approach is discussed in the next section.

### Defensive checks¶

Conceptually modes correspond to different situations triggering different
behaviors for a node. Kind 2 is *defensive* in the sense that when a contract
has at least one mode, it will check that the modes account for **all
situations** the assumptions allow before trying to prove the node respects
its contract.

More formally, consider a node `n`

with contract

The defensive check consists in checking that the disjunction of the requires of each mode

is an invariant for the system

If `one_mode_active`

is indeed invariant, it means that as long as

the assumptions are respected, and

the node is correct

*w.r.t.*its contract then at least one mode is active at all time.

Kind 2 follows this defensive approach. If a mode is missing, or a requirement is more restrictive than it should be then Kind 2 will detect the modes that are not exhaustive and provide a counterexample.

This defensive approach is not as constraining as it first appears. If one wants to leave some situation unspecified on purpose, it is enough to add to the current set of (non-exhaustive) modes a mode like

```
mode base_case (
require true ;
) ;
```

which explicitly accounts for, and hence documents, the missing cases.

In addition, Kind 2 checks that all modes are reachable in the system. In other words, Kind 2 also checks that for each mode there exists a reachable state satisfying the conjunction of its requires. This lets you know whether the mode implication is vacuously true or not.

When the node associated to the contract has a body (it is not imported), the check will be performed twice. First, considering only the information of the contract. Then, considering the equations of the body too.

Notice that when running Kind 2 in modular mode, the reachability check is performed locally to a node without taking call contexts into account; only the specified assumptions are considered.

You can disable this check by passing `--check_nonvacuity false`

to Kind 2,
or by suppressing all reachability checks (`--check_reach false`

).