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
This operator is mostly used in model programs. maintaining expresses a loop invariant in a model program's loop, however since model programs are not yet supported in SpEx-JML, this operator is not present in the current implementations. Although, there are plans for including it.
- decreasing
- diverges
- \signals
- \when