SpEx-JML - JML Coverage
In this section we show those features of JML that are currently covered by the work on SpEx-JML. The list also includes features that are not currently totally supported, but are under implementation. A checkmark indicates that the feature is fully supported and implemented. An 'X' mark indicates that the feature is under study, but not yet fully implemented.
- assignable
- invariant
- \old()
- constraint
Class constraints are a form of invariant but that is usually checked only in the post-state of methods (to be technically correct, it is checked every time there is a transition from one visible state to another visible state, but usually the approximation just mentioned is enough). Because of its similarity with invariants it is implemented just the same way.
- \forall and \exists
- \max, \min, \product and \sum
- \num_of
- Set Comprehension
- \fresh()
- \lockset
- \nonnullelements()
- \not_modified()
- \reach()
- maintaining
- decreasing
- diverges
- \signals
- \when