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
Set Comprehension is a non-trivial operation, very complex operation, because it requires the evaluation of a set of expressions over potentially vast (even infinite) sets of elements. For example, a set comprehension expression that represents the even natural numbers, needs to be evaluated over the range of all natural numbers, in order to obtain the working set, which is very impractical. We have included support for a very limited version of set comprehension in which a set over which the resulting set is calculated, must be provided and it must be finite.
- \fresh()
- \lockset
- \nonnullelements()
- \not_modified()
- \reach()
- maintaining
- decreasing
- diverges
- \signals
- \when