External 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 external way, i.e. the contract class refers to its target class by using the C4J Annotation @Contract and extending the target class.
That means, that the source code of the target class has not to be modified which is especially important for adding contracts to legacy systems.
The target class TimeOfDay uses the external way and looks like this (complete listing): 

package timeofday;

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;
   }

   public int getHour() {
      return hour;
   }

   public int getMinute() {
      return minute;
   }

   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.Contract;
import de.vksi.c4j.PureTarget;
import de.vksi.c4j.Target;

@Contract(forTarget = TimeOfDay.class)
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
   @PureTarget
   public int getHour() {
      return ignored();
   }

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

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

Please note that external contracts need a special configuration of C4J which is explained in the section Configuration.