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
The current implementation of \forall and \exists is limited to well defined sets. For example, the set of all objects of a specific type currently existing in the heap or the set of all integers enclosed in a specific integers collection. There's no support for quantification over open sets (e.g. the set of all integers) or for set comprehension (a quantification defined by a set of inequalities). JML does support a limited version of set comprehension by static analysis and recognition of certain patterns. We are working towards giving that kind of limited support too.
- \max, \min, \product and \sum
- \num_of
- Set Comprehension
- \fresh()
- \lockset
- \nonnullelements()
- \not_modified()
- \reach()
- maintaining
- decreasing
- diverges
- \signals
- \when