Appendix 1: @assert.
-------------------

   The syntax for the @assert tag is:

    AssertStmt
        : @assert BooleanExpression
        | @assert '(' BooleanExpression ')'
        | @assert '(' BooleanExpression , MessageExpression ')'

   the MessageExpression can be of any type.

   For example:

    /** @assert value > 0 */
    /** @assert (value > 0) */
    /** @assert (value > 0, "value should be positive */
    /** @assert (value > 0, value) */


   The @assert tags should appear in Javadoc comments inside the method
bodies. If the classes are compiled with 'dbc_javac' and the preferences
Instrument.InstrumentAssertConditions is true, then the @assert boolean
expression will be evaluated. If the the expression evaluates to false
then the one or more of the following actions take place:

a) An error message is reported in the Jcontract Monitor.

b) A runtime exception (jcontract.AssertException) is thrown.

c) The program exits by invoking System.exit (1).

   See section 3 in "spec10.txt" for more information about how to select
the actions that take place. The default action is to report and error
and continue program execution.


Appendix 2: @verbose.
--------------------

   The syntax for the @verbose tag is:

    VerboseStmt
        : @verbose MessageExpression
        | @verbose '(' MessageExpression ')'

   For example:

    /** @verbose "process starts" */
    /** @verbose ("process ends") */
    /** @verbose 26.7 */


   The @verbose tags should appear in Javadoc comments inside the method
bodies. If the classes are compiled with 'dbc_javac' and the preferences
Instrument.InstrumentVerboseConditions is true, then the classes are 
instrumented with the verbose expression.

   By default all verbose statements are inactive, once they are activated,
they print the MessageExpression to System.out.
   The @verbose statements can be separately activated for each class.
The @verbose statements for a class are active if the system property
jcontract.verbose.CLASSNAME is set to the value ON. Where CLASSNAME is the
name of the class without the package part. For example to activate the
verbose statements in class pkg.DataDictionary on Windows use:

$ java -Djcontract.verbose.DataDictionary=ON ...

   Note that the MessageExpression in a verbose statement is not evaluated
if the verbose statement is inactive.


Appendix 3: @throws/@exception.
------------------------------

   Those are the standard @throws and @exception tags found in javadoc
and are used to document that the method throws a given exception.
@throws and @exception are synonimous, in the following text we will use
@throws to represent both of them.

   The syntax for the @throws tag is:

    ThrowsContract
        : @throws ExceptionName Text

    Example:

        /** @throws NegativeArraySizeException if size is negative */

   When a method throws an exception, the Jcontract Runtime Handler
will call 'documentedExceptionThrown (Throwable t)' if that exception
is documented with a @throws tag.
   Note that the Runtime Monitors provided with Jcontract don't take
any action when 'documentedExceptionThrown' is called. You can nevertheless
take a specific action by defining a user defined Runtime Handler.

   Jtest uses the @throws tags to suppress exceptions that are documented
with it. For that, the classes need to have been instrumented with the 
intrument @throws condition preference set to true.