A critical advantage of Whiley over other programming languages, such as Java or C#, is the ability to define constrained types. A constrained type is simply a type with a specific constraint imposed upon it. For example, the type of natural numbers can be defined like so:

define nat as int where $ >= 0

Here, “`$`

” is used to refer to the value held by a variable of type `nat`

. Thus, we see that `nat`

is an `int`

whose values are never negative. Any attempt to pass a negative number to a variable of type `nat`

will result in a compile-time error. The following program illustrates some simple methods:

nat f(nat x): return x + 1 // always OK nat g(nat x): return x - 1 // always a compile-time error nat h(int y): x = y // always a compile-time error

Whiley reasons about the values of variables in a modular fashion. That is, it considers all the available information and attempts to determine whether a particular state is invalid or not. In the above example, the first function `f()`

is valid because incrementing a natural number always gives a natural number. However, subtracting one from a natural number may give a negative number. Hence, function `g()`

is considered invalid as `x`

could be zero on entry. A similar argument applies for function `h()`

.

Type constraints are not limited to primitive types, and can be used on any type. The following provides some more interesting examples:

define nelist as [int] where |$| > 0 // non-empty list define zlist as {int} where !(0 in $) // cannot contain 0 define dim as {int low, int high} where low < high

By using quantifiers, you can define more useful constraints on lists and sets. For example:

define pset as {int} where no { x in $ | x < 0 }

This defines a set type where no element can be negative (or, conversely, where every element must be a natural number). We can define this equivalently like so:

define nat as int where $ >= 0 define pset as {nat}

Whiley simply inlines the above definition for `nat`

into that for `pset`

, arriving at something similar to the previous definition.