The Design by Contract Specification Language

This document describes the syntax and semantics for the Design by Contract (DbC) specification supported by Jtest and Jcontract.

The Design by Contract contracts are expressed with Java code embedded in Javadoc comments in the .java source file.

This document is divided into the following sections:

• Tags Used for Design by Contract
• Contract Syntax
• Contract Semantics
• Contract Inheritance
• Coding Conventions

Tags Used for Design by Contract

The reserved Javadoc tags for DbC are:

• @invariant: Specifies class invariant condition.
• @pre: Specifies method precondition.
• @post: Specifies method postcondition.
• @concurrency: Specifies the method concurrency.

Other tags supported by Jtest and Jcontract include:

• @throws/@exception: Used to document exceptions.
• @assert: Used to add assertions in the method bodies.
• @verbose: Used to add verbose statements to the method bodies. (Not currently used by Jtest)

The following subsections describe each DbC tag in detail.

@pre

Description

Pre-conditions check that the client calls the method correctly.

Point of execution

Right before calling the method.

Scope

Can access anything accessible from the method scope except local variables. For example, it can access method arguments, and methods/fields of the class.

@post

Description

Post-conditions check whether the method works correctly.

Sometimes when a post-condition fails it means that the method was not actually supposed to accept the arguments that were passed to it. The fix in this case is to strengthen the precondition.

Point of execution

Right after the method returns successfully. Note that if the method throws an exception the @post contract is not executed.

Scope

Same as @pre, plus it can access "$result" and "$pre (type, expression)".

Accessibility

Same as @pre.

@invariant

Description

Class invariants are contracts that the objects of the class should always satisfy.

Point of execution

Same as @pre/@post: invariant checked before checking the precondition and after checking the postcondition.

Done for every non-static, non-private method entry and exit and for every non-private constructor exit.

If a constructor throws an exception, its @invariant contract is not executed.

Not done for "finalize ()".

When inner class methods are executed, the invariants of the outer classes are not checked.

Scope

Class scope, can access anything a method in the class can access, except local variables.

Accessibility

Same as @pre/@post.

@concurrency

Description

The @concurrency tag specifies how the method can be called by multiple threads. Its possible values are:

• Concurrent: The method can be called simultaneously by different threads (i.e., the method is multi-thread safe). Note that this is the default mode for Java methods.
• Guarded: The method can be called simultaneously by different threads, but only one will execute it in turn, while the other threads will wait for the executing one to finish. In other words, it specifies that the method is synchronized. Jcontract will only report a compile-time error if a method is declared as "guarded" but is not declared as "synchronized".
• Sequential: The method can only by executed by one thread at once and it is not declared synchronized. It is thus the responsibility of the callers to ensure that no simultaneous calls to that method occur. For methods with this concurrency contract, Jcontract will generate code to check if they are being executed by more than one thread at once. An error will be reported at runtime if the contract is violated.

Point of execution

Right before calling the method.

@throws/@exception

These are the standard @throws and @exception tags found in Javadoc; they are used to document that the method throws a given exception. @throws and @exception are synonymous. In this entry, we use @throws to represent both tags.

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 suppresses exceptions that are documented with the @throws tag as long as the the classes were instrumented with the instrument @throws condition preference set to "true".

@assert

Syntax

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 Instrument.InstrumentAssertConditions preference is true/enabled, then the @assert boolean expression will be evaluated. If the expression evaluates to false, then one or more of the following actions take place:

• An error message is reported in Jtest's Design by Contract> @assert Results panel/Errors Found panel branch or in the Jcontract Monitor.
• A runtime exception (jcontract.AssertException) is thrown.
• The program exits by invoking System.exit (1).

See Contract Semantics for more information about how to select the actions that take place. The default action is to report an error and continue program execution.

@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 Instrument.InstrumentVerboseConditions preferences is true/enabled, 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.

Contract Syntax

The general syntax for a contract is:

 
         DbcContract:
               DbcTag DbcCode
             | @concurrency { concurrent | guarded | sequential }
 

where

 
         DbcTag:
               @invariant
             | @pre
             | @post
 
         DbcCode:
               BooleanExpression
             | '(' BooleanExpression ')'
             | '(' BooleanExpression ',' MessageExpression ')'
             | CodeBlock
             | $none
 
         MessageExpression:
               Expression
 

Any Java code can be used in the DbcCode with the following restriction: the code should not have side effects (i.e., it should not have assignments or invocation of methods with side-effects).

The following extensions to Java (DbC keywords) are allowed in the contract code:

• $result: Used in a @post contract, evaluates to the return value of the method.
• $pre: Used in a @post contract to refer to the value of an expression at @pre-time. The syntax to use it is:
  $pre (ExpressionType, Expression).
Note: The full "$pre (...)" expression should not extend over multiple lines.
• $assert: Can be used in DbcCode CodeBlocks to specify the contract conditions.
  The syntax to use it is:
  $assert (BooleanExpression)
or
  $assert (BooleanExpression , MessageExpression)
• $none: Used to specify there is no contract.

Notes

• The @pre, @post and @concurrent tags apply to the method that follows in the source file.
• The MessageExpression is optional and will be used to identify the contract in the error messages or contract violation exceptions thrown. The MessageExpression can be of any type. If it is a reference type it will be converted to a String using the "toString ()" method. If it is of primitive type it will first be wrapped into an object.
• There can be multiple conditions of the same kind for a given method. If there are multiple conditions, all conditions are checked. The conditions are ANDed together into one virtual condition. For example it is equivalent (and encouraged for clarity) to have multiple @pre conditions instead of a single big @pre condition.

Examples

 
     /**
       * @pre {
       *     for (int i = 0; i < array.length; i++)
       *         $assert (array [i] != null, "array elements
are non-null"); 
       * }
       */
 
     public void set (int[] array) {...}
 
     /** @post $result == ($pre (int, arg) + 1) */
 
     public int inc (arg) {...}
 
 /** @invariant size () >= 0 */
 
     class Stack {...}
 
     /**
      * @concurrency sequential
      * @pre (value > 0, "value positive:" + value)
      */
 
     void update (int value) {...}

Contract Semantics

The contracts are specified in comments and will not have any effect if compiling or executing in a non DbC enhanced environment.

In a DbC-enhanced environment, the contracts are executed/checked when methods of a class with DbC contracts are invoked.

A contract fails if any of these conditions occur:

• The "BooleanExpression" evaluates to "false."
• An "$assert (BooleanExpression)" is called in a "CodeBlock" with an argument that evaluates to "false."
• The method is called in a way that violates its @concurrency contract.

If a contract fails, the Runtime Handler for the class is notified of the contract violation. Jcontract provides several Runtime Handlers; the default one uses a GUI Monitor that shows program progress and contract violations. You can also write your own Runtime Handlers.

With the Monitor Runtime Handlers provided by Jcontract, program execution continues as if nothing has happened when a contract is violated. For example, if a @pre contract is violated, the method will still be executed.

This option makes the DbC-enabled and non DbC-enabled versions of the program work in exactly the same way. The only difference is that in the DbC-enabled version, the contract violations are reported to the current Jcontract Monitor.

Note: Contract evaluation is not nested; when a contract calls another method, the contracts in the other method are not executed.

Contract Inheritance

Contracts are inherited. If the derived class or overriding method doesn't define a contract, it inherits that of the super class or interface. Note that a contract of $none implies that the super contract is applied.

If an overriding method does define a contract then it can only:

• Weaken the precondition: Because it should at least accept the same input as the parent, but it can also accept more.
• Strengthen the postcondition: Because it should at least do as much as the parent one, but it can also do more.

To enforce this:

• When checking the @pre condition, the precondition contract is assumed to succeed if any of the @pre conditions of the chain of overridden methods succeeds (i.e., the preconditions are ORed).
• When checking the @post condition, the postcondition contract is assumed to succeed if all the @post conditions of the chain of overridden methods succeed (i.e., the postconditions are ANDed).

Note: If there are multiple @pre conditions for a given method, the preconditions are ANDed together into one virtual @pre condition and then ORed with the virtual @pre conditions for the other methods in the chain of overridden methods.

For @invariant conditions, the same logic as for @post applies.

@concurrency contracts are also inherited. If the overriding method doesn't have an @concurrency contract, it inherits that of the parent. If it has an inheritance contract, it can only weaken it (as it does for @pre conditions). For example, if the parent has a "sequential" @concurrency, the overriding method can have a "guarded" or "concurrent" @concurrency.

Coding Conventions

When using Design by Contract in Java, the following coding conventions are recommended:

• Place all the @invariant conditions in the class Javadoc comment with the Javadoc comment appearing immediately before the class definition.
• Javadoc comments with the @invariant tag should appear before the class definition.
• All public and protected methods should have a contract. All package-private and private methods should also have a contract.
• If a method has a DbC tag, it should have a complete contract. This means that if you have both a precondition and a postcondition, you should use "DbcTag $none" to specify that a method doesn't have any condition for that tag.
• No public class field should participate in an @invariant clause. Because any client can modify such a field arbitrarily, there is no way for the class to ensure any invariant on it.
• The code contracts should only access members visible from the interface. For example, the code in a method's @pre condition should only access members that are accessible from any client that could use the method. In other words, the contract of a public method should only use public members from the method's class.

Note: Jcontract does not currently enforce these conventions.

Related Topics

Using Design by Contract With Jtest

About Design by Contract

Performing Black-Box Testing

Customizing White-Box Testing

Testing A Class - Two Simple Examples