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
- \forall and \exists
- \max, \min, \product and \sum
- \num_of
- Set Comprehension
- \fresh()
- \lockset
- \nonnullelements()
- \not_modified()
- \reach()
- maintaining
- decreasing
- diverges
diverges is a very interesting operator that is used to express termination constraints. Specifically, it expresses a condition for which the method in question should not terminate normally. We are studying ways in which to implement this operator, but it is not very clear how to do it.
- \signals
- \when