A precondition states what a method requires in order to be able to perfom its intended task. If the precondition is violated, the caller of the method (the customer) has broken the contract. Therefore the method (the supplier) is no longer bonded to the contract, i.e. it will no longer ensure that the postconditions will hold. In other words a precondition is an obligation to the customer and a right to the supplier.
The general structure of a precondition in C4J is like that:
if (preCondition()) {
precondition clause 1
precondition clause 2
...
precondition clause n
}
A precondition clause in C4J can be any valid Java source code that contains an assert statement.
What does that mean for our example? The target class TimeOfDay looks like this (partial listing):
@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;
}
}
Constructors may also have preconditions. The corresponding contract class TimeOfDayContract extends TimeOfDay and shows a precondition for the constructor of class TimeOfDay (partial listing):
public class TimeOfDayContract extends TimeOfDay {
public TimeOfDayContract(int hour, int minute, int second) {
super(hour, minute, second);
if (preCondition()) {
assert hour >= HOUR_MIN : "hour >= HOUR_MIN"; // precondition clause 1
assert hour <= HOUR_MAX : "hour <= HOUR_MAX"; // precondition clause 2
assert minute >= MINUTE_MIN : "minute >= MINUTE_MIN"; // precondition clause 3
assert minute <= MINUTE_MAX : "minute <= MINUTE_MAX"; // precondition clause 4
assert second >= SECOND_MIN : "second >= SECOND_MIN"; // precondition clause 5
assert second <= SECOND_MAX : "second <= SECOND_MAX"; // precondition clause 6
}
if (postCondition()) {
...
}
}
Read as: The overloaden constructor of class TimeOfDay has a precondition with six precondition clauses. Precondition clauses 1 and 2 require that parameter hour is between HOUR_MIN and HOUR_MAX, precondition clauses 3 and 4 require that parameter minute must be between MINUTE_MIN and MINUTE_MAX and precondition clauses 5 and 6 require that parameter second must be between SECOND_MIN and SECOND_MAX. The customer must fulfill this obligation in order to expect the supplier to create a valid instance of class TimeOfDay.
Another example: The command setHour has a precondition (partial listing):
public class TimeOfDayContract extends TimeOfDay {
...
@Override
public void setHour(int hour) {
if (preCondition()) {
assert hour >= HOUR_MIN : "hour >= HOUR_MIN"; // precondition clause 1
assert hour <= HOUR_MAX : "hour <= HOUR_MAX"; // precondition clause 2
}
if (postCondition()) {
...
}
}
Read as: The command setHour has a precondition with two precondition clauses which require that parameter hour is between HOUR_MIN and HOUR_MAX. The customer must fulfill this obligation in order to expect the supplier to set hour to the recommended value.