CSE331 Autumn 2011
Software Design and Implementation


 Using Javadoc to generate specifications for 331

The Java Development Kit includes Javadoc, a tool that produces specifications from source code annotated with special comments. Javadoc recognizes these comments through the use of "tags", which start with an at-sign (@).

Configuring Javadoc

[Note: This is only partial instructions -- more soon on how to get the tag extensions below, etc.]

To generate Javadoc for your own code (or for code we provide), you have to configure Eclipse by right-clicking the project name and choosing Properties. Then select Javadoc Location and enter (directly or using the browse button) file:/C:/Users/yourUserID/workspace/yourProjectName/doc/

Running Javadoc with ant

You have to run Javadoc to generate the (web-readable) documents from the (annotated) Java source code:s

  1. Right-click on build.xml in Package Explorer
  2. Select Run Ant...
  3. Toggle the checkboxes so that javadoc is the only box selected
  4. Click Run
  5. After you see a BUILD SUCCESSFUL message in the console at the bottom of the screen, right-click on doc in Package Explorer and hit Refresh
  6. Open the < doc>doc< folder and double-click index.html

When you look at your results, you may find that you need to add line (<br>) or paragraph breaks (<p>) to your javadoc comments for readability. Also, if you omit certain tags or have them out-of-order, subsequent text may fail to appear in the output. Finally, since much of the text of javadoc comments is inserted in a HTML document, you must be careful with text that can be interpreted as HTML markup, such as the less-than  (<) and greater-than (>) characters. (For instance, if you include "<x>" in a tagged comment it will be interpreted as HTML.  You would probably want "&lt;x&gt;" instead, using HTML escape characters.)

CSE331 @tag Extensions

We have extended the javadoc program to recognize additional CSE331 tags. These additional tags declare specification fields for classes and requires, modifies, and effects clauses for methods. These tags must appear after all non-tag comments for classes and methods (as well as after any standard Javadoc tags).

Our basic extended tags belong in the specification for a method; they define the method's preconditions, postconditions, and side effects.

@requires X Declares X to be a precondition for the method
@modifies Y

Declares that nothing besides Y will be modified by the method (as long as any preconditions hold when the method is invoked)
@effects Z Declares that Z will hold at exit from the method (as long as any preconditions hold when the method is invoked)

Some additional extended tags belong in the overview for a class, and are used to formally define what a given Abstract Data Type represents. (These will be introduced during the two ADT lectures.)

@specfield name : T    // text
 Indicates that name is a abstract specification field of type T for the class, with text as an optional comment
@derivedfield name : T    // text
 Same as specfield, also adding the property "derived" to the output information

Derived fields can be viewed as functions on pre-existing state; thus if a class had @specfield n : integer we could define a derived field:

@derivedfield pos : boolean // pos = true iff n > 0

Derived fields do not hold any information that could not be already calculated from the already existing state in the object. Thus, specfields introduce new state variables and derivedfields introduce functions on those state variables. (Derived fields are not strictly needed in specifications, but they may reduce complexity and redundancy.)