|
|
Optimize with a SATA RAID Storage Solution
Range of capacities as low as $1250 per TB. Ideal if you currently rely on servers/disks/JBODs
Page 2 of 4
So far, we have talked about DBC in general. You probably have some idea by now what I am talking about, but if you are new to DBC, things might still be a bit foggy.
In this section, things will become more concrete. iContract, developed by Reto Kamer, adds constructs to Java that allow you to specify the DBC assertions we talked about earlier.
iContract is a preprocessor for Java. To use it, you first process your Java code with iContract, producing a set of decorated Java files. Then you compile the decorated Java code as usual with the Java compiler.
All iContract directives in Java code reside in class and method comments, just like Javadoc directives. In this way, iContract ensures complete backwards-compatibility with existing Java code, and you can always directly compile your Java code without the iContract assertions.
In a typical program lifecycle, you would move your system from a development environment into a test environment, then into a production environment. In the development environment, you would instrument your code with iContract assertions and run it. That way you can catch newly introduced bugs early on. In the test environment you may still want to keep the bulk of the assertions enabled, but you should take them out of performance-critical classes. Sometimes it even makes sense to keep some assertions enabled in a production environment, but only in classes that definitely are in no way critical to your system's performance. iContract allows you to explicitly select the classes that you want to instrument with assertions.
In iContract, you place preconditions in a method header using the @pre directive. Here's an example:
/**
* @pre f >= 0.0
*/
public float sqrt(float f) { ... }
The example precondition ensures that the argument f of function sqrt() is greater than or equal to zero. Clients who use that method are responsible for adhering to that precondition. If they
don't, we as implementors of sqrt() are simply not responsible for the consequences.
The expression after the @pre is a Java Boolean expression.
Postconditions are likewise added to the header comment of the method they belong to. In iContract, the @post directive defines postconditions:
/**
* @pre f >= 0.0
* @post Math.abs((return * return) - f) < 0.001
*/
public float sqrt(float f) { ... }
In our example, we have added a postcondition that ensures that the sqrt() method calculates the square root of f within a specific margin of error (+/- 0.001).
iContract introduces some specific notations for postconditions. First of all, return stands for the return value of the method. At runtime, that will be replaced by the method's return value.
Within postconditions, there often exists a need to differentiate between the value of an argument before execution of the method and afterwards, supported in iContract with the @pre operator. If you append @pre to an expression in a postcondition, it will be evaluated based on the system state before the method executes: