Constraints

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.