A function contract is composed of a pre-condition and a post-condition in terms of a requires and an ensures clause. Similarly to chapter, we begin by introducing an informal notation with informal reasoning first and then provide Slang syntax.

In order to specify a contract for a function informally we write the following two clauses before the function body,

``````// requires: ...
// ensures: ...
``````

Using the formal Slang contract notation, we write

``````Contract(
Requires(...),
Ensures(...)
)
``````

## Functions

A function declaration in Slang is similar to a Scala function declaration. The only noticeable difference is the use of Slang types in the signature. The Slang type `B` corresponds to Scala’s `boolean` and `Z` to Sala’s `int`. Note however, that Slang’s `Z` is unbounded. For instance,

• a function to increment an integer number could have the signature
``````def incr(x: Z): Z
``````
• and a function to determine whether an integer number divides another
``````def divides(x: Z, y: Z): B
``````

We have an intuitive understanding of what we expect these functions to accomplish, consulting the informal description and relying on the naming of the functions. However, we would like to carry out rigorous correctness arguments similar to those presented in the preceding chapter. Supposing that the implementation of the functions could be arbitrarily complex, we begin by stating what is expected by providing a contract.

• For instance, the contract for `incr` could be specified as

``````def incr(x: Z): Z = {
// requires: true
// ensures: Res > x
}
``````

The ensures clause contains the term `Res` that refers to the result of the function. All we ensure is `Res > x`. In other words, `incr` may yield and increment of `x` of arbitrary size. Any expression `x + d` with `d` larger than `0` achieves this.

The requires clause specifies `true` which means it requires nothing. We can leave the clause away, getting a more concise version

``````def incr(x: Z): Z = {
// ensures: Res > x
}
``````

It is common to leave away trivial statements such as `requires: true`, although we specify them sometimes for emphasis. Think of it as docmumentation: Is it important to know?

We can implement incr by proving an expression in the function body

``````def incr(x: Z): Z = {
// ensures: Res > x
x + 1
}
``````

In order to verify that the property to be ensured holds, we have to should that the result `Res` is larger than `x`. The result returned is `x + 1`. If we substitute `Res` by `x + 1` in `Res > x`, we obtain `x + 1 > x`. This is true. So, we have verified that the implementation of the function fulfils its contract. A caller of the function only knows of the contract `Res > x` but not about the implementation, `Res = x + 1`. As a consequence, the function body could be changed to `x + 2` without affecting any correstness argument concerning function `incr`. This is why function contracts are often specified loose, permitting local changes to the implementation.

• Let’s specify a contract for `divides`.

``````def divides(x: Z, y: Z): B = {
// requires: y != 0
// ensures: Res == (x % y == 0)
}
``````

The contract of function `divides` contains a requires clause `y != 0`. This can be relied upon in the implementation. In the body and the ensures clause it can be assumed that `y != 0`. We see immediately that this is necessary for the post-condition in the ensures clause to be defined: The expression `x % y` requires `y` to be different from `0`. We can implement function `divides` in the obvious way

``````def divides(x: Z, y: Z): B = {
// requires: y != 0
// ensures: Res == (x % y == 0)
x % y == 0
}
``````

Substituting `x % y == 0` for `Res` in the ensures clause yields `(x % y == 0) == (x % y == 0)` which holds trivially.

## Logical Operators

The formulas in the preceding section do not use any logical operators. In programming languages one has to pay attention to the meaning of logical operators because they come in two flavours:

• Classical operators correspond to the common logical operators known from high-school maths.
• Short-circuit operators are closely linked to (efficient) execution of programs.

Slang use the symbols `&` and `|` for classical conjunction and disjunction, and `&&` and `||` for short-circuit conjunction and disjunction. The short-circuit operators only evaluate the second argument when necessary: `a && b` is true when `a` is true and `b` is true, and it is false when `a` is false whatever the value of `b`. The formula `a && b` could also be written `if a then b else false`. If `a` is false, then `b` is not evaluated. So, if `a` is false, it’s ok for `b` to be undefined. By contrast, the classical operators are always fully evaluated so that `a` and `b` must always be defined. Similarly, for disjunction.

The difference between classical and short-circuit operators might not appear far-reaching but it has a profound effect on the admitted reasoning. For instance, the following commutative law holds for classical conjunction but not for short-circuit conjunction (unless we can prove that both terms are always defined)

``````a & b == b & a
``````

Slang permits the two symbols `~` and `!` for negation.

## Quantification

There are two kinds of quantification in Slang: bounded and unbounded. Unbounded quantifiers correspond to the common (classical) logical operators. Bounded quantifiers are restricted to finite domains.

### Bounded Quantification

Bounded universal and existential quantification are avaible using the syntax `All(range)(fn)` and `Exists(range)(fn)`.

``````All(range)(fn)
``````
``````a & b == b & a
``````

### Unbounded Quantification

todo

Introduce classical quantifiers

## Pure and Strict Pure Functions

todo

pure: functional programming (nearly)

strictpure: permits defining predicates