org.jmlspecs.jml4.rac.runtime
Interface JMLOption

All Known Implementing Classes:

JMLChecker

public interface JMLOption

An interface to provide compile-time and runtime options. The compile-time options chooses the kinds of assertions for which assertion check code be generated, and the runtime options are for reporting and recovering assertion violations. These options are arranged so that runtime subset can be easily determined. That is if the run-time option is ALL but the compile-time option was PRECONDITIONS_ONLY, then at run-time, only PRECONDITIONS can be checked. This validity can be found out by just comparing numerical values.

Version:

$Revision: 1.4 $

Author:

Yoonsik Cheon

Field Summary

static int	ALL Indicates that all assertion check code is generated at compile-time and all are checked at runtime.
static int	NONE Indicates that no assertion check code is generated at compile time, and thus no check at runtime.
static int	PRECONDITIONS_ONLY Indicates that only precondition check code is generated at compile-time, and only precondition check is performed at runtime.

Field Detail

NONE

static final int NONE

Indicates that no assertion check code is generated at compile time, and thus no check at runtime.

See Also:

Constant Field Values

PRECONDITIONS_ONLY

static final int PRECONDITIONS_ONLY

Indicates that only precondition check code is generated at compile-time, and only precondition check is performed at runtime.

See Also:

Constant Field Values

ALL

static final int ALL

Indicates that all assertion check code is generated at compile-time and all are checked at runtime.

See Also:

Constant Field Values