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
- \signals
This operator is particularly easy to implement in Bogor because because of Bogor's built-in support for exception handling. Therefore, a signals clause is handled by catching, analyzing and then re-throwing a method's exceptions.
- \when