7 Measure Functions
Sometimes a predicate needs to depend on something more complicated than a constant. For this, Liquid Shplait provides measures. A measure fun is a function that predicates may call. Its body is a single match on a datatype parameter, with one clause per constructor, each written in the predicate language (The Predicate Language). In the following example, OList reflects an ordered list (in ascending order):
type OList
| onil()
| ocons(hd :: Int, tl :: {t :: OList | is_onil(t) || ohd(t) >= hd})
measure fun is_onil(l :: OList) :: Boolean:
match l
| onil(): #true
| ocons(h, t): #false
measure fun ohd(l :: OList) :: Int:
match l
| onil(): 0
| ocons(h, t): h
The second field of ocons says the list is sorted. A measure function is available as an ordinary function that can be used in the program. However, it is also available to the checker as a recursive function that the solver interprets exactly. A refinement can, for instance, therefore say what inserting into an ordered list does to its head, and the checker proves it for this key function in insertion sort:
fun insert(x :: Int, xs :: OList)
:: {r :: OList | !is_onil(r)
&& ohd(r) == (if is_onil(xs) | x | min(x, ohd(xs)))}:
match xs
| onil(): ocons(x, onil())
| ocons(y, ys):
| ocons(x, ocons(y, ys))
| ocons(y, insert(x, ys))
The result is never empty; its head is x if xs was empty; otherwise, the head is the smaller of x and the old head.
An important limitation of measure functions is that they must be total. That means they must provide a value even when no meaningful one exists: e.g., the 0 above in the onil case. When using measure functions, either make this value meaningless, or guard against it ever being used (e.g., only caring about the value of ohd in the ocons case).
Lists and strings are not modelled themselves, but a predicate may refer to them through the measures length, string_length, is_empty and is_cons.