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
Checking for assignable clauses is fully implemented in SpEx-JML and the implementation is both sound and complete (with respect to the current environment). Given that Bogor maintains an explicit representation of the heap and thanks to the extremely flexible Bogor's API the implementation, surprisingly enough, is rather straightforward. At the beginning of every method that declares assignable memory, a set is created with all the memory points that can be assigned to. Because we have direct access to the heap, all problems related with aliasing are avoided. Then, all assignments are trapped and a check is performed to determine whether the assignment is valid.
All the assignable declarations are propagated to subsequent method calls. That way, if a method that declares assignable memory is called, a check is performed to assert that the memory declared assignable by the callee is a subset of that declared assignable by the caller.
Every time an assignable violation is found, a spec error is thrown specifying the type of error and the location where it happened.
- 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
- \when