Testing by Contract

Testing by Contract is a term coined by a paper of Per Madsen Testing by Contract. The idea is that the test case we have written in the Analysis by Contract activity is sufficient to pass the class over to the integration and system tests, ideally performed by TestBots which simulate real world user behaviour. During these tests, any vialoation of the defined contract will by detected by C4J.

A precondition violation indicates that the caller of the method (the customer) did not fulfill its obligations.
That means, the error will be found in the body of the calling method (the customer).

A postcondition violation indicates that the method (the supplier) did not fulfill its obligations.
That means, the error will be found in the body of the called method (the supplier).


By that simple but powerful approach, C4J will lead us directly to the root cause of the problem and not only the symptoms. To experience this fine grained error detection and isolation mechanism, lets provoke some errors on customer and supplier side.

As a rule of thumb, 80 percent of all software errors have their root cause on the caller side. The reason is simple: As without contracts the preconditions are not stated explicitly, the probabilty is very high that the caller of a method deals with wrong assumtions of what this method requires in order to be able to perform its intended task. So let us start with the caller side, i.e. the test case TimeOfDayTest (partial listing): 

public class TimeOfDayTest {
   private TimeOfDaySpec classUnderTest;
   
   private final int HOUR = 23;   // experimental change from 12 to 23
   
   ...
   
   @Test
   public void setHourTest() {
      classUnderTest.setHour(HOUR + 1); // line 46
      assertEquals(HOUR + 1, classUnderTest.getHour());
   }

   ...

Running the modified test case TimeOfDayTest, C4J detects the precondition violation at once: 

java.lang.AssertionError: hour <= HOUR_MAX (pre-condition)
   at timeofday.TimeOfDaySpecContract.setHour(TimeOfDaySpecContract.java:30)
   at timeofday.TimeOfDay.setHour(TimeOfDay.java)
   at timeofday.TimeOfDayTest.setHourTest(TimeOfDayTest.java:46)
   ...

Read as: The method setHourTest of class TimeOfDayTest called at line 46 the method setHour of class TimeOfDay and violated the precondition assertion hour <= HOUR_MAX which is defined in TimeOfDaySpecContract at line 30.

Following the above rule of thumb, only 20 percent of all software errors have their root cause on the supplier side. Most times these errors are hard to find as they are very subtle. So let us undo the above experimental change to our test case TimeOfDayTest and do some experiments on the supplier side, i.e. the class under test TimeOfDay (partial listing): 

@ContractReference(TimeOfDayContract.class)
public class TimeOfDay implements TimeOfDaySpec {
   private int hour;
   private int minute;
   private int second;

   public TimeOfDay(int hour, int minute, int second) {
      setHour(hour);
      setMinute(minute);
      // setSecond(second); // experimental change
   } // line 17

Running the restored test case TimeOfDayTest with the modified class under test TimeOfDay, C4J detects the postcondition violation at once: 

java.lang.AssertionError: second set (post-condition)
   at timeofday.TimeOfDayContract.constructor$(TimeOfDayContract.java:25)
   at timeofday.TimeOfDay.(TimeOfDay.java:17)
   at timeofday.TimeOfDayTest.setUp(TimeOfDayTest.java:21)
   ...

Read as: The method setUp of class TimeOfDayTest called at line 21 the constructor of class TimeOfDay which violated its postcondition assertion second set which is defined in TimeOfDayContract at line 25. That means the error must be found in the method body of the constructor of class TimeOfDay.

Lets try something more subtle. We restore TimeOfDay and insert an unexpected side effet (partial listing): 

@ContractReference(TimeOfDayContract.class)
public class TimeOfDay implements TimeOfDaySpec {
   private int hour;
   private int minute;
   private int second;

   ...
   
   @Override
   public void setHour(int hour) {
      this.hour = hour;
      minute = 0; // new line added as experimental change
   } // line 23

Running the test case TimeOfDayTest again with the restored and newly modified class under test TimeOfDay, C4J detects the postcondition violation again at once: 

java.lang.AssertionError: minute unchanged (post-condition)
   at timeofday.TimeOfDaySpecContract.setHour(TimeOfDaySpecContract.java:34)
   at timeofday.TimeOfDay.setHour(TimeOfDay.java:23)
   at timeofday.TimeOfDayTest.setHourTest(TimeOfDayTest.java:46)
   ...

Read as: The method setHourTest of class TimeOfDayTest called at line 46 the method setHour of class TimeOfDay which violated its postcondition assertion minute unchanged which is defined in TimeOfDayContract at line 34. That means the error must be found in the method body of method setHour of class TimeOfDay.

What about adding an unexpected side effet to a query? Let us restore the class TimeOfDay again and manipulate an query (partial listing): 

@ContractReference(TimeOfDayContract.class)
public class TimeOfDay implements TimeOfDaySpec {
   private int hour;
   private int minute;
   private int second;

   ...
   
   @Override
   public int getHour() {
      second = 0; // line 36 added as an experimental change
      return hour;
   }

Running the test case TimeOfDayTest again with the restored and newly modified class under test TimeOfDay, C4J detects the postcondition violation again at once: 

java.lang.AssertionError: illegal write access on field second
                          in pure method timeofday.TimeOfDay.getHour() on line 36 (post-condition)
   at timeofday.TimeOfDay.getHour(TimeOfDay.java)
   at timeofday.TimeOfDaySpecContract.setHour(TimeOfDaySpecContract.java:33)
   at timeofday.TimeOfDay.setHour(TimeOfDay.java:22)
   at timeofday.TimeOfDay.(TimeOfDay.java:14)
   at timeofday.TimeOfDayTest.setUp(TimeOfDayTest.java:21)
   ...

Read as: The method setUp of class TimeOfDayTest called at line 21 the constructor of class TimeOfDay which called at line 14 method setHour of class TimeOfDay. The postcondition of method setHour defined in contract class TimeOfDaySpecContract called at line 33 the pure method getHour of class TimeOfDay. During the execution of getHour C4J detected an illegal write access on field second in pure method timeofday.TimeOfDay.getHour() in line 36 That means the error must be found in line 36 of the method body of method getHour of class TimeOfDay.

Please note that an illegal write access in a pure method is only detected if the automatic pure validation is activated as described in section Configuration.