The file taglets.zip contains Java classes that define three custom Javadoc tags:
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.