C4J provides these annotations to define special attributes of a class, method or variable:
- @ContractReference
- @Contract
- @Target
- @ClassInvariant
- @Pure
- @PureTarget
Each of these annotations wil now be described by an example.
@ContractReference annotates a class or an interface as guarded by the indicated contract class.
@ContractReference(TimeOfDayContract.class)
public class TimeOfDay {
...
Read as: The class TimeOfDay is guarded by the contract class TimeOfDayContract.
@Contract annotates an contract class as being an external contract for extended class or implemented interface.
@Contract
public class TimeOfDayContract extends TimeOfDay {
...
Read as: The contract class TimeOfDayContract guards the class TimeOfDay as an external contract.
@Target annotates an instance variable as being the reference to the guarded object (the target). There can be only one instance variable annoted as target reference. The name of the instance variable is arbitrary, but it is good contract coding style to name it target. The visibilty should be private as this reference will only be used within the class contract it is declared in. The type is always the type of the target class which is the class the contract class extends or the interface the contract class implements.
public class TimeOfDayContract extends TimeOfDay {
@Target
private TimeOfDay target;
...
Read as: The private instance variable target of type TimeOfDay is a reference to the guarded object (the target) of type TimeOfDay.
@ClassInvariant annotates a method as the class invariant of the guarded class. If more than one method is annoted as class invariant, all of them are concatenated to one big method. The name of the method is arbitrary, but it is good contract coding style to name it classInvariant.
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";
}
...
Read as: The public method classInvariant() is a class invariant. It ensures that getHour() always returns a value between HOUR_MIN and HOUR_MAX, getMinute() always returns a value between MINUTE_MIN and MINUTE_MAX and getSecond() always returns a value between SECOND_MIN and SECOND_MAX.
@Pure annotates pure methods, i.e. queries without side effects. A contract class is only allowed to use pure methods, as there must be no difference in the behavior of the guarded class whether the contract guards it or not.
@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;
@Pure
public int getHour() {
return hour;
}
@Pure
public int getMinute() {
return minute;
}
@Pure
public int getSecond() {
return second;
}
...
Read as: The public methods getHour, getMinute and getSecond are pure, i.e. queries without any side effect which can therefore be used in contract classes.
@PureTarget annotates pure methods from an external contract class.
@Contract
public class TimeOfDayContract extends TimeOfDay {
@Override
@PureTarget
public int getHour() {
return ignored();
}
@Override
@PureTarget
public int getMinute() {
return ignored();
}
@Override
@PureTarget
public int getSecond() {
return ignored();
}
...
Read as: The public methods getHour, getMinute and getSecond in the target class TimeOfDay are pure, i.e. queries without any side effect which can therefore be used in contract classes.
C4J provides these static methods to implement contract clauses:
- preCondition()
- postCondition()
- ignored()
- result()
- old()
- unchanged()
Each of these static methods will now be described by an example.
preCondition() allows us to implement a precondition for a method.
public class TimeOfDayContract extends TimeOfDay {
@Override
public void setHour(int hour) {
if (preCondition()) {
assert hour >= HOUR_MIN : "hour >= HOUR_MIN";
assert hour <= HOUR_MAX : "hour <= HOUR_MAX";
}
}
...
Read as: The method setHour of class TimeOfDay has a precondition which requires that the value of the method parameter hour is between HOUR_MIN and HOUR_MAX.
postCondition() allows us to implement a postcondition for a method.
public class TimeOfDayContract extends TimeOfDay {
@Target
private TimeOfDay target;
@Override
public void setHour(int hour) {
if (postCondition()) {
assert target.getHour() == hour : "hour set";
}
}
...
Read as: The method setHour of class TimeOfDay has a postcondition which ensures that the value of hour is successfully set, i.e. calling the method getHour() on target will return the value of hour.
ignored() is needed when the guarded method has a return value, i.e. is a query. A contract class has to extend the target class or implement the target interface. All methods of the target class or target interface have to be overridden in the contract class. As the overriding method in the contract class must have the same signature as the guarded method in the target class, it also has to return a dummy value of the right type. This dummy return value is created by calling ignored().
public class TimeOfDayContract extends TimeOfDay {
@Override
public int getHour() {
return ignored();
}
...
Read as: The method getHour() of class TimeOfDay has a return value of type int. Therefore the corresponding method getHour of the contract class TimeOfDayContract needs a dummy return value of type int, which is created by calling ignored().
result() gives a postcondition access to the return value of the guarded method. It is good coding style to assign the return value of result() to a local variable named result, which has to have the same type as the return value of the guarded method.
public class TimeOfDayContract extends TimeOfDay {
@Override
public int getHour() {
if(postCondition()) {
int result = result();
assert result >= HOUR_MIN : "result >= HOUR_MIN";
assert result <= HOUR_MAX : "result <= HOUR_MAX";
}
return ignored();
}
...
Read as: The method setHour of class TimeOfDay has a postcondition which ensures that the returned value, i.e. the result of calling this method is between HOUR_MIN and HOUR_MAX.
old() allows us in postconditions to get access to the value of a target attribute as it has been in the precondition, i.e. before the guarded method has been executed.
public class TimeOfDayContract extends TimeOfDay {
@Target
private TimeOfDay target;
@Override
public void nextHour() {
if (postCondition()) {
if (old(target.getHour()) < HOUR_MAX) {
assert target.getHour() == old(target.getHour()) + 1 : "if old hour < HOUR_MAX then hour == old hour + 1";
}
else {
assert target.getHour() == HOUR_MIN : "if old hour == HOUR_MAX then hour == HOUR_MIN";
}
}
}
...
Read as: The method nextHour of class TimeOfDay has a postcondition which ensures that hour will be set to the next valid hour between HOUR_MIN and HOUR_MAX.
unchanged() allows us in postconditions to ensure that a dedicated target attribute did not change since the call of the precondition, i.e. before the guarded method has been executed. By that we can exactly frame the intended side effect of the guarded method.
public class TimeOfDayContract extends TimeOfDay {
@Target
private TimeOfDay target;
@Override
public void setHour(int hour) {
if (postCondition()) {
assert target.getHour() == hour : "hour set";
assert unchanged(target.getMinute()) : "minute unchanged";
assert unchanged(target.getSecond()) : "second unchanged";
}
}
...
Read as: The method setHour of class TimeOfDay has a postcondition which ensures that only hour will be set to a new value whereas minute and second will remain unchanged.