Function Contracts
A function contract is composed of a precondition and a postcondition 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 asdef 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 isRes > x
. In other words,incr
may yield and increment ofx
of arbitrary size. Any expressionx + d
withd
larger than0
achieves this.The requires clause specifies
true
which means it requires nothing. We can leave the clause away, getting a more concise versiondef 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 thanx
. The result returned isx + 1
. If we substituteRes
byx + 1
inRes > x
, we obtainx + 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 contractRes > x
but not about the implementation,Res = x + 1
. As a consequence, the function body could be changed tox + 2
without affecting any correstness argument concerning functionincr
. 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 clausey != 0
. This can be relied upon in the implementation. In the body and the ensures clause it can be assumed thaty != 0
. We see immediately that this is necessary for the postcondition in the ensures clause to be defined: The expressionx % y
requiresy
to be different from0
. We can implement functiondivides
in the obvious waydef divides(x: Z, y: Z): B = { // requires: y != 0 // ensures: Res == (x % y == 0) x % y == 0 }
Substituting
x % y == 0
forRes
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 highschool maths.
 Shortcircuit operators are closely linked to (efficient) execution of programs.
Slang use the symbols &
and 
for classical conjunction and disjunction,
and &&
and 
for shortcircuit conjunction and disjunction. The shortcircuit 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 shortcircuit operators might not appear farreaching but it has a profound effect on the admitted reasoning. For instance, the following commutative law holds for classical conjunction but not for shortcircuit 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