JMLOK 2.0 Evaluation

This page presents the main results of the evaluation of our approach concerning to nonconformances detection and categorization.

Samples

In the set of example programs, we detect and categorize 18 nonconformances. Table 1 shows all nonconformances detected on Samples:

Table 1. Nonconformances on Samples. Column Experimental Unit shows the name of each experimental unit. Column Class shows class name that has one (or more) nonconformance(s). Column Method show the method name that has one (or more) nonconformance(s). Column Type shows the nonconformance's type. Column Category shows the nonconformance's category. Column Likely Cause shows the nonconformance's likely cause. Column Breadth (B) shows the value of the Breadth metric. And finally column Depth (D) shows the value of D metric.

Now we present the explanation about each nonconformance and a test case that reveals each nonconformance:

Package BoundedStack*:

*this package is an adaptation of the stacks package

Class BoundedStack

There is an invariant problem at the constructor of the BoundedStack class: the nonconformance occurs in the first call to the constructor of this class, so the measure B receives value 1; but the measure D receives 3 because the nonconformance is revealed in the super interface of the interface implemented by the BoundedStack class.

This nonconformance has as likely cause a problem into the specification: the absence of a precondition that restrict the range of values to maxSize parameter.

A test case that reveals this nonconformance:

public void testBoundedStack1(){

 BoundedStack var1 = new BoundedStack(0);

}

There is a postcondition problem at the constructor of the BoundedStack class: the nonconformance occurs in the first call to the constructor of this class, so the measure B receives value 1; and the measure D also receives value 1 because the nonconformance is revealed into the constructor - there is a try to creates an array with negative value.

This nonconformance has as likely cause a problem into the specification: the absence of a precondition that restrict the range of values to maxSize parameter.

A test case that reveals this nonconformance:

public void testBoundedStack2(){

 BoundedStack var1 = new BoundedStack((-1));

}

The two nonconformances present in this class are related to the same problem: the absence of a precondition that restrict the range of values to a field of the class.

Package dbc:

Class Polar

There is a postcondition problem at the angle method of the Polar class: the nonconformance occurs after the creation of one Polar object in the first call to angle method; so the measure B receives 2. The D measure receives 3 because the nonconformance is revealed in the specification of an interface implemented by the super class of Polar.

This nonconformance has as likely cause a problem at the specification of the method, a strong postcondition (with a tolerance value very small: 0.005 to compare two values) that uses the JMLDouble type of JML. Therefore the category of this nonconformance is specification error and the likely cause: strong postcondition.

A test case that reveals this nonconformance:

public void testAngle(){

 Polar var2 = new Polar(3.296908309475615d, 10.0d);

 double var3 = var2.angle();

}

There is a postcondition problem at the imaginaryPart method of the Polar class: the nonconformance occurs after the creation of one Polar object in the first call to imaginaryPart method; so the measure B receives 2. The D measure receives 3 because the nonconformance is revealed in the specification of an interface implemented by the super class of Polar.

This nonconformance has as likely cause a problem at the specification of the method, a strong postcondition (with a tolerance value very small: 0.005 to compare two values) that uses the JMLDouble type of JML. Therefore the category of this nonconformance is specification error and the likely cause: strong postcondition.

A test case that reveals this nonconformance:

public void testImaginaryPart(){

 Polar var2 = new Polar(0.0d, (-84.14709848078965d));

 double var3 = var2.imaginaryPart();

}

There is a postcondition problem at the magnitude method of the Polar class: the nonconformance occurs after the creation of one Polar object, a creation of one Rectangular object, in the fist call to the method mul (with the Polar object and passing the Rectangular object as parameter); so B receives 3. D receives 4 because the nonconformance occurs in the call of mul method from Polar that internally calls magnitude and the specification stays at into an interface implemented by the super class of Polar.

This nonconformance has as likely cause a problem at the specification of the method, a strong postcondition (with a tolerance value very small: 0.005 to compare two values) that uses the JMLDouble type of JML. Therefore the category of this nonconformance is specification error and the likely cause: strong postcondition.

A test case that reveals this nonconformance:

public void testMagnitude(){

 Polar var5 = new Polar(10.0d, 0.0d);

 Rectangular var7 = new Rectangular(10.0d);

 Complex var8 = var5.mul((Complex)var7);

}

There is a postcondition problem at the realPart method of the Polar class: the nonconformance occurs after the creation of two Polar objects, in the fist call to the add method (with one Polar object and passing the other as parameter); so B receives 3. D receives 4 because the nonconformance occurs in the call of add method from Polar that internally calls realPart and the specification stays at into an interface implemented by the super class of Polar.

This nonconformance has as likely cause a problem at the specification of the method, a strong postcondition (with a tolerance value very small: 0.005 to compare two values) that uses the JMLDouble type of JML. Therefore the category of this nonconformance is specification error and the likely cause: strong postcondition.

A test case that reveals this nonconformance:

public void testRealPart(){

 Polar var2 = new Polar(100.0d, (-1.0d));

 Polar var5 = new Polar(10.0d, 0.0d);

 Complex var8 = var2.add((Complex)var5);

}

Class Rectangular

There is a postcondition problem at the angle method of the Rectangular class: the nonconformance occurs after the creation of one Rectangular object in the first call to angle method; so the measure B receives 2. The D measure receives 3 because the nonconformance is revealed in the specification of an interface implemented by the super class of Rectangular.

This nonconformance has as likely cause a problem at the specification of the method, a strong postcondition (with a tolerance value very small: 0.005 to compare two values) that uses the JMLDouble type of JML. Therefore the category of this nonconformance is specification error and the likely cause: strong postcondition.

A test case that reveals this nonconformance:

public void testAngle(){

 Rectangular var2 = new Rectangular(3.141592653589793d, 10.0d);

 double var3 = var2.angle();

}

There is a postcondition problem at the imaginaryPart method of the Rectangular class: the nonconformance occurs after the creation of one Rectangular object in the first call to imaginaryPart method; so the measure B receives 2. The D measure receives 3 because the nonconformance is revealed in the specification of an interface implemented by the super class of Rectangular.

This nonconformance has as likely cause a problem at the specification of the method, a strong postcondition (with a tolerance value very small: 0.005 to compare two values) that uses the JMLDouble type of JML. Therefore the category of this nonconformance is specification error and the likely cause: strong postcondition.

A test case that reveals this nonconformance:

public void testImaginaryPart(){

 Rectangular var1 = new Rectangular((-1.0d));

 double var2 = var1.imaginaryPart();

}

There is a postcondition problem at the magnitude method of the Rectangular class: the nonconformance occurs after the creation of one Rectangular object in the first call to magnitude method; so the measure B receives 2. The D measure receives 3 because the nonconformance is revealed in the specification of an interface implemented by the super class of Rectangular.

This nonconformance has as likely cause a problem at the specification of the method, a strong postcondition (with a tolerance value very small: 0.005 to compare two values) that uses the JMLDouble type of JML. Therefore the category of this nonconformance is specification error and the likely cause: strong postcondition.

A test case that reveals this nonconformance:

public void testMagnitude{

 Rectangular var2 = new Rectangular((-1.0d), 3.141592653589793d);

 double var3 = var2.magnitude();

}

There is a postcondition problem at the realPart method of the Rectangular class: the nonconformance occurs after the creation of one Rectangular object in the first call to realPart method; so the measure B receives 2. The D measure receives 3 because the nonconformance is revealed in the specification of an interface implemented by the super class of Rectangular.

This nonconformance has as likely cause a problem at the specification of the method, a strong postcondition (with a tolerance value very small: 0.005 to compare two values) that uses the JMLDouble type of JML. Therefore the category of this nonconformance is specification error and the likely cause: strong postcondition.

A test case that reveals this nonconformance:

public void testRealPart(){

 Rectangular var6 = new Rectangular((-1.0d));

 double var7 = var6.realPart();

}

All the eight (8) nonconformances discovered in this package apparently have the same likely cause: strong postcondition (a very small value to compare two values using a method of a JML type - JMLDouble).

Package list

Class Link

There is an evaluation problem at the method getEntry of Link class: the nonconformance occurs after the creation of two objects (one OneWayNode and one Link) in the first call to getEntry method. So B measure receives 3, and D also receives 3 because the nonconformance is revealed into the specification of the method in the Link.jml-refined file, that is refined by Link.jml and that is refined by the Link class.

This nonconformance has as likely cause a problem at the specification of getEntry method; since in the specification of the method there is an instruction declaring that the method and the parameter used in the ensures clause can be null, but there is an instruction in the ensures that try to access a method of the object (that can be null) throwinf a NullPointerException and causing this nonconformance.

A test case that reveals this nonconformance:

public void testLink(){

 OneWayNode var1 = new OneWayNode((java.lang.Object)0.0f);

 Link var2 = var1.getNextLink();

 Object var3 = var2.getEntry();

}

Class E_OneWayList (list2)

There is a postcondition problem at the equals method of E_OneWayList (package list2) class: the nonconformance occurs after the creation of one object of the class in the first call to equals method. So B measure receives 2; D measure receives 3 because the nonconformance is revealed into the specification of the method in the E_OneWayList.jml-refined file, that is refined by E_OneWayList.jml and that is refined by the E_OneWayList class.

In this case, we cannot determine if the problem is on the code or on the specification, so we categorize the nonconformance as undefined; since the researcher is not expert in the domain of this experimental unit. Considering only our set of heuristics we would point as likely cause (in our implementation) a strong postcondition of the equals method.

A test case that reveals this nonconformance:

public void testE_OneWayList(){

 E_OneWayList v0 = new E_OneWayList();

 assertTrue("Contract failed: v0.equals(v0)", v0.equals(v0));

}

Class E_OneWayList (list3)

There is a postcondition problem at the equals method of E_OneWayList (package list3) class: the nonconformance occurs after the creation of one object of the TwoWayList class (a subclass of E_OneWayList) in the first call to equals method. So B measure receives 2; D measure receives 4 because the nonconformance is revealed into the specification of the method in the E_OneWayList.jml-refined file, that is refined by E_OneWayList.jml and that is refined by the E_OneWayList class and this class is inherited by TwoWayList.

In this case, we too cannot determine if the problem is on the code or on the specification, so we categorize the nonconformance as undefined; since the researcher is not expert in the domain of this experimental unit. Considering only our set of heuristics we would point as likely cause (in our implementation) a strong postcondition of the equals method.

A test case that reveals this nonconformance:

public void testE_OneWayList(){

 TwoWayList v0 = new TwoWayList();

 assertTrue("Contract failed: v0.equals(v0)", v0.equals(v0));

}

Class TwoWayIterator (list3)

There is a postcondition problem at the isDone method of the class TwoWayIterator (package list3): the nonconformance occurs after the creation of two objects (one TwoWayNode and one TwoWayIterator), two calls to last method and one call to isDOne method. So B receives 5, and D receives 3 because the nonconformance is revealed in the specification present in the super interface of the interface implemented by the TwoWayIterator class.

In this case, we too cannot determine if the problem is on the code or on the specification, so we categorize the nonconformance as undefined; since the researcher is not expert in the domain of this experimental unit. Considering only our set of heuristics we would point as likely cause (in our implementation) a weak precondition of the isDone method (because there is a requires unchanged where unchanged is equals true).

A test case that reveals this nonconformance:

public void testIsDone(){

 TwoWayNode var0 = new TwoWayNode();

 TwoWayIterator var2 = new TwoWayIterator(var0);

 var2.last();

 var2.last();

 boolean var5 = var2.isDone();

}

There is a postcondition problem at the method next of the class TwoWayIterator (package list3): the nonconformance occurs after the creation of two objects (one TwoWayNode and one TwoWayIterator), one call to method last, in the first call to method next. B measure receives 4, and D receives 3 because the nonconformance is revealed in the specification present in the super interface of the interface implemented by the TwoWayIterator class.

In this case, we too cannot determine if the problem is on the code or on the specification, so we categorize the nonconformance as undefined; since the researcher is not expert in the domain of this experimental unit. Considering only our set of heuristics we would point as likely cause (in our implementation) a strong postcondition of the method next.

A test case that reveals this nonconformance:

public void testNext(){

 TwoWayNode var0 = new TwoWayNode();

 TwoWayIterator var2 = new TwoWayIterator(var0);

 var2.last();

 var2.next();

}

Since we do not have an expert in the domain of this package the majority (4 of 5) of the nonconformances discovered got an undefined as category. Considering that the code is right and using our set of heuristics we can suggest a likely cause for each one (as we pointed).

Package misc

Class SingleSolution

There is a postcondition problem at the method limit in the class SingleSolution: the nonconformance occurs after one creation of a EqualsN object (subclass of SingleSolution), in the first call to method limit. B receives 2, and D receives 3 because the nonconformance is revealed in the specification of the method in the LinearSearch class, super class of SingleSolution, super class of EqualsN.

This nonconformance has as likely cause the absence of a precondition in the specification of the constructor of the classes EqualsN or SingleSolution that restrict the range of valid values to parameter n (this parameter is used in the postcondition of limit method). So we assign specification error as category and weak precondition as likely cause for this nonconformance.

A test case that reveals this nonconformance:

public void testLimit(){

 EqualsN var1 = new EqualsN((-214));

 int var2 = var1.limit();

}

Package stacks:

Class BoundedStack

There is an invariant problem at the constructor of the BoundedStack class: the nonconformance occurs in the first call to the constructor of this class, so the measure B receives value 1; but the measure D receives 3 because the nonconformance is revealed in the super interface of the interface implemented by the BoundedStack class.

This nonconformance has as likely cause a problem into the specification: the absence of a precondition that restrict the range of values to maxSize parameter.

A test case that reveals this nonconformance:

public void testBoundedStack1(){

 BoundedStack var1 = new BoundedStack(0);

}

There is a postcondition problem at the constructor of the BoundedStack class: the nonconformance occurs in the first call to the constructor of this class, so the measure B receives value 1; and the measure D also receives value 1 because the nonconformance is revealed into the constructor - there is a try to creates an array with negative value.

This nonconformance has as likely cause a problem into the specification: the absence of a precondition that restrict the range of values to maxSize parameter.

A test case that reveals this nonconformance:

public void testBoundedStack1(){

 BoundedStack var1 = new BoundedStack((-1));

}

The two nonconformances present in this class are related to the same problem: the absence of a precondition that restrict the range of values to a field of the class.

Real programs

In the set of real programs, we detect 66 nonconformances; how is shown in Table 2:

Table 2. Nonconformances on Real Programs. Nonconformances on Samples. Column Experimental Unit shows the name of each experimental unit. Column Class shows class name that has one (or more) nonconformance(s). Column Method show the method name that has one (or more) nonconformance(s). Column Type shows the nonconformance's type. Column Category shows the nonconformance's category. Column Likely Cause shows the nonconformance's likely cause. Column Breadth (B) shows the value of the Breadth metric. And finally column Depth (D) shows the value of D metric.

Now we present the explanation about each nonconformance and a test case that reveals each nonconformance:

• On Bomber:

Class Building

There is an invariant problem at the class Building: the nonconformance occurs after the creation of one object of the class Building, using the default constructor. So B measure is equals 1, and D is equals 1 because the nonconformance occurs directly in the class Building.

This nonconformance is caused by the not initialization of some attributes of this class in the default constructor, violating the invariant default of JML; so this nonconformance has as category a code error - the not initialization of some attributes of the class.

A test case that reveals this nonconformance:

public void testBuilding(){

 Building var0 = new Building();

}

Class Common

There is a precondition problem at the method div in the class Common: the nonconformance occurs in the call to method distancePointToLine that creates a variable in its body that receives as result the square root of the sum of square of two values (vx and vy) and returns a call to method div with the variable and two call to method mul as parameter. So B is equals 1 and D is equals 5 because the nonconformance is revealed in the method div.

This nonconformance apparently relates to the methods sqr, sqrt e mul performs a shift of several bits (10 in some cases) and since the values generated in the test case are small (10 and 1 for vx and vy, respectively) the shift will returns 0, violating the precondition of the method div. Once the domain of the Bomber project is games for mobile, can be that the shift not result in 0; so we categorize this nonconformance as undefined because we are not expert in the domain of the project. Considering only our set of heuristics, we would suggest as likely cause the strong precondition of the method div.

A test case that reveals this nonconformance:

public void testCommon(){

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

}

Class Explosion

There is an invariant problem in the class Explosion: the nonoconformance occurs after the creation of an array of integers (that will be used as parameter for the creation of one object Explosion) in the creation of an object Explosion. So B is equals 2 and D is equals 2 because the constructor of this class calls the method init and in the entry of this method some attributes of this class are null.

This nonconformance occurs because some attributes of the class are no initialized in the constructor, violating the default invariant of JML; so the category of the nonconformance is code error - the not initialization of all attributes directly in the constructor.

A test case that reveals this nonconformance:

public void testExplosion(){

 int[] var1 = new int[] { 1};

 Explosion var11 = new Explosion(var1, 100, 0, (byte)10, 100, 1, 10, 1, (byte)(-1), (byte)1);

}

Class FlakSmoke

There is a postcondition problem at the method getBoundingBox in the class FlakSmoke: the nonoconformance occurs after the creation of one object FlakSmoke in the first call to method getBoundingBox. So B is equals 2 and D is equals 1 because the nonconformance is revealed directly in the method getBoundingBox.

This nonconformance occurs because the method getBoundingBox returns null violating the default postcondition (ensures true); so the category of this nonconformance is code error - maybe the programmer have forgotten of implement this method.

A test case that reveals this nonconformance:

public void testFlakSmoke(){

 FlakSmoke var3 = new FlakSmoke(2, (-12288), 92160);

 Object var10 = var3.getBoundingBox();

}

The majority of the nonconformances in the Bomber project (3 of 4) are related to code errors - not initialization of attributes, null return of a method. These problems can be related to the fact of some current JML patterns (for invariants or postconditions) were not patterns when Bomber was developed; or can indicate a bad use of JML specifications.

• On Healthcard:

Class Allergies_Impl

Method getAllergyDesignation

There is a postcondition problem in the method getAllergyDesignation from the class Allergies_Impl: the nonconformance occurs after the creation of one object Allergies_Impl in the first call to method getAllergyDesignation. So B is equals 2 and D is equals 2 because there is a call to a method in the return of getAllergyDesignation that returns a NullPointerException.

This nonconformance occurs because in the call to default constructor only 3 values are assigned to the created array (whose size is 50), so if the test case try to access some element greater than 2 (since the first index is 0) it enters into the specification of the exceptional behaviour of the method and the call to method (getDesignation from Allergy_Impl) results in an exception NullPointerException that is not specified signals clause of the method (is specified that only UserException can be threw). In this context we chose as likely cause the strong postcondition of the method.

A test case that reveals this nonconformance:

public void testGetAllergyDesignation(){

 Allergies_Impl var0 = new Allergies_Impl();

 byte[] var4 = var0.getAllergyDesignation((short)10);

}

Method removeAllergy

There is a postcondition problem in the method remveAllergy from the class Allergies_Impl: the nonconformance occurs after the creation of one object Allergies_Impl in the first call to the method removeAllergy. So B is equals 2 and D is equals 2 because the nonconformance is revealed at the method specification in the interface implemented by Allergies_Impl.

This nonconformance occurs by the try to remove an array element whose value is null, entering in the exceptional behaviour of the method. So the likely cause for this nonconformance is strong postcondition of the method.

A test case that reveals this nonconformance:

public void testRemoveAllergy(){

 Allergies_Impl var0 = new Allergies_Impl();

 var0.removeAllergy((short)3);

}

Method setAllergyDate

There is a postcondition problem in the method setAllergyDate from the class Allergies_Impl: the nonconformance occurs after the creation of one Allergies_Impl object, one object Medicine_Impl, one call to method getDate (from the class Medicine_Impl), and one call to the method cleanField (method estático from CardUtil), in the first call to the method setAllergyDate. So B is equals 5 and D is equals 4 because the object used in the call to the method is created in the call to method getDate, modified by cleanField and then used in the call to setAllergyDate - that violates the specification in the interface implemented by Allergies_Impl.

This nonconformance occurs because the call to the default constructor from the class only assigns 3 values to created array (whose size is 50), so if the test case try to access some position greater than 2 it enters into the specification of the exceptional behaviour of the method and the call to the method setIdentificationDate from Allergy_Impl returns a NullPointerException a kind of exception that is not specified in the signals clause of the method (it is specified only exceptions UserException). So the likely cause for this nonconformance is strong postcondition.

A test case that reveals this nonconformance:

public void testSetAllergyDate(){

 Allergies_Impl var0 = new Allergies_Impl();

 Medicine_Impl var24 = new Medicine_Impl((byte)0, (byte)10, (byte)1, (byte)0);

 byte[] var26 = var24.getDate();

 CardUtil.cleanField(var26);

 var0.setAllergyDate((short)3, var26);

}

Method setAllergyDesignation

There is a postcondition problem in the method setAllergyDesignation from the class Allergies_Impl: the nonconformance occurs after the creation of one array of bytes, two objects from the class, one call to the method getAllergyDate of the second object, one call to the method arrayCopy (from CardUtil) in the first call to the method setAllergyDesignation. So B is equals 6 and D is equals 4 because the nonconformance occurs after the call to the method getAllergyDate followed for one call to arrayCopy and the call to setAllergyDesignation - that violates the specification in the interface implemented by Allergies_Impl.

This nonconformance occurs because the call to the default constructor from the class only assigns 3 values to created array (whose size is 50), so if the test case try to access some position greater than 2 it enters into the specification of the exceptional behaviour of the method setDesignation from Allergy_Impl returns a NullPointerException that is not specified in the signals clause of the method (it is specified only exceptions UserException). So the likely cause for this nonconformance is strong postcondition.

A test case that reveals this nonconformance:

public void testSetAllergyDesignation(){

 byte[] var13 = new byte[] { (byte)(-1), (byte)1, (byte)10};

 Allergies_Impl var0 = new Allergies_Impl();

 Allergies_Impl var19 = new Allergies_Impl();

 byte[] var21 = var19.getAllergyDate((short)0);

 CardUtil.arrayCopy(var13, var21);

 var0.setAllergyDesignation((short)10, var21);

}

Class Appointments_Impl

There is an invariant problem in the class Appointments_Impl: the nonconformance occurs after the creation of one object Treatments_Impl. So B is equals 1 and D is equals 5 because in the creation of one object Treatments_Impl there is a call to constructor of Diagnostics_Impl that calls the constructor Appointments_Impl - which violates one invariant of the interface Appointments that inherit from the interface Common.

This nonconformance occurs because of a problem into the code of Appointments_Impl constructor that assign one value of date and time of 2009 year for the first element of the Appointment_Impl array, violating one invariant from Appointments that specifies if the difference between the current date and the dates into the array elements is less than 24 hours, and once the value inserted is from 2009, the invariant is violated. This problem was known by the programmer, there is a comment into the constructor saying that is needed to update the values of the first element. This problem only has occurred because the HealthCard developer assigned values to the first element of the array. Analysing from the point view of a not expert in the domain of HealthCard the specification seems consistent with the domain but the code of assignment of values to the first element of the Appointments array makes that the constructor has a fix value to be compared with the current date and time, violating the invariant from the class. So the category of this nonconformance is code error.

A test case that reveals this nonconformance:

public void testAppointments_Impl(){

 Treatments_Impl var0 = new Treatments_Impl();

}

Class CardException

There is an invariant problem in the class CardException: the nonconformance occurs in the call to the static method throwIt from UserException (subclass of CardException). So B is equals 1 and D is equals 2 because the nonconformance occurs by the fact of the attribute from the class be null when the method is called.

This nonconformance occurs by the violation of the default invariant of JML. So the category of this nonconformance is code error - the not initialization of some attribute from the class.

A test case that reveals this nonconformance:

public void testCardException(){

 UserException.throwIt((short)514);

}

Class CardRuntimeException

There is an invariant problem in the class CardRuntimeException: the nonconformance occurs in the call to the static method throwIt from TransactionException (subclass of CardRuntimeException). So B is equals 1 and D is equals 2 because the nonconformance occurs by the fact of the attribute from the class be null when the method is called.

This nonconformance occurs by the violation of the default invariant of JML. So the category of this nonconformance is code error - the not initialization of some attribute from the class.

A test case that reveals this nonconformance:

public void testCardRuntimeException(){

 TransactionException.throwIt((short)1);

}

Interface Common

Method getDate

There is a constraint problem in the method getDate from the interface Common - revealed in the class Appointment_Impl: the nonconformance is revealed after four array creations to be used in the creation of the Appointment_Impl object, in the first call to the method getDate. So B is equals 6 and D is equals 3 because the nonconformance occurs in the specification of the interface Common inherited by the interface Appointment, implemented in the class Appointment_Impl.

This nonconformance apparently occurs because there are not check of the parameters received in the constructor of Appointment_Impl violating the constraint about the date that can be manipulated by the system. So the likely cause is weak precondition.

A test case that reveals this nonconformance:

public void testGetDate(){

 byte[] var2 = new byte[] { (byte)10};

 byte[] var5 = new byte[] { (byte)0, (byte)(-1)};

 byte[] var9 = new byte[] { (byte)(-1), (byte)1, (byte)10};

 byte[] var12 = new byte[] { (byte)1, (byte)100};

 Appointment_Impl var14 = new Appointment_Impl((byte)10, var2, var5, var9, var12, (byte)0);

 byte[] var15 = var14.getDate();

}

Method getHour

There is a constraint problem in the method getHour from the interface Common - revealed in the class Appointment_Impl: the nonconformance is revealed after four array creations to be used in the creation of the Appointment_Impl object, in the first call to the method getHour. So B is equals 6 and D is equals 3 because the nonconformance occurs in the specification of the interface Common inherited by the interface Appointment, implemented in the class Appointment_Impl.

This nonconformance apparently occurs because there are not check of the parameters received in the constructor of Appointment_Impl violating the constraint about the date that can be manipulated by the system. So the likely cause is weak precondition.

A test case that reveals this nonconformance:

public void testGetHour(){

 byte[] var12 = new byte[] { (byte)10};

 byte[] var15 = new byte[] { (byte)0, (byte)(-1)};

 byte[] var19 = new byte[] { (byte)(-1), (byte)1, (byte)10};

 byte[] var22 = new byte[] { (byte)1, (byte)100};

 Appointment_Impl var24 = new Appointment_Impl((byte)10, var12, var15, var19, var22, (byte)0);

 byte[] var25 = var24.getHour();

}

Method getType

There is a constraint problem in the method getType from the interface Common - revealed in the class Appointment_Impl: the nonconformance is revealed after four array creations to be used in the creation of the Appointment_Impl object, in the first call to the method getType. So B is equals 6 and D is equals 3 because the nonconformance occurs in the specification of the interface Common inherited by the interface Appointment, implemented in the class Appointment_Impl.

This nonconformance apparently occurs because there are not check of the parameters received in the constructor of Appointment_Impl violating the constraint about the date that can be manipulated by the system. So the likely cause is weak precondition.

A test case that reveals this nonconformance:

public void testGetType(){

 byte[] var2 = new byte[] { (byte)10};

 byte[] var5 = new byte[] { (byte)0, (byte)(-1)};

 byte[] var9 = new byte[] { (byte)(-1), (byte)1, (byte)10};

 byte[] var12 = new byte[] { (byte)1, (byte)100};

 Appointment_Impl var14 = new Appointment_Impl((byte)10, var2, var5, var9, var12, (byte)0);

 byte var15 = var14.getType();

}

Method getVaccinationDate

There is a constraint problem in the method getVaccinationDate from the interface Common - revealed in the class Vaccine_Impl: the nonconformance is revealed after two array creations to be used in the creation of the Vaccine_Impl object, in the first call to the method getVaccinationDate. So B is equals 4 and D is equals 3 because the nonconformance occurs in the specification of the interface Common inherited by the interface Vaccine, implemented in the class Vaccine_Impl.

This nonconformance apparently occurs because there are not check of the parameters received in the constructor of Vaccine_Impl violating the constraint about the date that can be manipulated by the system. So the likely cause is weak precondition.

A test case that reveals this nonconformance:

public void testVaccinationDate(){

 byte[] var2 = new byte[] { (byte)0, (byte)0};

 byte[] var4 = new byte[] { (byte)1};

 Vaccine_Impl var5 = new Vaccine_Impl(var2, var4);

 byte[] var6 = var5.getVaccinationDate();

}

Method setDate

There is a constraint problem in the method setDate from the interface Common - revealed in the class Medicine_Impl: the nonconformance is revealed after the creation of one object Medicine_Impl, one modification in the object (setTreatmentID), one array of bytes creation, one Allergies_Impl creation, other creation of arrays of bytes to receive the result of the method getAllergyDate (of the object Allergies_Impl), the mutation of the array of bytes - exchange its value by the value of the array early created and one call to the method setDate from the class Medicine_Impl. So B is equals 7 and D is equals 3 because the nonconformance occurs in the specification of the interface Common inherited by the interface Medicine, implemented in the class Medicine_Impl.

This nonconformance occurs apparently by a strong constraint once the precondition of the method checks somethings in the array (check null and if the size of the array is equals to the size of one date). So the likely cause is strong constraint.

A test case that reveals this nonconformance:

public void testSetDate(){

 Medicine_Impl var4 = new Medicine_Impl((byte)0, (byte)10, (byte)1, (byte)0);

 var4.setTreatmentID((byte)0);

 byte[] var17 = new byte[] { (byte)(-1), (byte)1, (byte)10};

 Allergies_Impl var23 = new Allergies_Impl();

 byte[] var25 = var23.getAllergyDate((short)0);

 CardUtil.arrayCopy(var17, var25);

 var4.setDate(var25);

}

Method toString

There is a constraint problem in the method toString from the interface Common - revealed in the class Appointment_Impl: the nonconformance is revealed after four array creations to be used in the creation of the Appointment_Impl object, in the first call to the method toString. So B is equals 6 and D is equals 3 because the nonconformance occurs in the specification of the interface Common inherited by the interface Appointment, implemented in the class Appointment_Impl.

This nonconformance apparently occurs because there are not check of the parameters received in the constructor of Appointment_Impl violating the constraint about the date that can be manipulated by the system. So the likely cause is weak precondition.

A test case that reveals this nonconformance:

public void testToString(){

 byte[] var2 = new byte[] { (byte)10};

 byte[] var5 = new byte[] { (byte)0, (byte)(-1)};

 byte[] var9 = new byte[] { (byte)(-1), (byte)1, (byte)10};

 byte[] var12 = new byte[] { (byte)1, (byte)100};

 Appointment_Impl var14 = new Appointment_Impl((byte)10, var2, var5, var9, var12, (byte)0);

 String var15 = var14.toString();

}

The nonconformances revealed in the methods getDate, getHour, getType, getVaccinationDate, and toString are related to the same constraint - that defines the range of valid values to date.

Class Diagnostic_Impl

Method getDescription

There is a postcondition problem in the method getDescription from the class Diagnostic_Impl: the nonconformance occurs after the creation of one object Diagnostic_Impl, one modification of the object (method setAppointmentID) in the first call to the method getDescription. So B is equals 3 and D is equals 2 because the nonconformance occurs in the call to the method arraycopy from System into the method getDescription.

This nonconformance is apparently caused by an error in the code of the method because in this method there is a call to the method arraycopy from System using as source array one with size 160 and as target array one with size 80. Once in our test case there is a try to copy from the position 1, 100 positions from the source array to the target array, there is a launching of one ArrayIndexOutOfBoundsException causing a problem in the postcondition of the method. So the category of this nonconformance is code error.

A test case that reveals this nonconformance:

public void testGetDescription(){

 Diagnostic_Impl var2 = new Diagnostic_Impl((byte)10, (byte)1);

 var2.setAppointmentID((byte)0);

 byte[] var7 = var2.getDescription((short)1, (short)100);

}

Constructor

There is an invariant error in the constructor of the class: the nonconformance occurs after the creation of one Diagnostic_Impl object. So B is equals 1 and D is equals 2 because the nonconformance is revealed in the method specification into the interface Diagnostic implemented by the class: the invariant that determines the range of values to appointmentID.

This nonconformance occurs by the absence of one precondition in the constructor of the class that checks the values received as parameter. So the likely cause is weak precondition.

A test case that reveals this nonconformance:

public void testDiagnostic(){

 Diagnostic_Impl var2 = new Diagnostic_Impl((byte)(-1), (byte)10);

}

Method setAppointmentID

There is an invariant error in the method setAppointmentID from the class Diagnostic_Impl: the nonconformance occurs after the creation of one object Diagnostic_Impl in the first call to the method setAppointmentID. So B is equals 2 and D is equals 2 because the nonconformance is revealed in the method specification into the interface Diagnostic implemented by the class: the invariant that determines the range of values to appointmentID.

This nonconformance occurs by the absence of one precondition in the method that checks if the values received as parameter are in the valid range ([0; 127]). So the likely cause is weak precondition.

A test case that reveals this nonconformance:

public void testSetAppointmentID(){

 Diagnostic_Impl var2 = new Diagnostic_Impl((byte)10, (byte)1);

 var2.setAppointmentID((byte)(-1));

}

Method setDescription

There is a postcondition problem in the method setDescription from the class Diagnostic_Impl: the nonconformance occurs after the creation of one object Diagnostic_Impl, one update of the object (with the method setAppointmentID), the creation of one array (that will be used as parameter of the method setDescription) and one call to the method setDescription. So B is equals 4 and D is equals 2 because the nonconformance is revealed in the method specification into the interface Diagnostic implemented by the class.

This nonconformance occurs by the absence of one precondition that checks if the second parameter of the method (the quantity of positions from the array to be copied) is less than or equals to the array size passed as first parameter, allowing a try to copy more elements than the array passed as parameter has, causing an ArrayIndexOutOfBoundsException. So the likely cause is weak precondition.

A test case that reveals this nonconformance:

public void testSetDescription(){

 Diagnostic_Impl var2 = new Diagnostic_Impl((byte)10, (byte)1);

 var2.setAppointmentID((byte)0);

 byte[] var15 = new byte[] { (byte)(-1), (byte)1, (byte)10};

 var2.setDescription(var15, (short)10, (short)0, true);

}

Class Medicine_Impl

There is an invariant problem in the class Medicine_Impl: the nonconformance occurs after the creation of one object Medicine_Impl. So B is equals 1 and D is equals 2 because there is a violation of one invariant specified in the interface Medicine implemented by the class: the invariant that determines the range of valid values for the diagnostic id.

This nonconformance occurs by the absence of one precondition in the constructor of the class that restricts the range of valid values for the parameters of the constructor. So the likely cause is weak precondition.

A test case that reveals this nonconformance:

public void testMedicine_Impl(){

 Medicine_Impl var4 = new Medicine_Impl((byte)100, (byte)(-1), (byte)(-1), (byte)(-1));

}

Class Personal_Impl

There is an invariant problem in the class Personal_Impl: the nonconformance occurs after the creation of one Personal_Impl object. So B is equals 1 and D is equals 1 because the invariant default is violated directly in the constructor.

This nonconformance occurs because the attribute birthPlace is not initialized in the default constructor of this class. So the category of this nonconformance is code error - the not initialization of all attributes from the class.

A test case that reveals this nonconformance:

public void testPersonal_Impl(){

 Personal_Impl var0 = new Personal_Impl();

}

Class Treatment_Impl

Method getMedicalRecommendation

There is a postcondition problem in the method getMedicalRecommendation from the class Treatment_Impl: the nonconformance occurs after the creation of one object Treatment_Impl in the first call to the method getMedicalRecommendation. So B is equals 2 and D is equals 2 because there is a try to copy elements from a source array to a target array using the method arraycopy from System with size less than 0 causing an ArrayIndexOutOfBoundsException.

This nonconformance occurs by the absence of one precondition that checks if the parameters are in a valid range. So the likely cause of this nonconformance is weak precondition.

A test case that reveals this nonconformance:

public void testGetMedicalRecommendation(){

 Treatment_Impl v3 = new Treatment_Impl((byte)1, (byte)10, (byte)10);

 byte[] v = v3.getMedicalRecommendation((short)100, (short)(-1));

}

Constructor

There is an invariant problem in the constructor from the class: the nonconformance occurs after the creation of one object Treatment_Impl. So B is equals 1 and D is equals 2 because there is a violation of one invariant specified into the interface Treatment implemented by the class: the invariant that specifies the range of valid values to the diagnostic id ([0, 127]).

This nonconformance occurs by the absence of one precondition in the constructor from the class that checks the values received as parameter. So the likely cause of this nonconformance is weak precondition.

A test case that reveals this nonconformance:

public void testTreatment_Impl(){

 Treatment_Impl v = new Treatment_Impl((byte)0, (byte)(-1), (byte)0);

}

Method setAppointmentID

There is an invariant problem in the method setAppointmentID from the class Treatment_Impl: the nonconformance occurs after the creation of one object Treatment_Impl in the first call to the method setAppointmentID. So B is equals 2 and D is equals 2 because there is a violation of one invariant specified into the interface Treatment implemented by the class: the invariant that specifies the range of valid values to the appointment id ([0; 127]).

This nonconformance occurs by the absence of one precondition in the method that checks the values received as parameter. So the likely cause of this nonconformance is weak precondition.

A test case that reveals this nonconformance:

public void testSetAppointmentID(){

 Treatment_Impl var3 = new Treatment_Impl((byte)0, (byte)100, (byte)0);

 var3.setAppointmentID((byte)(-1));

}

Method setDiagnosticID

There is an invariant problem in the method setDiagnosticID from the class Treatment_Impl: the nonconformance occurs after the creation of one object Treatment_Impl in the first call to the method setDiagnosticID. So B is equals 2 and D is equals 2 because there is a violation of one invariant specified into the interface Treatment implemented by the class: the invariant that specifies the range of valid values to the diagnostic id ([0, 127]).

This nonconformance occurs by the absence of one precondition in the method that checks the values received as parameter. So the likely cause of this nonconformance is weak precondition.

A test case that reveals this nonconformance:

public void testSetDiagnosticID(){

 Treatment_Impl var3 = new Treatment_Impl((byte)1, (byte)0, (byte)0);

 var3.setDiagnosticID((byte)(-1));

}

Method setMedicalRecomendation

There is a postcondition problem in the method setMedicalRecomendation from Treatment_Impl: the nonconformance occurs after the creation of one object Treatment_Impl, a creation of one bytes array (that will be used in the call to the method setMedicalRecommendation) in the first call to the method setMedicalRecomendation. So B is equals 3 and D is equals 2 because there is a try to copy more elements than the array size violating the normal specification of the method in the interface implemented by the class.

This nonconformance occurs by the absence of one precondition in the method that checks if the number of elements that wants to copy is in the range of the array (if the number is less than or equals the array size). So the likely cause is weak precondition.

A test case that reveals this nonconformance:

public void testSetMedicalRecommendation(){

 Treatment_Impl var3 = new Treatment_Impl((byte)1, (byte)0, (byte)0);

 byte[] var10 = new byte[] { (byte)0, (byte)0};

 var3.setMedicalRecommendation(var10, (short)100, (short)3, true);

}

Method setTreatmentID

There is an invariant problem in the method setTreatmentID from Treatment_Impl: the nonconformance occurs after the creation of one object Treatment_Impl, one call to the method setAppointmentID in the first call to the method setTreatmentID. So B is equals 3 and D is equals 2 because there is a violation of one invariant specified into the interface Treatment implemented by the class.

This nonconformance occurs by the absence of one precondition in the method that checks the values received as parameter. So the likely cause of this nonconformance is weak precondition.

A test case that reveals this nonconformance:

public void testSetTreatmentID(){

 Treatment_Impl var3 = new Treatment_Impl((byte)0, (byte)100, (byte)0);

 var3.setAppointmentID((byte)100);

 var3.setTreatmentID((byte)(-1));

}

Class Vaccine_Impl

Method setDesignation

There is a precondition problem in the method setDesignation from Vaccine_Impl: the nonconformance occurs after the creation of one object Vaccines_Impl, a creation of one object Treatment_Impl, one call to the method getHealthProblem from Treatment_Impl (that is assigned to the variable used in the call to method setVaccineDesignation (that calls setDesignation in its body) from Vaccines_Impl), in the first call to the method setVaccineDesignation. So B is equals 4 and D is equals 3 because the nonconformance is revealed in the precondition of the method setDesignation from Vaccine_Impl that is specified at the interface Vaccine.

This nonconformance occurs possibly by the strong precondition of the method setDesignation - that specifies that the array received as parameter must be not null and has size 4. So the likely cause is strong precondition.

A test case that reveals this nonconformance:

public void testSetDesignation(){

 Vaccines_Impl var0 = new Vaccines_Impl();

 Treatment_Impl var12 = new Treatment_Impl((byte)1, (byte)0, (byte)0);

 byte[] var13 = var12.getHealthProblem();

 var0.setVaccineDesignation((short)1, var13);

}

Class Vaccines_Impl

Method getVaccineDesignation

There is a postcondition problem in the method getVaccineDesignation from Vaccines_Impl: the nonconformance occurs after the creation of one object Vaccines_Impl in the first call to the method getVaccineDesignation. So B is equals 2 and D is equals 2 because the nonconformance is revealed in the specification into the interface Vaccines implemented by Vaccines_Impl.

This nonconformance occurs by a try to access a position from the array with null value - since in the constructor only 3 elements are initialized - causing a NullPointerException (try to access a method of a null object), that is not specified in the exceptional behaviour of the method. So the likely cause of this problem is strong postcondition.

A test case that reveals this nonconformance:

public void testGetVaccineDesignation(){

 Vaccines_Impl var0 = new Vaccines_Impl();

 byte[] var2 = var0.getVaccineDesignation((short)10);

}

Method removeVaccine

There is a postcondition problem in the method removeVaccine from Vaccines_Impl: the nonconformance occurs after the creation of one object in the first call to the method removeVaccine - So B is equals 2 and D is equals 2 because the nonconformance is revealed in the specification into the interface Vaccines implemented by Vaccines_Impl.

This nonconformance occurs by a try to remove one element of one position from the array that exceeds its the size, causing an exception; but in the exceptional behaviour is expected only UserException and occurs an ArrayIndexOutOfBoundsException. So the likely cause is strong postcondition.

A test case that reveals this nonconformance:

public void testRemoveVaccine(){

 Vaccines_Impl var0 = new Vaccines_Impl();

 var0.removeVaccine((short)25601);

}

Method setVaccineDesignation

There is a postcondition problem in the method setVaccineDesignation from Vaccines_Impl: the nonconformance occurs after the creation of one object Vaccines_Impl, a creation of one array that will be used in the call to the method, and one call to the method setVaccineDesignation. So B is equals 3 and D is equals 2 because the nonconformance is revealed in the specification into the interface Vaccines implemented by Vaccines_Impl.

This nonconformance occurs by a try to access the method setDesignation in the body of the method of one position from the array whose object is null - since the default constructor initializes only 3 elements occurs one exception, carrying the method to the exceptional behaviour; but is expected only UserException and the exception that occurs is a NullPointerException. So the likely cause is strong postcondition.

A test case that reveals this nonconformance:

public void testSetVaccineDesignation(){

 Vaccines_Impl var0 = new Vaccines_Impl();

 byte[] var11 = new byte[] { (byte)10};

 var0.setVaccineDesignation((short)10, var11);

}

Method validateVaccinePosition

There is a postcondition problem in the method validateVaccinePosition from Vaccines_Impl: the nonconformance occurs after the creation of one object Vaccines_Impl and one call to method validateVaccinePosition. So B is equals 2 and D is equals 3 because into the body of validateVaccinePosition there is a call to the method validateObjectArrayPosition from CardUtil with value less than zero, returning false, causing the exceptional behaviour specified at the interface Vaccines.

This nonconformance occurs because the method validateObjectArrayPosition returns false when receives a value less than zero, causing the exceptional behaviour of the method. So the likely cause is strong postcondition.

A test case that reveals this nonconformance:

public void testValidateVaccinePosition(){

 Vaccines_Impl var0 = new Vaccines_Impl();

 boolean var1 = var0.validateVaccinePosition((short)(-1));

}

• On Jaccounting:

Class Account

Method getCurrency

There is an evaluation problem in the method getCurrency from Account: the nonconformance occurs after the creation of one object Account, one call to the method setID and one call to the method getCurrency. So B is equals 3 and D is equals 1 because the nonconformance occurs directly in the called method.

This nonconformance occurs because in the default constructor the attribute currency is not initialized, inducing the method to return null which forbid the evaluation of the postcondition clause. Possibly if the precondition of this method was not requires true; and checks if the attribute currency is not null the nonconformance would not occur.

A test case that reveals this nonconformance:

public void testGetCurrency(){

 Account var0 = Account.getDefault();

 var0.setId((Integer)1);

 String var3 = var0.getCurrency();

}

Method getDescription

There is an evaluation problem in the method getDescription from Account: the nonconformance occurs after the creation of one object Account and one call to the method getDescription. So B is equals 2 and D is equals 1 because the nonconformance occurs directly in the called method.

This nonconformance occurs because in the default constructor the attribute description is not initialized, inducing the method to return null which forbid the evaluation of the postcondition clause. Possibly if the precondition of this method was not requires true; and checks if the attribute description is not null the nonconformance would not occur.

A test case that reveals this nonconformance:

public void testGetDescription(){

 Account var0 = new Account();

 String var4 = var0.getDescription();

}

Method getName

There is a postcondition problem in the method getName from Account: the nonconformance occurs after the creation of one object Account, one call to the method setDetailTypeKey and one call to method getName. So B is equals 3 and D is equals 1 because the nonconformance occurs directly in the method.

This nonconformance occurs because the default constructor does not initializes the attribute name, causing a null return of the method. So the likely cause is weak precondition.

A test case that reveals this nonconformance:

public void testGetName(){

 Account var0 = new Account();

 var0.setDetailTypeKey(0);

 String var5 = var0.getName();

}

Class AClass

There is a postcondition problem in the method getName from AClass: the nonconformance occurs after the creation of one AClass object with the static method getDefault and one call to the method getName. So B is equals 2 and D is equals 1 because the nonconformance occurs directly in the method.

This nonconformance occurs because there is not a precondition in the method that checks if the attribute name is different of empty string. So the likely cause is weak precondition.

A test case that reveals this nonconformance:

public void testAClass(){

 AClass var0 = AClass.getDefault();

 String var2 = var0.getName();

}

Class ArrayUtils

Method getMaxIntArrayIndex

There is a postcondition problem in the method getMaxIntArrayIndex from ArrayUtils: the nonconformance occurs after the creation of one array of integers and one call to the method getMaxIntArrayIndex. So B is equals 2 and D is equals 1 because the nonconformance occurs directly in the method.

This nonconformance occurs because there is a try to access values from a empty array causing an ArrayIndexOutOfBoundsException; possibly because there is not check in the precondition if the array received as parameter is not empty (if the size is greater than zero). So the likely cause is weak precondition.

A test case that reveals this nonconformance:

public void testGetMaxIntArrayIndex(){

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

 int var1 = ArrayUtils.getMaxIntArrayIndex(var0);

}

Method stringArrayToIntArray

There is a postcondition problem in the method stringArrayToIntArray from ArrayUtils: the nonconformance occurs after the creation of one array of strings and one call to method stringArrayToIntArray. So B is equals 2 and D is equals 1 because the nonconformance occurs directly in the method.

This nonconformance occurs because there is a try to convert an array with only one element - the empty string - into an array of integers causing a NumberFormatException; possibly because there is not a check if the parameter received is a valid array. So the likely cause is weak precondition.

A test case that reveals this nonconformance:

public void testStringArrayToIntArray(){

 String[] var1 = new String[] { ""};

 int[] var4 = ArrayUtils.stringArrayToIntArray(var1);

}

Class ByteArrayDataSource (mail)

Method byteArrayDataSource

There is an invariant problem in the method byteArrayDataSource from the class ByteArrayDataSource (package mail): the nonconformance occurs after a bytes array creation and one call to the constructor from the class. So B is equals 2 and D is equals 2 because the default invariant is violated in the call to the method byteArrayDataSource into the constructor of the class.

This nonconformance occurs because one attribute from the class (baos) is not initialized into the constructor. So the category of this nonconformance is a code error - the not initialization of all attributes from the class.

A test case that reveals this nonconformance:

public void testByteArrayDataSource(){

 byte[] var3 = new byte[] { (byte)0};

 ByteArrayDataSource var5 = new ByteArrayDataSource(var3, "country_select");

}

Class ByteArrayDataSource (util)

Constructor

There is an invariant problem in the class ByteArrayDataSource (package util): the nonconformance occurs after the creation of one array of bytes and one call to the constructor from the class. So B is equals 2 and D is equals 1 because the default invariant of JML is violated directly in the constructor.

This nonconformance occurs because one attribute from the class (baos) is not initialized into the constructor. So the category of this nonconformance is a code error - the not initialization of all attributes from the class.

A test case that reveals this nonconformance:

public void testConstructor(){

 byte[] var5 = new byte[] { (byte)100};

 ByteArrayDataSource var7 = new ByteArrayDataSource(var5, "hi!");

}

Class Charge

There is an invariant problem in the class Charge: the nonconformance occurs after the creation of one object Charge. So B is equals 1 and D is equals 1 because the default invariant of JML is violated directly in the constructor.

This nonconformance occurs because some attributes from the class are not initialized in the constructor. So the category of this nonconformance is a code error - the not initialization of all attributes from the class.

A test case that reveals this nonconformance:

public void testCharge(){

 Charge var0 = new Charge();

}

Class Company

There is a postcondition problem in the method getId from Company: the nonconformance occurs after the creation of one object Company, one modification of this object with the method setActive and one call to getId. So B is equals 3 and D is equals 1 the nonconformance is revealed directly in the method.

This nonconformance has as likely cause the lack of a precondition in the method that checks if the attribute id is not null. So the likely cause is weak precondition.

A test case that reveals this nonconformance:

public void testCompany(){

 Company var0 = new Company();

 var0.setActive(true);

 Integer var4 = var0.getId();

}

Class CookieUtils

Method getCookie

There is a postcondition problem in the method getCookie from CookieUtils: the nonconformance occurs in the call to the static method getCookie from CookieUtils. So B is equals 1 and D is equals 3 because into the method there is a creation of an Cookie object from Javax.servlet and one call to the method setMaxAge from Cookie.

This nonconformance occurs by the launching of an IllegalArgumentException. It occurs because there is not a precondition that checks valid inputs to parameters name and value, only the parameter seconds is checked. So the likely cause is: weak precondition.

A test case that reveals this nonconformance:

public void testGetCookie(){

 javax.servlet.http.Cookie var3 = CookieUtils.getCookie("<select name=\"color_select\" id=\"color_select\">\n<option value=\"Black\" style=\"color:Black\">Black\n<option value=\"Maroon\" style=\"color:Maroon\">Maroon\n<option value=\"Green\" style=\"color:Green\">Green\n<option value=\"Olive\" style=\"color:Olive\">Olive\n<option value=\"Navy\" style=\"color:Navy\">Navy\n<option value=\"Purple\" style=\"color:Purple\">Purple\n<option value=\"Teal\" style=\"color:Teal\">Teal\n<option value=\"Gray\" style=\"color:Gray\">Gray\n<option value=\"Silver\" style=\"color:Silver\">Silver\n<option value=\"Red\" style=\"color:Red\">Red\n<option value=\"Lime\" style=\"color:Lime\">Lime\n<option value=\"Yellow\" style=\"color:Yellow\">Yellow\n<option value=\"Blue\" style=\"color:Blue\">Blue\n<option value=\"Fuschia\" style=\"color:Fuschia\">Fuschia\n<option value=\"Aqua\" style=\"color:Aqua\">Aqua\n<option value=\"White\" style=\"color:White\">White\n</select>\n0", "accountKey=0     companyKey=nulljournalEntryKey=0Amount=null memo:null", 2);

}

Method getDeleteCookie

There is a postcondition problem in the method getDeleteCookie from CookieUtils: the nonconformance occurs in the call to the static method getDeleteCookie from CookieUtils. So B is equals 1 and D is equals 3 because into the method there is a creation of one Cookie object from Javax.servlet, and one call to method setMaxAge from Cookie.

This nonconformance occurs by the launching of an IllegalArgumentException. It occurs because there is not a precondition that checks valid inputs to the method parameters. So the likely cause is: weak precondition.

A test case that reveals this nonconformance:

public void testGetDeleteCookie(){

 javax.servlet.http.Cookie var1 = CookieUtils.getDeleteCookie("<select id=\"month_select\" name=\"month_select\">\n<option value=\"0\">January\n<option value=\"1\">February\n<option value=\"2\">March\n<option value=\"3\">April\n<option value=\"4\">May\n<option value=\"5\">June\n<option value=\"6\">July\n<option value=\"7\">August\n<option value=\"8\">September\n<option value=\"9\">October\n<option value=\"10\" SELECTED>November\n<option value=\"11\">December\n</select>\n");

}

Class CustomerLog

There is a postcondition problem in the method getCustomerKey from CustomerLog: the nonconformance occurs after the creation of one CustomerLog object and one call to the method getCustomerKey. So B is equals 2 and D is equals 1 because the nonconformance is revealed directly into the method.

This nonconformance occurs because the attribute customerKey is not initialized, receiving the default value to integers: 0, but in the postcondition there is a clause specifying that the result must be greater than zero. So the likely cause is weak precondition.

A test case that reveals this nonconformance:

public void testGetCustomerKey(){

 CustomerLog var0 = new CustomerLog();

 int var4 = var0.getCustomerKey();

}

Class DateUtils

There is a postcondition problem in the method monthAsString from DateUtils: the nonconformance occurs in the call to the static method monthAsString. So B is equals 1 and D is equals 1 because the nonconformance is revealed directly in the method.

This nonconformance probably occurs by the absence of a precondition to check the parameter of the method (check if the value is in a valid range). So the likely cause is weak precondition.

A test case that reveals this nonconformance:

public void testDateUtils(){

 String var1 = DateUtils.monthAsString(100);

}

Class Mailer (mail)

There is an invariant problem in the class Mailer (from package mail): the nonconformance occurs after the creation of one object Mailer. So B is equals 1 and D is equals 1 because the nonconformance occurs directly in the call to the constructor.

This nonconformance occurs because some attributes from the class (to, from, cc, bcc, subject, and body) are not initialized in the constructor, violating the invariant default of JML. So the category of this nonconformance is code error - the not initialization of all attributes from the class.

A test case that reveals this nonconformance:

public void testMailer(){

 mail.Mailer var1 = new mail.Mailer("0000000001");

}

Class Mailer (util)

There is an invariant problem in the class Mailer (from package util): the nonconformance occurs after the creation of one object Mailer. So B is equals 1 and D is equals 1 because the nonconformance occurs directly in the call to the constructor.

This nonconformance occurs because some attributes from the class (to, from, cc, bcc, subject, and body) are not initialized in the constructor, violating the invariant default of JML. So the category of this nonconformance is code error - the not initialization of all attributes from the class.

A test case that reveals this nonconformance:

public void testMailer(){

 util.Mailer var1 = new util.Mailer("ByteArrayDataSource");

}

Class PageElements

There is an invariant problem in the class PageElements: the nonconformance occurs after the creation of one object RegisterAction. So B is equals 1 and D is equals 4 because RegisterAction is a subclass of Register and Register is a subclass of Base the in its body calls the default constructor of PageElements - whose constructor does not initializes all attributes from the class.

This nonconformance occurs because some attributes from the class (pageTitle, sectionColor, sectionTitle, and mainPage) are not initialized in the constructor, violating the invariant default of JML. So the category of this nonconformance is code error - the not initialization of all attributes from the class.

A test case that reveals this nonconformance:

public void testPageElements(){

 RegisterAction var0 = new RegisterAction();

}

Class PaymentDistribution

There is an invariant problem in the class PaymentDistribution: the nonconformance occurs after the creation of one object PaymentDistribution. So B is equals 1 and D is equals 1 because the nonconformance occurs directly in the call to the constructor.

This nonconformance occurs because some attributes from the class (id, paymentKey, invoiceKey, transaction, transactionKey, and companyKey) are not initialized in the constructor, violating the invariant default of JML. So the category of this nonconformance is code error - the not initialization of all attributes from the class.

A test case that reveals this nonconformance:

public void testPaymentDistribution(){

 PaymentDistribution var0 = new PaymentDistribution();

}

Class Preferences

There is an invariant problem in the class Preferences: the nonconformance occurs after the creation of one object Preferences. So B is equals 1 and D is equals 1 because the nonconformance occurs directly in the call to the constructor.

This nonconformance occurs because one attribute from the class (fromEmail) is not initialized in the constructor, violating the default constructor of JML. So the category of this nonconformance is code error - the not initialization of all attributes from the class.

A test case that reveals this nonconformance:

public void testPreferences(){

 Preferences var0 = new Preferences();

}

Class Product

There is an invariant problem in the class Product: the nonconformance occurs after the creation of one object Product by the call to the method getDefault. So B is equals 1 and D is equals 2 because the nonconformance occurs when the method calls the default constructor of the class that not initializes all attributes from the class.

This nonconformance occurs because some attributes from the class (id, companyKey e accountKey) are not initialized in the constructor, violating the invariant default of JML. So the category of this nonconformance is code error - the not initialization of all attributes from the class.

A test case that reveals this nonconformance:

public void testProduct(){

 Product var0 = Product.getDefault();

}

Class Recurrence

There is an invariant problem in the class Recurrence: the nonconformance occurs after the creation of one object Recurrence. So B is equals 1 and D is equals 1 because the nonconformance occurs directly in the constructor of the class.

This nonconformance occurs because some attributes from the class (realm, itemKey, startDate, endDate, and nextDate) are not initialized in the constructor, violating the invariant default of JML. So the category of this nonconformance is code error - the not initialization of all attributes from the class.

A test case that reveals this nonconformance:

public void testRecurrence(){

 Recurrence var2 = new Recurrence();

}

Class StringDataSource

There is an invariant problem in the class StringDataSource: the nonconformance occurs after the creation of one object StringDataSource. So B is equals 1 and D is equals 1 because the nonconformance occurs directly in the constructor of the class.

This nonconformance occurs because some attributes from the class (s, in, and out) are not initialized in the constructor, violating the invariant default of JML. So the category of this nonconformance is code error - the not initialization of all attributes from the class.

A test case that reveals this nonconformance:

public void testStringDataSource(){

 StringDataSource var0 = new StringDataSource();

}

Class Tax

There is an invariant problem in the class Tax: the nonconformance occurs after the creation of one object Tax by the call to the method getDefault. So B is equals 1 and D is equals 2 because the nonconformance occurs when the method calls the default constructor of the class that not initializes all attributes from the class.

This nonconformance occurs because some attributes from the class (id, companyKey, percent, name, payableAccountKey, receivableAccountKey, and invoiceKey) are not initialized in the constructor, violating the invariant default of JML. So the category of this nonconformance is code error - the not initialization of all attributes from the class.

A test case that reveals this nonconformance:

public void testTax(){

 Tax var2 = Tax.getDefault();

}

• On Mondex:

Class APDU

There is an invariant problem in the class APDU: the nonconformance occurs after the creation of one object APDU. So B is equals 1 and D is equals 1 because the nonconformance occurs directly in the constructor.

This nonconformance occurs because one of attributes of the class is not initialized in the constructor, receiving null value and violating the JML default invariant. So the category of this nonconformance is code error - the not initialization of one attribute of the class.

A test case that reveals this nonconformance:

public void testAPDU(){

 APDU var0 = new APDU();

}

Class ConPurseJC

There is an invariant problem in the class ConPurseJC: the nonconformance occurs after the creation of one array of bytes that will be used in the call to the static method install (method that initializes one object ConPurseJC). So B is equals 2 and D is equals 2 because the nonconformance is revealed when into the method there is a call to the default constructor of the class.

This nonconformance occurs because one invariant of the class is violated after the creation of the object in the constructor default. The category of this nonconformance is code error. (We have confirmed this after contact the authors of Mondex - they had two versions of the project and an erroneous version stayed available).

A test case that reveals this nonconformance:

public void testConPurseJC(){

 byte[] var2 = new byte[] { (byte)1, (byte)(-1)};

 ConPurseJC.install(var2);

}

• On TransactedMemory:

Package AbstractJMLSpec

Class AbstractTransactedMemory

There is a postcondition problem at the method ANewTag in the class AbstractedTransactedMemory: the nonconformance occurs after several object creations and modifications, resulting in the throw of one exception in the method ANewTag. So B receives 32 and D receives 2 because the nonconformance occurs in the call to method choose of class JMLValueSet into the body of ANewTag.

This nonconformance occurs when into the method ANewTag there is a try to use the method choose using a empty set of values (attribute TAGS), launching one JMLNoSuchElementException. This problem has as likely cause the weak precondition of the method that does not check if TAGS is empty.

A test case that reveals this nonconformance:

public void testANewTag(){

 TagToInfoSeqSeqMap var2 = new TagToInfoSeqSeqMap();

 TagToInfoSeqSeqMap var3 = new TagToInfoSeqSeqMap();

 org.jmlspecs.models.JMLValueToValueRelation var4 = var2.difference((org.jmlspecs.models.JMLValueToValueRelation)var3);

 TagToInfoSeqSeqMap var20 = new TagToInfoSeqSeqMap();

 org.jmlspecs.models.JMLValueToValueRelation var24 = var2.remove((org.jmlspecs.models.JMLType)var6, (org.jmlspecs.models.JMLType)var20);

 TagToInfoSeqSeqMap var25 = new TagToInfoSeqSeqMap();

 TagToInfoSeqSeqMap var26 = new TagToInfoSeqSeqMap();

 org.jmlspecs.models.JMLValueToValueRelation var27 = var25.difference((org.jmlspecs.models.JMLValueToValueRelation)var26);

 TagToInfoSeqSeqMap var29 = new TagToInfoSeqSeqMap();

 TagToInfoSeqSeqMap var31 = new TagToInfoSeqSeqMap();

 org.jmlspecs.models.JMLValueToValueRelation var33 = var29.difference((org.jmlspecs.models.JMLValueToValueRelation)var31);

 org.jmlspecs.models.JMLValueToValueRelationEnumerator var35 = var31.elements();

 InfoSeqSeq var37 = new InfoSeqSeq();

 org.jmlspecs.models.JMLValueSet var39 = var37.toSet();

 org.jmlspecs.models.JMLValueToValueMap var40 = var31.rangeRestrictedTo(var39);

 org.jmlspecs.models.JMLValueToValueMap var41 = var25.restrictedTo(var39);

 TagToInfoSeqSeqMap var45 = new TagToInfoSeqSeqMap();

 InfoSeqSeq var58 = new InfoSeqSeq();

 InfoSeqSeq var59 = new InfoSeqSeq();

 InfoSeqSeq var62 = new InfoSeqSeq();

 org.jmlspecs.models.JMLValueSequence var65 = var59.insertFront((org.jmlspecs.models.JMLType)var62);

 org.jmlspecs.models.JMLValueSequence var66 = var58.insertFront((org.jmlspecs.models.JMLType)var62);

 InfoSeqSeq var68 = new InfoSeqSeq();

 InfoSeqSeq var72 = new InfoSeqSeq();

 org.jmlspecs.models.JMLValueSequence var76 = var68.insertFront((org.jmlspecs.models.JMLType)var72);

 org.jmlspecs.models.JMLValueSequence var77 = var66.insertAfterIndex(0, (org.jmlspecs.models.JMLType)var68);

 org.jmlspecs.models.JMLValueSet var79 = var45.inverseElementImage((org.jmlspecs.models.JMLType)var66);

 org.jmlspecs.models.JMLValueToValueRelation var80 = var25.restrictRangeTo(var79);

 org.jmlspecs.models.JMLValueToValueMap var81 = var2.disjointUnion((org.jmlspecs.models.JMLValueToValueMap)var25);

 org.jmlspecs.models.JMLValueSet var82 = var25.range();

 AbstractTransactedMemory var83 = new AbstractTransactedMemory(100, 10, var82);

 Tag var85 = var83.ANewTag(100);

}

Package JavaImplementation

Class DPage

There is an invariant problem in the class DPage: the nonconformance occurs after the creation of one object DPage. So B is equals 1 and D is equals 1 because one invariant of this class is violated directly in the constructor.

This nonconformance occurs because of the violation of the invariant that specifies the set of possible values to the attribute version (VA == 0 or VB == 1 or VC == 2); but in the constructor there is not checking about the value received in the parameter version (that will assigned to the attribute of the class); so the likely cause is: weak precondition.

A test case that reveals this nonconformance:

public void testDPage(){

 DPage var6 = new DPage(true, 0, 100, 1, 1, 100);

}

Class DTagData

There is an invariant problem in the class DTagData: the nonconformance occurs after the creation of one object DTagData. So B is equals 1 and D is equals 1 because one invariant of the class is violated directly in the constructor.

This nonconformance occurs because the invariant that specifies the valor of attribute size must be greater than zero; but in the constructor is not checked the value received in the parameter size (that will be asigned to the attribute of the class); so the likely cause is: weak precondition.

A test case that reveals this nonconformance:

public void testDTagData(){

 DTagData var3 = new DTagData(true, (-1), false);

}

Package JavaImplementationEnums

Class Generation

There is an invariant problem in the class Generation: the nonconformance occurs after the creation of one object Generation. So B is equals 1 and D is equals 1 because one invariant of the class is violated directly in the constructor.

This nonconformance occurs because there is an invariant that restricts the range ([0; 5]) of values to value attribute; but in the constructor is not checked the value received in the parameter sh (that will be assigned to value); so the likely cause is: weak precondition.

A test case that reveals this nonconformance:

public void testGeneration(){

 Generation var1 = new Generation(10);

}

Class GenGenbyte

There is an invariant problem in the class GenGenbyte: the nonconformance occurs in the call to static method ReallyDTidy from the class TestFramework. So B is equals 1 and D is equals 8 because the nonconformance occurs when into the method ReallyDTidy of TestFramework there is a call to method DTidy of TransactedMemory, that calls the method DGeneration also of TransactedMemory and into this method, that creates an object GenGenbyte, there are several iterations (at least 4) with the object until violates the GenGenbyte invariant.

This nonconformance occurs by the violation of the invariant from the class GenGenbyte that specifies the range of valid values to the attribute cnt; but after successive updates in this attribute realized by the method DGeneration from TransactedMemory violates this invariant. So the category of this problem is code error. For a more precise cause is needed an expert in the experimental unit domain.

A test case that reveals this nonconformance:

public void testGenGenbyte(){

 TestFramework.ReallyDTidy();

}

Class Tag

There is an invariant problem in the class Tag: the nonconformance occurs after the creation of one object Tag. So B is equals 1 and D is equals 1 because one invariant of the class is violated directly in the constructor.

This nonconformance occurs by the violation of the invariant from the class that specifies the range of valid values ([0; 6]) to the attribute value; but in the constructor is not checked the value received as parameter; so the likely cause is: weak precondition.

A test case that reveals this nonconformance:

public void testTag(){

 Tag var1 = new Tag(10);

}

Class Version

There is an invariant problem in the class Version: the nonconformance occurs after the creation of one object Version. So B is equals 1 and D is equals 1 because one invariant of the class is violated directly in the constructor.

This nonconformance occurs by the violation of the invariant from the class that specifies the range of valid values to the attribute value (the range [0;2]); but in the constructor is not checked the value received as parameter; so the likely cause is: weak precondition.

A test case that reveals this nonconformance:

public void testVersion(){

 Version var1 = new Version(100);

}

These test cases were sent to lead's projects and the feedback received was positive.

Considering the complete experiment, we detected 84 nonconformances that were categorized and a likely cause was attributed for each nonconformance. In Fig. 1 we present this result considering only the category of the nonconformances.

Fig. 1 The nonconformances detected on RGT Evaluation

And in Fig. 2 we present the likely causes that we attributed for the nonconformances:

Fig. 2 The likely causes for the nonconformances

The complete set of tests that reveal nonconformances explained above is available here.