Refinements in Classes
LiquidJava contains the mechanisms to model Object Type State.
Since class methods can have effects on the internal state of objects, each method can be annotated with the allowed state transitions using the @StateRefinement(from = "...", to = "...")
annotation. In this annotation, the from
argument represents the object states in which the method can be invoked, whereas the to
argument represents the state the object will have at the end of the method execution.
There are two possibilities of modelling object state:
State Sets: If a class has a defined set of states, it is possible to create multiple @StateSet
that include the allowed object states.
Ghost Properties: To model other properties (int or boolean) it is possible to create @Ghost
properties that work as uninterpreted functions.
In either case, whenever there is a need to refer to the previous state of the object, it is possible to use the old
keyword.