org.jmlspecs.jml4.esc.gc.lang
Class KindOfAssertion

java.lang.Object
  org.jmlspecs.jml4.esc.gc.lang.KindOfAssertion

public class KindOfAssertion
extends java.lang.Object

Provides an enumeration of the kinds of assertions that can be thrown in JML code.

Field Summary

static KindOfAssertion	ASSERT
java.lang.String	description
static KindOfAssertion	INVARIANT
static KindOfAssertion	LOOP_INVAR
static KindOfAssertion	LOOP_INVAR_PRE
static KindOfAssertion	LOOP_VAR
static KindOfAssertion	POST
static KindOfAssertion	PRE
static KindOfAssertion	UNKNOWN

Method Summary

static KindOfAssertion[]	all()
static KindOfAssertion	fromString(java.lang.String labelName)
static boolean	matches(java.lang.String label)
java.lang.String	toString()

Methods inherited from class java.lang.Object

equals, getClass, hashCode, notify, notifyAll, wait, wait, wait

Field Detail

ASSERT

public static final KindOfAssertion ASSERT

PRE

public static final KindOfAssertion PRE

POST

public static final KindOfAssertion POST

LOOP_VAR

public static final KindOfAssertion LOOP_VAR

LOOP_INVAR_PRE

public static final KindOfAssertion LOOP_INVAR_PRE

LOOP_INVAR

public static final KindOfAssertion LOOP_INVAR

INVARIANT

public static final KindOfAssertion INVARIANT

UNKNOWN

public static final KindOfAssertion UNKNOWN

description

public final java.lang.String description

Method Detail

toString

public java.lang.String toString()

Overrides:

toString in class java.lang.Object

all

public static KindOfAssertion[] all()

matches

public static boolean matches(java.lang.String label)

fromString

public static KindOfAssertion fromString(java.lang.String labelName)