C4J - Contracts for Java

Class contract example

There are two ways to attach a contract to a class, an "internal" way and an "external" way. The following example uses the internal way, i.e. the class refers to its contract class by using the C4J Annotation @ContractReference.
That means, that the source code of the target class has to modified which is not the case when using external contracts.
The target class TimeOfDay uses the internal way and looks like this (complete listing):

package timeofday;

import de.vksi.c4j.ContractReference;
import de.vksi.c4j.Pure;

@ContractReference(TimeOfDayContract.class)
public class TimeOfDay {
   public static final int HOUR_MIN = 0;
   public static final int HOUR_MAX = 23;
   public static final int MINUTE_MIN = 0;
   public static final int MINUTE_MAX = 59;
   public static final int SECOND_MIN = 0;
   public static final int SECOND_MAX = 59;

   private int hour;
   private int minute;
   private int second;

   public TimeOfDay(int hour, int minute, int second) {
      setHour(hour);
      setMinute(minute);
      setSecond(second);
   }

   public void setHour(int hour) {
      this.hour = hour;
   }

   public void setMinute(int minute) {
      this.minute = minute;
   }

   public void setSecond(int second) {
      this.second = second;
   }

   @Pure
   public int getHour() {
      return hour;
   }

   @Pure
   public int getMinute() {
      return minute;
   }

   @Pure
   public int getSecond() {
      return second;
   }
}

The corresponding contract class TimeOfDayContract extends TimeOfDay and looks like this (complete listing):

package timeofday;

import static de.vksi.c4j.Condition.ignored;
import static de.vksi.c4j.Condition.postCondition;
import static de.vksi.c4j.Condition.preCondition;
import static de.vksi.c4j.Condition.unchanged;
import de.vksi.c4j.ClassInvariant;
import de.vksi.c4j.Target;

public class TimeOfDayContract extends TimeOfDay {
   @Target
   private TimeOfDay target;

   @ClassInvariant
   public void classInvariant() {
      assert target.getHour() >= HOUR_MIN : "hour >= HOUR_MIN";
      assert target.getHour() <= HOUR_MAX : "hour <= HOUR_MAX";
      assert target.getMinute() >= MINUTE_MIN : "minute >= MINUTE_MIN";
      assert target.getMinute() <= MINUTE_MAX : "minute <= MINUTE_MAX";
      assert target.getSecond() >= SECOND_MIN : "second >= SECOND_MIN";
      assert target.getSecond() <= SECOND_MAX : "second <= SECOND_MAX";
   }

   public TimeOfDayContract(int hour, int minute, int second) {
      super(hour, minute, second);
      if (preCondition()) {
         assert hour >= HOUR_MIN : "hour >= HOUR_MIN";
         assert hour <= HOUR_MAX : "hour <= HOUR_MAX";
         assert minute >= MINUTE_MIN : "minute >= MINUTE_MIN";
         assert minute <= MINUTE_MAX : "minute <= MINUTE_MAX";
         assert second >= SECOND_MIN : "second >= SECOND_MIN";
         assert second <= SECOND_MAX : "second <= SECOND_MAX";
      }
      if (postCondition()) {
         assert target.getHour() == hour : "hour set";
         assert target.getMinute() == minute : "minute set";
         assert target.getSecond() == second : "second set";
      }
   }

   @Override
   public void setHour(int hour) {
      if (preCondition()) {
         assert hour >= HOUR_MIN : "hour >= HOUR_MIN";
         assert hour <= HOUR_MAX : "hour <= HOUR_MAX";
      }
      if (postCondition()) {
         assert target.getHour() == hour : "hour set";
         assert unchanged(target.getMinute()) : "minute unchanged";
         assert unchanged(target.getSecond()) : "second unchanged";
      }
   }

   @Override
   public void setMinute(int minute) {
      if (preCondition()) {
         assert minute >= MINUTE_MIN : "minute >= MINUTE_MIN";
         assert minute <= MINUTE_MAX : "minute <= MINUTE_MAX";
      }
      if (postCondition()) {
         assert unchanged(target.getHour()) : "hour unchanged";
         assert target.getMinute() == minute : "minute set";
         assert unchanged(target.getSecond()) : "second unchanged";
      }
   }

   @Override
   public void setSecond(int second) {
      if (preCondition()) {
         assert second >= SECOND_MIN : "second >= SECOND_MIN";
         assert second <= SECOND_MAX : "second <= SECOND_MAX";
      }
      if (postCondition()) {
         assert unchanged(target.getHour()) : "hour unchanged";
         assert unchanged(target.getMinute()) : "minute unchanged";
         assert target.getSecond() == second : "second set";
      }
   }

   @Override
   public int getHour() {
      return ignored();
   }

   @Override
   public int getMinute() {
      return ignored();
   }

   @Override
   public int getSecond() {
      return ignored();
   }
}

Please note that all these assertions have been implicit before and have now become explicit. The content of the contract class TimeOfDayContract is therefore most valuable to users of class TimeOfDay. The C4J javadoc tool (available in Q2/2013) creates a javadoc class documentation including contract class assertions.