JML

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

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.


JML

JML is Copyright (C) 1998-2002 by Iowa State University and is distributed under the GNU General Public License as published by the Free Software Foundation; either version 2 of the License, or (at your option) any later version. This release depends on code from the MultiJava project and is based in part on the Kopi project Copyright (C) 1990-99 DMS Decision Management Systems Ges.m.b.H.