Function Contracts

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