|
|
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 3 of 5
You could also add assertions in Java by using tags. The documentation tool javadoc supports a variety of predefined tags. However, you can define additional tags that javadoc and its Doclet architecture can process.
In this article, I introduce three new tags to support assertions and DBC in Java. One for each assertion type:
@pre for preconditions
@post for postconditions
@invariant for invariants
The rules for these new tags are as follows:
logical_statement, except when you use keywords $implies and $return (described later):
@pre logical_statement [, wait] @post logical_statement @invariant logical_statement
logical_statement uses regular Java syntax. You use the text inside the logical_statement as-is (again, except when using $implies and $return); in other words, it is not further parsed. Not supporting a separate DBC syntax was a clear design goal of the DBCProxy
framework.
obj(). A primary object is the object for which the assertion is being made. For example, if a primary object's interface has a
method called count(), then @pre obj().count() >= 0 is a valid precondition. To make this a valid postcondition or invariant, simply replace @pre with @post or @invariant.
$implies, which has the following syntax:
@pre logical_statement $implies logical_statement @post logical_statement $implies logical_statement @invariant logical_statement $implies logical_statement
In the following sections, I'll present rules and examples for the three assertion types, @pre, @post, and @invariant, in more detail.
You declare preconditions in a method's special comments section, as described above. Preconditions can assert arguments and
call methods on the primary object. In the following example, the precondition asserts the object x passed to the put() method must not equal null:
/** * @pre x != null */ public void put(Object x);
The next example asserts the primary object must not be empty and calls the method empty() on the primary object as part of the precondition declaration:
/** * @pre !obj().empty() */ public Object item(Object x);
I describe the wait keyword, which optionally follows the logical_statement, in the section "Separate Objects."
You also declare postconditions in the method's special comments section. A postcondition has the same capabilities as a precondition but possesses two additional features:
old(). This example uses old() and asserts the method count() will increment by one, as a result of executing the put() method:
/** * @post obj().count() == old().count() + 1 */ public void put(Object x);
$return. This example uses $return and asserts the item() method will never return null:
/** * @post $return != null */ public Object item();
You declare invariants in the class/interface special comments. Invariants can only call methods on the primary object. This
example asserts the method count() will always return a value greater than or equal to zero: