Using Custom Tags with Javadoc and Eclipse

The file taglets.zip contains Java classes that define three custom Javadoc tags:

• @invariant
• @pre
• @post

If you wish to use these tags to document your code, you must do the following when running Javadoc from Eclipse:

1. Download the taglets.zip file and unzip it into a 'taglets' subdirectory in your cs211 directory (i.e. ~/cs211/taglets)

2. Choose Export from the Eclipse File menu and then choose Javadoc

3. Specify the options in the dialog box and then click Next (don't click Finish)

4. Choose a title for your document and then click Next

5. In the Extra Javadoc options textbox, enter the following:
        -taglet PreTaglet -taglet PostTaglet -taglet InvariantTaglet -tagletpath ~/cs211/taglets

6. Click Finish

Check your output to ensure that the documentation corresponding to @invariant, @pre and @post tags has been generated.

Note:  The @invariant tag has been created in such a way that the only place it can be used is to document a type (a class or an interface).

/**
  *@invariant  numPassengers >= 0
  */
public class Flight
{...}

If you attempt to use it anywhere else, an error will be generated.

Similarly, the @pre and @post tags can be used only to document a method.