org.jmlspecs.jmlrac.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

Class Specifications

Specifications inherited from class Object

represents objectState <- org.jmlspecs.lang.JMLDataGroup.IT; public represents _getClass <- \typeof(this);

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

public static final int NONE

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

PRECONDITIONS_ONLY

public static final int PRECONDITIONS_ONLY

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

ALL

public static final int ALL

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