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