Assertions

Assertions are useful both to document assumptions made by the code, and to verify them at runtime. Basic Storm provides special syntax for assertions. Both to make them stand out and to let them capture more information from the environment (e.g. source location and expression). In Storm, a failing assertion throws an core.AssertError exception.

Basic Storm provides two keywords for assertion. The first one, assert, accepts a condition and optionally a message. The second one, fail, just accepts a message and is intended to be used in situations where the condition would just be false.

The assert keyword is used in any of the two following forms (inspired by the syntax in Java): 

assert <expr>;
assert <expr> : <message>;

In the first form, assert only accepts an expression, <expr>, that should evaluate to core.Bool. If the expression evaluates to false, an core.AssertError is thrown. The exception contains a stack trace, the location of the failing assertion, and the text of the expression to aid debugging.

The second form also provides a message to be included in the exception. Note that <message> needs to be a string literal. It may, however, contain references to variables if desired (see interpolated strings).

For example, we could use an assertion as below: 

Int pow(Int base, Int exp) {
    assert exp >= 0;
    if (exp == 0) {
        return 1;
    } else {
        return pow(base, exp - 1);
    }
}

Note that it is often preferable to express constraints in types. For example, using core.Nat instead of core.Int as the second parameter if possible.

To include a more informative text, we can do it as follows: 

Int pow(Int base, Int exp) {
    assert exp >= 0 : "The exponent to 'pow' may not be negative.";
    if (exp == 0) {
        return 1;
    } else {
        return pow(base, exp - 1);
    }
}

As noted, we can include string interpolation in the message to include more information. However, note that the intention is to allow assertions to be disabled to save performance. As such, make sure that neither the expression nor the message has any side-effects that the program depends on.

The second form, fail, just accepts a message as follows: 

fail <message>;

It is equivalent to assert false : <message>; but does not include the word false in the assertion message. It is intended to be used in cases where no expression is needed, like below (we are assuming that this is an internal function where it should be the case that op has already been validated). 

Int apply(Str op, Int a, Int b) {
    if (op == "pow") {
        return pow(a, b);
    } else if (op == "+") {
        return a + b;
    } else if (op == "-") {
        return a - b;
    // ...
    } else {
        fail "Unknown operand.";
    }
}