# Illustrating Compile-Time Verification in Whiley

With the latest release of Whiley, compile-time checking of constraints can be enabled with a command-line switch.  So, I thought a few examples of this were in order.

## Example: Absolute of an Integer

Consider this simple program:

``````type nat is (int x) where x >= 0

function abs(int x) -> nat:
return x
``````

This defines a type `nat` which is an `int` whose values are non-negative.  The function abs`(int)` accepts an `int` and returns a `nat`.  However, it contains a bug because `int` does not subtype `nat` (since `int` includes negatives whilst `nat` does not).  We can compile this on the command-line like so:

``````./example.whiley:4: constraint not satisfied
return x
^^^^^^^^
``````

The command-line switch `-X verification:enable=true` turns on compile-time verification. This is not enabled by default because it is experimental. As we can see, the compiler has correctly spotted the error on line 4. We can fix the code like so:

``````type nat is (int x) where x >= 0

function abs(int x) -> nat:
if x >= 0
return x
else:
return -x
``````

This will now compile correctly with verification enabled.  As you can see the verifier is able to correctly reason about the effect of conditional statements.

## Example: Maximum of two Integers

As another illustration, consider the following (broken) implementation of the `max(int,int)` function:

``````function max(int x, int y) -> int:
if x < y:
return x
else:
return y
``````

At this point, the function does the opposite of what you would expect (i.e. it computes the minimum of `x` and `y` because of a bug). However, the function will compile with verification enabled because the code meets the given specification. Let us improve the specification a little by introducing some constraints:

``````function max(int x, int y) -> (int r)
ensures r == x || r == y:
if x < y:
return x
else:
return y
``````

The given constraint states the return value `r` is equal to either `x` or `y`. However, this constraint is not strong enough to enforce that the maximum of `x` and `y` is returned. Hence, the code still compiles even with verification enabled. Finally, we add the missing bit:

``````function max(int x, int y) -> (int r)
ensures (r == x || r == y) && x <= r && y <= r:
if x < y:
return x
else:
return y
``````

Compiling the above with verification enabled now gives the following error:

``````./max.whiley:3: postcondition not satisfied
return x
^^^^^^^^
``````

At this point, we can fix the bug by changing the condition to be `if x > y` and it will compile correctly with verification enabled.