Interface contract example

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

package timeofday;

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

@ContractReference(TimeOfDaySpecContract.class)
public interface TimeOfDaySpec {
   int HOUR_MIN = 0;
   int HOUR_MAX = 23;
   int MINUTE_MIN = 0;
   int MINUTE_MAX = 59;
   int SECOND_MIN = 0;
   int SECOND_MAX = 59;

   void setHour(int hour);

   void setMinute(int minute);

   void setSecond(int second);

   @Pure
   int getHour();

   @Pure
   int getMinute();

   @Pure
   int getSecond();

   @Pure
   boolean isBefore(TimeOfDaySpec other);
}

The corresponding contract class TimeOfDaySpecContract implements TimeOfDaySpec 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.result;
import static de.vksi.c4j.Condition.unchanged;
import de.vksi.c4j.ClassInvariant;
import de.vksi.c4j.Target;

public class TimeOfDaySpecContract implements TimeOfDaySpec {
   @Target
   private TimeOfDaySpec 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";
   }

   @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();
   }

   @Override
   public boolean isBefore(TimeOfDaySpec other) {
      if (preCondition()) {
         assert other != null : "other != null";
      }
      if (postCondition()) {
         boolean result = result();
         if (result) {
            assert !other.isBefore(target) : "if isBefore then not other isBefore";
         }
      }
      return ignored();
   }
}

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