Annotations

LiquidJava extends Java with logical predicates and object protocol specifications. This section covers the different annotations for writing specifications.

@Refinement

Learn about how to use refinements to specify constraints on variables, fields, parameters, and return values.

@RefinementAlias

Learn how to reuse common refinement predicates with aliases to keep contracts shorter and easier to maintain.

@StateRefinement

Learn how to model protocol-oriented object states and valid method transitions.

@ExternalRefinementsFor

Learn how to refine external libraries that cannot be annotated directly.

@Ghost

Learn how to track logical state that helps express and verify richer object invariants.

@RefinementPredicate

Learn how to declare custom ghost functions and how they relate to ghosts and states.