In this page we present our enhanced classification model for nonconformances.
For
each nonconformance detected by the tool, we use a three-level model to
categorization: each nonconformance a category (specification error,
code error, or undefined), a type
(invariant, precondition, postcondition, constraint, or evaluation) - we
are considering only the visible behavior of the systems (a black-box
approach) -, and a likely cause (weak precondition, strong
precondition, weak postcondition, strong postcondition, strong
invariant, strong constraint, or code error).
The category is given by the manual analysis of the code
and specification by a JML expert (but not expert in the domain of the
projects) and has three possible values: Specification error - when the
error apparently occurs in the specification. Code error - when the
error apparently occurs in the source code. And Undefined - when is not
possible, considering a not expert in the application domain, determine
if the problem is into the specification or into the source code.
The
type corresponds to the part of JML that was violated: if was a
violation of Invariant, Precondition, Postcondition, History Constraint
or Evaluation - we are considering only the behavior visible of the
methods (an approach black-box). Each error may present several likely causes, which
cannot be deterministically diagnosed -- debugging can be aided,
however, by specific heuristics. Below, we present the set of likely causes for each type of nonconformance.
Precondition
- Code error inside method's body or inside the body of some intermediate called method, modifying the value used as parameter in the call to the method where the nonconformance occurred. The updates on the value used as parameter should be reviewed in order to respect the callee's precondition.
- Weak precondition of the caller method: there is no check on the value received and sent to the method where the nonconformance occurred. The caller precondition is so permissive and should be strengthened.
- Weak postcondition of some intermediate called method, allowing some unrestricted be used as parameter for the method where the nonconformance occurred. The intermediate methods' postconditions should be strengthened.
- Strong precondition of the method: there are so many clauses in the method's precondition that was not possible to satisfy it. The precondition is so restrictive that should be weaken.
Postcondition
- Code error inside method's body or inside some intermediate method (called by the method where the nonconformance occurred) modifying a value that breaks the postcondition of the method.
- Weak precondition of the method: the method's precondition is so permissive that the clauses in the postcondition cannot be satisfied by the method. The precondition should be strengthened.
- Weak postcondition of some method called into the body of the method where the nonconformance occurred: exists some method where its postcondition is so weak that allows the return of a value that breaks the postcondition of the caller method. The postcondition of the called method should be strengthened.
- Strong postcondition: there are several clauses in the method's postcondition that makes it very hard to be satisfied. The postcondition should be weaken.
Invariant
- Code error inside method's body or inside the body of some called method (methods called by the method where the nonconformance was detected) that changes a value or expression breaking some clause from the class invariant. The code should be reviewed in order to avoid the change and maintain the class invariant.
- Weak precondition of the current method (method where the nonconformance was detected) or of some called method allowing a value that breaks the class invariant before or after method execution. The precondition should be strengthened.
- Weak postcondition of the current method (method where the nonconformance was detected) or of some called method allowing a value that breaks the class invariant after method execution. The postcondition should be strengthened.
- Strong invariant of the class that have several clauses and cannot be satisfied by the current or some called method. The invariant should be weaken.
Constraint
- Code error inside method's body or inside the body of some called method (methods called by the method where the nonconformance was detected) that changes a value or expression breaking some clause from the constraint. The code should be reviewed in order to avoid the change and maintain the constraint.
- Weak precondition of the current method (method where the nonconformance was detected) or of some called method allowing a value that breaks the constraint before or after method execution. The precondition should be strengthened.
- Weak postcondition of the current method (method where the nonconformance was detected) or of some called method allowing a value that breaks the constraint after method execution. The postcondition should be strengthened.
- Strong constraint that have several clauses and cannot be satisfied by the current or some called method. The constraint should be weaken.
Evaluation
- Code error inside the current method's body or inside some called method, making the evaluation of some clause not possible (e.g. resulting in an runtime exception). The code should be reviewed in order to does not invalidate the evaluation of the expression
- Evaluation problem because the current expression was built in a wrong way.
|
|