A postcondition states what a method ensures if it has been called by fulfilling its precondition. If the postcondition is violated although the precondition holds, the method (the supplier) has broken the contract (implementation error). In other words a postcondition is a right to the customer and an obligation to the supplier.
The general structure of a postcondition in C4J is like that:
if (postCondition()) {
postcondition clause 1
postcondition clause 2
...
postcondition clause n
}
A postcondition 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 postconditions. 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()) {
...
}
if (postCondition()) {
assert target.getHour() == hour : "hour set"; // postcondition clause 1
assert target.getMinute() == minute : "minute set"; // postcondition clause 2
assert target.getSecond() == second : "second set"; // postcondition clause 3
}
}
Read as: The overloaden constructor of class TimeOfDay has a postcondition with three postcondition clauses. Postcondition clauses 1 up to 6 ensure that if the precondition holds the parameters hour, minute and second will be successfully set when the constructor has finished. The supplier must fulfill this obligation if the customer has fulfilled his part of the contract, the precondition.
Another example: The command setHour has a postcondition (partial listing):
public class TimeOfDayContract extends TimeOfDay {
...
@Override
public void setHour(int hour) {
if (preCondition()) {
...
}
if (postCondition()) {
assert target.getHour() == hour : "hour set"; // postcondition clause 1
assert unchanged(target.getMinute()) : "minute unchanged"; // postcondition clause 2
assert unchanged(target.getSecond()) : "second unchanged"; // postcondition clause 3
}
}
Read as: The command setHour has a postcondition with three postcondition clauses. Postcondition clause 1 ensures that if the precondition holds the value of getHour will be successfully changed to hour whereas postcondition 2 and 3 ensure the value of getMinute and getSecond will not have changed at all after the execution of setHour. The supplier must fulfill this obligation if the customer has fulfilled his part of the contract, the precondition.