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:
define nat as int where $ >= 0 nat abs(int x): return x
This defines a type . . . → Read More: Illustrating Compile-Time Verification in Whiley