Example
You can assert that parameters have certain values with requires.
int fib (int i) requires (i > 0) {
if (i == 1) {
return i;
} else {
return fib (i - 1) + fib (i - 2);
}
}
fib (-1);
You won't get any error during the compilation, but you'll get an error when running your program and the function won't run.
You can also assert that the return value matches a certain condition with ensures
int add (int a, int b) ensures (result >= a && result >= b) {
return a + b;
}
You can have as many requires and ensures as you want.
