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
Class invariants are supported in SpEx-JML at the method level, that is, invariants are translated into assertions that are checked at entry and exit of every method of the class. Note that this approach is not complete from the point of view of JML semantics, but it works fine as long as the objects in the system being analyzed are properly encapsulated. Work is being done for extending this approach of invariants checking.
- \old()
- constraint
- \forall and \exists
- \max, \min, \product and \sum
- \num_of
- Set Comprehension
- \fresh()
- \lockset
- \nonnullelements()
- \not_modified()
- \reach()
- maintaining
- decreasing
- diverges
- \signals
- \when