## Design by Contract with F#

This article presents a way to get design by contract in F#. Preconditions and postconditions may be grouped at the beginning of the function.

Some languages natively support design by contract features. F# includes an "assert" function. But this function is quite "imperative": it returns a unit type, which is not very nice in a functional code.

The following "ensure" function is easier to integrate in functional code. For example, it's easier to test return values (postconditions) with this function:

```[fsharp]
let ensure f x =
assert (f x)
x

let positive x = x >= 0

let rec fibo = function
| 0 | 1 -> 1
| n -> fibo (n - 1) + fibo (n - 2)
|> ensure positive
```

In Eiffel and in some other languages, preconditions and postconditions are grouped in the code, in order to make them more visible. It is possible to get a similar result with F#.

Let's define precondition and postcondition functions.

```[fsharp]
let postcondition cond f x =
let res = f x
assert (cond res)
res

let precondition cond f x =
assert (cond x)
f x
```

You can then add conditions to existing functions:

```[fsharp]
let checked_abs = abs |> postcondition positive
```

Here is a way to add conditions when defining a function. You can put as many conditions as you want, you can even call the famous memoize function:

```[fsharp]
// note: ^< is right associative
// <| may become right associative in a future release of F#.
let (^<) = (<|)

let rec fibo =
precondition positive  ^<
postcondition positive ^<
memoize                ^<
function
| 0 | 1 -> 1
| n -> fibo (n - 1) + fibo (n - 2)
```

I think this is a good example to show how high-order functions may greatly factor code. There's one limitation with the example: functions have only one argument. But it's easy to find a work around, let's define a curry function:

```[fsharp]
let curry f x y = f (x, y)

let rec foo =
curry                           ^<
precondition  (fst >> positive) ^<
precondition  (snd >> positive) ^<
postcondition positive          ^<
fun (x, y) ->
// ...

foo 4 2
```

1. On Monday, November 3 2008, 13:34 by Vesa Karvonen

I encourage you to look at:

Contracts for Higher-Order Functions
Robert Bruce Findler and Matthias Felleisen
ICFP 2002
citeseer.ist.psu.edu/find...

You might also be interested in my SML library for higher-order contracts. You can see the signature at mlton.org/cgi-bin/viewsvn... .