Heron provides support for the technique of Programming with Contracts, which is the usage of contract classes to express and verify design specifications.
A contract class can be used to express and verify the following contractual clauses:
The purpose of a contract is to make sure that the intended design specifications are satisfied and not at conflict with each other. In other words a contract helps identify design flaws.
Heron is flexible with regards to the specific details of how programming with contracts is applied by a programmer. The programmer can use it however they feel fit. What Heron does provide which is severely lacking in many other languages, is a facility which allows the single-point expression of class invariant checking. In C++, for isntance, to check class invariants the only way is through a
A contract in whatever manner desired by the programmer. The technique used by the Heron standard library is to use wrapper classes around implementation classes, which verify the preconditions and postconditiosn using Assert ( or A() ) functions, before calling the inherited class version. An Assert function halts if passed an expression which evaluates to false.
An interesting problem, which can not be easily solved in languages like C++ and Java, is the verification of a class invariant at a single location. A class invariant needs to be tested before and after every function in a class. In Hern this can be done through the use of Aspect Oriented Programming techniques.
A detailed description on how to test class invariants is given in the section on AOP, but in short works in the following manner. Every function in Heron is prepended with an implicit #_before meta-expansion statement, and appended with an implicit #_after. Both _before and _after are user-defined code blocks which are expanded inline. These can be defined in the class to check the invariant condition and to perform custom behaviour.
A simple example of a contract class can be found in the heron.arrays module:
class Array_contract<type Array_T, type T>
{
inherits {
Array_T;
}
public {
SetAt(Int n, T x) {
PreAssert(ValidIndex(n), "invalid index to SetAt");
inherited;
}
GetAt(Int n) : T {
PreAssert(ValidIndex(n), "invalid index to GetAt");
result = inherited;
}
}
private {
ValidIndex(Int n) : Bool {
result = (n >= 0) && (n < Count());
}
}
}
A Heron Array class has a very simple contract, the precondition for SetAt and GetAt functions is that the index parameter must occur within the range of 0 to Count() - 1 inclusive.
Notice that the contract class inherits from its first template parameter. This is done so that an Array_contract can be reused on any class that implements the same functions as Array. This represents one of the major advantages of the Programming with Contracts technique, contract classes are general and reusable.
The verification of the contract,is not always desirable in final or release builds. This is easily accomplished through conditional compilation techniques. The contract class is used with an implementation class conditionally to define a user class as through the following technique:
define Array<type T> :
meta_if
<
APPLY_ARRAY_CONTRACTS,
Array_contract<Array_impl<T>, T>,
Array_impl<T>
>,
T
>;
The value APPLY_ARRAY_CONTRACTS is a meta_bool meta-primitive which has the value of either true or false. If it is true then the meta_if compile-time operation is equivalent to the second parameter, otherwise it is equivalent to the third parameters. In other words, if APPLY_ARRAY_CONTRACTS is true then the type Array refers an Array_impl class wrapped by an Array_contract class, otherwise it simply refers to an Array_impl.
This technique of conditionally applying contracts, allows us to use the same code base for release and debug code, without it being intermingled, as is the case in the traditional method of using assertion statements throughout code. The other advantag is that a contract class can have its own state, which is independant of the rest of the code, allowing for more sophisticated contract verification techniques without interfering with the release code base.