Contents:
At the beginning of the specification for your class, give a summary of its main goal--what object it's meant to represent, and why someone would generally look to use it.
A specfield is a reference to an abstract field of a data type. For example, consider an abstract data type that represents a bank account. Some of the fields, or properties, of the bank account that we would want to keep track of could be the name of the person who owns the account, the amount of money in the account, and the transaction history for the account. We would represent this in our spec as follows:
/** * <Class Overview Goes Here> * * @specfield name : string // name of account owner * @specfield balance : integer // balance of account, in US cents * @specfield transactions : sequence // history of transactions, most recent listed first */
balance as a
Integer;
however, a different Java programmer might use
Long
to allow more flexibility (it can hold amounts larger than $21
million). Representing the types of the specfields in an abstract way
allows for either implementation.size, head and rest.
The specfields however of this class would just be elements, the sequence of objects in the chain.
The @specfield tag is not part of Sun's standard set of
Javadoc tags; however, they are recognized by our CSE 331 doclet.
Here's an example method specification:
public interface Account {
/**
* @requires this.balance is at least $10
*
* @modifies this.balance, this.transactions, a.balance, a.transactions
*
* @effects decreases this.balance by $10,
* increases a.balance by $10,
* adds a transaction to both this.transactions and a.transactions
*
* @throws NotEnoughMoneyException if this.balance is less than $10.
* No transaction occurs if this exception is thrown.
*/
public void transferTenBucksTo(Account a);
}
Let's explore this notation in greater detail:
In CSE 331, we use the following tags in our method specifications.
Note that @throws and @return tags are also
of the Sun Javadoc tags.
| Precondition | @requires |
determines the conditions under which the method may be invoked |
| Frame Condition | @modifies |
a list of specfields identifying what might be modified by the method |
| Postcondition | @return |
describes the value that gets returned, if any |
@throws |
each of these lists an exception and the conditions under which it will be thrown | |
@effects |
any side effects that may result from invoking the method |
You may wonder why we have separate the @modifies and @effects
tags since they seem to contain the same information.
One advantage that the @modifies tag provides is that it allows us to
write software that can reason about our program by parsing the contents of the
@modifies tag to determine what could be affected by invoking the method.
Some programming languages, such as Eiffel,
explore this idea in more detail.
You may have trouble making your specification fit into these five tags. If you find yourself in this situation, do not hesitate to add text before these tags in your specification. It is more important that your specification be complete rather than it fit perfectly into our documentation scheme.
This does not mean that you should ignore these tags and write your specifications completely in prose. Using this scheme allows clients of your specification to extract information from it quickly and easily.
A strong specification is one that is tolerant on inputs and
demanding on outputs whereas a weak specification is one that
is demanding on inputs and weak on outputs.
In CSE 331, we want to produce strong specifications as they are more useful
for the clients of our specifications.
For example, consider the following three specifications of double sqrt(double x):
| A | @requires x ≥ 0 |
|---|---|
| B | @return y such that |y^2 - x| ≤ 1 |
| C | @requires x ≥ 0 |
We can make the following comparisons between specifications:
These comparisons are important because a module with a stronger specification can always replace a module with a weaker specification. However, one cannot generalize that strong or weak specifications are better: strong specifications are bad where weak ones should be used; weak specifications are bad where strong ones should be used.
For external routines, strong specifications tend to be more appropriate. However, for routines that are internal to some module (whether that module is a class, a package, or an entire system), weak specifications may be more appropriate because specifying full behavior would be counterproductive.
Even if the specifications are well-written and preconditions for a
method are spelled out, there are no guarantees that clients will
follow their side of the contract and a program will necessarily
observe good inputs. You will need decide how to handle malformed
inputs that violate the
requires clause. Although a program is justified in doing
whatever it likes if the requires clause is not
satisfied, having a program behave in a completely random and
unspecified manner is not a particularly graceful way to handle
malformed inputs. One advantage of handling malformed/non-compliant
inputs gracefully is that it often makes debugging easier.
Furthermore, you may have some cases for some methods that are allowed by the requires clause of the method, for which the method can nevertheless not complete normally. The specification for the method must then determine the behavior of the method for these cases.
In general, unless it is too expensive to do so (one such example
is the Arrays.binarySearch, which expects its input to be
sorted), you should try to check if the requires clause is
satisfied. If you should determine that the inputs violate
the requires clause, there are two reasonable ways to
indicate errant or exceptional behavior:
Returning a special value is often done because it is fast and convenient. It is fast because it does not require the overhead associated with creating a new Exception object and then throwing and catching it. Further, it is convenient because it does not force the client to create a try/catch block. This is acceptable practice when there is an acceptable special value available to return (such as null or -1), and that the error is not so drastic that you need to call the programmer's attention to it (such as when List.indexOf(Object o) fails to find o).
Sometimes throwing an exception is necessary to indicate a failure because there may be no special value available to return. For example, consider the following method:
public int max(a, b); //returns the max value of a or b
Though it is hard to imagine how this method could fail, it could not return a special int even if it did because every int is a potentially valid return value for max().
However, the lack of a special value is rarely the main motivation for deciding to throw an exception. Often, it is used to call the programmer's attention to an unexpected failure and to give him some information to help him recover from it. An Exception is an object just like any other, so it can have its own fields that can be used to store information about the failure that the programmer can use to help him figure out how to proceed. For a deeper discussion of deciding when to throw exceptions, please read Effective Java.
All this talk about specifications is about what an abstract data type does and how it's used. You eventually will have to get around to coding the thing, however. Since the specfields aren't even guaranteed to correspond directly to fields of the implementation, it would be nice to have a way to formally map the concrete value of your concrete Java fields to values of your abstract specfields. This function is called the abstraction function.
Each abstract data type you write (especially those of any complexity) should have an abstraction function written in its comments. Since the abstraction function concerns the specific implementation, it is not considered to be part of the public specification for the class, and so it should not go in javadoc-style (/** ... */) comments, but in standard (// or /* .. */) style comments. The abstraction function works as a formal description of the connection between a specification and its implementation.
For example, the abstraction function
for BallContainer in ps0 could have been:
/* this represents a container containing all Balls b such that contents.contains(b) */
Note that this maps a concrete representation (an instance of HashSet, and a method call on that instance) to the idea the concrete representation represents (a container of balls, containing specific balls).
The abstraction function defines a mapping from concrete representation to abstract value for a class. However, it often says little (or only implicitly) what allowed concrete representations actually have meaning. The domain of the abstraction function is defined by the representation invariant of an implementation of an abstract data type. Like the abstraction function, the representation invariant is not part of the public specification, so you should put it in your source code in standard (not javadoc) comments.
The representation invariant is expressed in the form of a function that takes in a given configuration of your concrete representation, and outputs whether this configuration is a legal, meaningful value for the type to hold. For example, if you have a ComplexNumber implementation that stores both rectangular coordinates and polar ones, you might give the invariant that the real part must be equal to the radius times to cosine of the angle, and the imaginary part must be equal to the radius times the sine of the angle. If these things are not true, the class is not likely to work properly.
In a sense, the representation invariant is similar to an implicit
addition to the requires of every public method.
However, since it is the implementor of a class who is responsible for
ensuring that it remains always true, and not the client's
responsibility, it is not part of the public requires
clause in the specification.
You may express the representation invariant in whatever way you feel you can be most precise and comprehensive . Many people like specifying representation invariants in math-like notation, and many others prefer prose, or a mix.
For every class you implement, we recommend (okay, usually require)
you also implement a private checkRep method which tests
your representation invariant, and throws a RuntimeError
if it is not met. Calling this method at the beginning and end of
every public method will ensure quick detection for any bugs in your
code that break your representation invariant. If this method takes
too long to complete, you can comment out the calls when using your
code in non-debugging contexts, but if checkRep is
efficient, we recommend you leave it in to catch any bugs that might
have been missed by your test suites.