4 What Liquid Shplait Proves🔗ℹ

Checking is an extended form of assume-guarantee reasoning. A function’s body can assume the refinements on its parameters; it must guarantee the refinements on the return value. At each call, the caller must guarantee the parameters and can assume the refinements on what the function returns.

In the example below, safe_div assumes (i.e., requires) that its second parameter be non-zero. The function use expects its parameter to be greater than zero, which means it is non-zero. Thus, Liquid Shplait will establish that there are no (refinement) type errors in this program:

fun safe_div(n :: Int, {d :: Int | d != 0}) :: Int:

n / d

fun use({x :: Int | x > 0}) :: Int:

safe_div(100, x)        // x > 0 gives x != 0

Suppose we weaken use’s parameter to {x :: Int | true}. At that point, the call to safe_div is rejected, because use can no longer guarantee what safe_div assumes.

The branches of a conditional add information based on what predicates passed to arrive at that branch. In the first arm of an if, the test is known to be true, and in the second, false; each arm of an if or cond is checked separately. A match clause knows that the value matched is that constructor applied to the pattern variables.

A recursive call assumes the function’s own result refinement, so a specification by induction needs no extra annotation:

fun count(xs :: Listof(Int)) :: {y :: Int | y >= 0}:

match xs

| []: 0

| cons(h, t): 1 + count(t)

This is partial correctness: if a function does not terminate, we do not know anything about the result. Thus, every guarantee from Liquid Shplait comes with an implicit expectation that the function terminates.

Division and mod are modelled exactly as Shplait computes them: / truncates, and mod takes the sign of the divisor. That is why n / 2 fails for double above: when n is 1, the result is 0.