13 The Predicate Language
A predicate is written in a much smaller language than all of Liquid Shplait, consistent with what the solver can handle:
predicate ::= integer | #true | #false | true | false |
| identifier a parameter, the binder, or a top-level def |
| - predicate | ! predicate |
| predicate op predicate + - * / mod |
| predicate cmp predicate < <= > >= == != |
| predicate && predicate | predicate || predicate |
| ( predicate ) |
| if predicate | predicate | predicate |
| builtin(predicate, ...) max min add1 sub1 is_even is_odd |
| measure(identifier) length string_length is_empty is_cons |
| name(predicate, ...) a measure fun of this module |
| ctor(predicate, ...) a constructor of this module |
| unbox(identifier) a Boxof parameter |
| #'identifier a symbol, with == and != only |
A predicate may not call an ordinary function. The only exception is measure funs, which in turn are heavily restricted in what they can express [Measure Functions].
There is no one way to write a specification. Sometimes it is convenient to write it to look more like an equation: {y :: Int | y == max(a, b)}. In other cases it may make more sense to write it as a property with one solution: y >= a && y >= b && (y == a || y == b). The checker treats them alike.