11 Mutable State
Liquid Shplait allows a small amount of mutable state to be combined with refinements. It permits writing a refinement on a Boxof element. Every write must re-establish it, so every read may assume it:
fun bump(b :: Boxof({v :: Int | v >= 0})) :: Void:
bump(counter)
Liquid Shplait has not been proven sound, and state interacts with the other features of the language in odd ways. Therefore, use it with caution. Nevertheless, to try to ensure soundness, there are various restrictions on boxes. A Boxof parameter may appear only in unbox(b) and set_box(b, e), or as a whole argument to another Boxof parameter with the same element refinement. The argument for a Boxof parameter must be a literal box(e), such a parameter, or a top-level def of a box(e) used at only one refinement. Without these rules, a box could be written through one view and read through a stronger one.