3 Refinements
Refinements attach to names, adding a predicate: e.g.,
{n :: Int | n > 0}
This notation should remind you of set notation from math. Vocalize the above as “n is an Int, where n is greater than 0”. Read the stick as “where”.
Liquid Shplait is a limited language meant primarily for educational purposes, so it supports only limited forms of writing refinements. They may appear in the following positions:
a fun result: fun f(n :: Int) :: {y :: Int | y >= 0}: n * n;
a Boxof element: b :: Boxof({v :: Int | v >= 0});
a datatype field: circle(radius :: {r :: Int | r > 0}).
The fun or def must be at the top level of the module. A refinement anywhere else is a compile-time error (Limitations).
You might notice in the examples above that we associate names even with the return value of a function (such as y above), which we don’t normally do. This is so that we can explicitly refer to, and refine, the return value. This name is only bound in that predicate.
Some predicates can refer to other names. A return’s predicate can refer to the function’s parameters:
fun percent_of({total :: Int | total >= 0},
{pct :: Int | pct >= 0 && pct <= 100})
:: {out :: Int | out >= 0 && out <= total}:
A parameter’s predicate may mention the other parameters, too. At a call, each parameter in a predicate stands for the corresponding argument:
fun safe_get(s :: String, {i :: Int | i >= 0 && i < string_length(s)}) :: Char:
string_get(s, i)
safe_get("hello", 1) // accepted
safe_get("hello", 7) // rejected: 7 < string_length("hello") is false
The predicate true is always true. It can be useful while debugging as you’re trying to figure out the exact claim. The predicate #false is never true, so it identifies situations that can never occur (for instance, unreachable code: see error, unreachable and assert).
Top-level definitions are immutable, so a function may use them in its refinements and its body. If you use a def with a refinement, that refinement applies to its use as well. You can also refer to top-level constants, which is useful for eliminating “magic constants” inside refinements:
def TICKET_COST = 2
fun unlock({credit :: Int | credit >= TICKET_COST}) :: Int:
credit - TICKET_COST