Classification Model

In this page we present our 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, or strong constraint).

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.

For a nonconformance from precondition type, we proposed to check whether there is at least one parameter on precondition, in positive case the likely cause is suggested as Strong precondition; otherwise Weak postcondition is the suggestion. If there is a parameter or field in the precondition, the method can become a little restrictive – indicating a possible strong precondition; otherwise, the postcondition of one method used in the call to the method with precondition problem can be weak and allows return values that violates the precondition of the called method. In Figure 1 we present the heuristics used to classify a nonconformance from type precondition.

Figure 1. Heuristics for nonconformances from precondition type.

For a nonconformance from postcondition or evaluation types, whether there is the default precondition, or nothing, or whether there is at least one field modified on method body; in either case, the likely cause suggested is Weak precondition; otherwise Strong postcondition is the suggestion. If a method has the default precondition, it means that all clients are allowed and this fact can cause problems in the method exit – the method’s body can be unable to produce the desired result; so, weak precondition is proposed; furthermore, if there is a field modified on method body, and the precondition does not check anything about the field, weak precondition is also suggested. Finally, if neither of these cases occurs, the suggestion is strong postcondition – a postcondition so strong that possibly cannot be satisfied by the method’s body. Figure 2 shows the heuristics for nonconformances of postcondition and evaluation.

Figure 2. Heuristics for nonconformances from postcondition and evaluation types.

For a nonconformance from invariant type, whether there are some field from the class that is not initialized into the constructor, the likely cause proposed is Code error; otherwise, whether there is the default precondition, or nothing, or whether there is at least one field modified on method body; in either case, the likely cause suggested is Weak precondition; otherwise Strong invariant is the suggestion. If a class has some field not initialized, the default JML invariant is violated (invariant that determines all fields must be non-null); so, in this case we suggest as likely cause Code error (null-related) due to the fact that the code does not initialize all field from the class. Case all field are non-null and the method has the default precondition or nothing, it means that all clients are allowed and this fact can cause problems in the method exit (violating an invariant, for example) – the method’s body can be unable to produce the desired result; so, weak precondition is proposed; furthermore, if there is a field modified on method body, and the precondition does not check anything about the field, weak precondition is also suggested. Finally, if neither of these cases occurs, the suggestion is strong invariant – an invariant so strong that possibly cannot be satisfied by the method’s body. Figure 3 shows the heuristics for nonconformances of invariant.

Figure 3. Heuristics for nonconformances from invariant type.

Finally, for a nonconformance from constraint type, whether there are some field from the class that is not initialized into the constructor, the likely cause suggested is Code error; otherwise, whether there is the default precondition, or nothing, or whether there is at least one field modified on method body; in either case, the likely cause suggested is Weak precondition; otherwise Strong constraint is the suggestion. If a class has some field not initialized can be that a field manipulated into a constraint had null value, so, the likely cause proposed is Code error (null-related); due to the code does not initialize all fields from the class. Case all field are non-null and the method has the default precondition or nothing, it means that all clients are allowed and this fact can cause problems in the method exit (violating a constraint, for example) – the method’s body can be unable to produce the desired result; so, the suggested likely cause is weak precondition; furthermore, whether there is at least one field modified on method body, and the precondition does not check anything about the field, weak precondition is also suggested. Finally, if neither of these cases occurs, the suggestion is strong constraint – a constraint so strong that possibly cannot be satisfied by the method’s body. Figure 3 presents the heuristics for nonconformances of constraint.

Figure 4. Heuristics for nonconformances from constraint type.

These set of heuristics were implemented in JMLOK 2.0 tool.

Concerning to manual categorization of nonconformances, the following flow is used to perform the manual classification:

As an example for the category of Specification error, the class ArrayUtils (project JAccounting) has a method getMaxIntArrayIndex, with a postcondition violation that occurs after a creation of an integer array and one call to the method; in this case,with breadth 2 and depth 1. The nonconformance occurs in the body of getMaxIntArrayIndex with an invalid access to an empty array, causing an exception (ArrayIndexOutOfBoundsException). This problem possibly occurs due to the precondition that does not check the array size. Therefore, we have a nonconformance with type Postcondition, category Specification error and likely cause weak precondition.

The test case that reveals this nonconformance:

public void testGetMaxIntArrayIndex(){

  int[] var0 = new int[] { };

  int var1 = ArrayUtils.getMaxIntArrayIndex(var0);

}

For the category of Code error, we chose the nonconformance that we discovered in the project HealthCard: class Personal_Impl, constructor of the class. In this class, there is an invariant violation that occurs after the creation of an object of the class; so the measures depth and breadth receive value 1. The nonconformance occurs because the default constructor does not initializes the field birthplace, violating the default invariant of JML that requires all fields non-null. This problem possibly occurs by a code error: the lack of initialization of all fields of this class.

The test case that reveals this nonconformance:

public void testPersonal_Impl(){

  Personal_Impl var0 = new Personal_Impl();

}

For the category of Undefined, we chose the nonconformance that we discovered in the project Bomber: class Common, method div. In this class there is a precondition violation in the method distancePointToLine call that calls the methods sqr, sqrt and mul to construct a call to the method div; so the measure depth receives value 5 and the meausure breadth receives value 1. The nonconformance apparently occurs because the methods sqr, sqrt, and mul - called to create the parameters for the call to div - perform a shift of several bits (in some cases 10) and, in the test cases the generated values are a little bit small (usually amount of 10), the shift will be result in zero, violating the precondition of the div. How the Bomber domain is mobile games, maybe the generated values are large enough; therefore, we categorize this nonconformance as Undefined, because we cannot say if the problem stays in the code or in the specification.

The test case that reveals this nonconformance:

public void testCommon(){

  int var4 = Common.distancePointToLine(32, (-4), 10, 1);

}