For the specification of the classes, we use JML. JML allows different kinds of syntax for specifications, and also allows it to be in seperate files. We won't :)
Files
All specifications will be written in the .java files. That way it is easier to keep things consistent, and it's also easier to use. An exception to this may be the specification of java classes. Since the specification of the Java API is only informal at best, it is very hard to use. If the need arrises for more formal specifications, they kan be put in .jml files, which we'll try to sync with the JML project.
Specification format
The general specification format looks like this:
/**
* Informal description of the method
*
* @param name of a parameter
* description of the parameter
* ...
*/
/*@
@ [also] public behavior
@
@ pre precondition;
@ ...
@ pre precondition;
@
@ post postcondition;
@ ...
@ post postcondition;
@
@ excep (name of exception) condition under which it may be thrown;
@ ...
@ excep (name of exception) condition under which it may be thrown;
@*/
The "also" should only be present when overriding a method from a superclass, in which case it will weaken the preconditions, and strengthen the postconditions.
Always use "public" behavior. Since we don't allow non-specified exception to be thrown, normal_behavior doesn't bring anything extra. We (I) don't find The exceptional_behavior clause very useful since it says that an exception _must_ be thrown when it's condition is true. We think it is wrong for software to depend on that. If no exception is thrown, the possible problem is dealt with, no need for throwing an exception.
Overriding a method without changing its contract
If you override or implement a method of a superclass without changing its contract, add the following specification. Then others will know that the contract is not modified. Otherwise they might think there is no specification yet.
/**
* @see superclass
*/
|
