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()
The \old clause is one of the features that show the advantage of using a model checker for verification, with respect to other approaches. Other dynamic checking systems check for \old. For example jmlc, Jass and jContractor, among others, store a copy of the data referenced by \old at method entry, to be used in the post-condition check at method exit. This approach is very simple, intuitive and very straightforward to implement.
However, there are several problems with this approach. To begin with, there is the restriction that the data referenced in \old must be Cloneable, otherwise, unless the data is primitive, there is no way to obtain the copy. Second, depending on the context and the property being checked, the portion of the heap that might need to be stored can be very big, for example, whole data structures. This can make the memory requirements very big, duplicating the memory needed by a method in the worst case. Finally, it might not be clear what portion of the heap would have to be copied, for example, if \old operates over a reference value, what must be copied? the reference value? all data reachable from the reference? some data reachable from the reference?
Another disadvantage of this approach is that the type of objects used in pre-condition statements must be immutable. This comes from the the method used to calculate the pre-state: simple copy. For example, suppose a reference type (a mutable type) is used in a pre-state and a copy is made. Then if the memory allocation pointed to by the reference is changed, then the pre-state value will be inconsistent with the actual value of the memory allocation upon entry of the method. The approach taken in SpEx-JML overcomes all this shortcomings.
Since Bogor maintains history information about the current trace being explored (needed for backtracking), this information is exploited using Bogor's backtracking API to reconstruct the pre-state. In this way, no copies need to be maintained about the pre-state values and no restriction is used about the kind of objects used in \old statements. Several challenges were encountered however, while implementing this operator, mostly because of state matching, in which case the model checker would backtrack before reaching the pre-state statement, missing some erroneous traces. For more information about this, check out the SpEx-JML paper "Checking Strong Specifications Using An Extensible Model Checking Framework" in the papers section.
- constraint
- \forall and \exists
- \max, \min, \product and \sum
- \num_of
- Set Comprehension
- \fresh()
- \lockset
- \nonnullelements()
- \not_modified()
- \reach()
- maintaining
- decreasing
- diverges
- \signals
- \when