9 error, unreachable and assert🔗ℹ

A call to error never returns. Therefore, every claim about the result holds on every path that reaches one. This makes error useful for cases not yet written and for run-time failures:

fun big({n :: Int | n > 0}) :: {r :: Int | r > 5}:

if n > 5

| n

| error(#'big, "too small")

The non-error paths are still checked.

However, sometimes we want to make a stronger claim: that some piece of code can never be reached. For instance, we may match across a datatype, but a refinement may tell us that some of those cases can never occur. For this, we can use unreachable(). This is a strong claim: that this body of code will never be called. If Liquid Shplait cannot prove that, it signals a static error. Therefore, use unreachable instead of error when that’s what you mean to signal.

fun sign({n :: Int | n != 0}) :: {s :: Int | s == 1 || s == -1}:

cond

| n > 0: 1

| n < 0: -1

| ~else: unreachable()

Without the precondition, sign is rejected:

Sometimes we want to make a claim about a particular predicate at some point in a program. assert(P) claims that P holds where it is written. P must follow from the assumptions there, and the rest of the body may then assume it:

fun midpoint({lo :: Int | lo >= 0}, {hi :: Int | hi >= lo})

:: {m :: Int | m >= lo && m <= hi}:

def half = (hi - lo) / 2

assert(half >= 0 && half <= hi - lo)

lo + half

The assert states, and the checker proves, the key fact that the result depends on. If we change the assertion to assert(half > 0), this produces an error:

Both unreachable and assert will signal an error at run time (the latter only if the predicate fails). Code inside the module, which has been checked by Liquid Shplait, can never trigger these run-time errors barring an error in the language. However, code in other modules is not checked (Limitations); it may violate refinement assertions, and hence can trigger these errors.