public static enum TextualJMLSpecCase.Clause extends java.lang.Enum<TextualJMLSpecCase.Clause>
Enum Constant and Description |
---|
ABBREVIATION |
BREAKS |
CONTINUES |
DECREASES |
DEPENDS |
DIVERGES |
INFORMATION_FLOW |
MEASURED_BY |
RETURNS |
SIGNALS |
SIGNALS_ONLY |
WORKING_SPACE |
Modifier and Type | Method and Description |
---|---|
static TextualJMLSpecCase.Clause |
valueOf(java.lang.String name)
Returns the enum constant of this type with the specified name.
|
static TextualJMLSpecCase.Clause[] |
values()
Returns an array containing the constants of this enum type, in
the order they are declared.
|
public static final TextualJMLSpecCase.Clause MEASURED_BY
public static final TextualJMLSpecCase.Clause WORKING_SPACE
public static final TextualJMLSpecCase.Clause SIGNALS
public static final TextualJMLSpecCase.Clause DIVERGES
public static final TextualJMLSpecCase.Clause DEPENDS
public static final TextualJMLSpecCase.Clause BREAKS
public static final TextualJMLSpecCase.Clause CONTINUES
public static final TextualJMLSpecCase.Clause RETURNS
public static final TextualJMLSpecCase.Clause DECREASES
public static final TextualJMLSpecCase.Clause SIGNALS_ONLY
public static final TextualJMLSpecCase.Clause ABBREVIATION
public static final TextualJMLSpecCase.Clause INFORMATION_FLOW
public static TextualJMLSpecCase.Clause[] values()
for (TextualJMLSpecCase.Clause c : TextualJMLSpecCase.Clause.values()) System.out.println(c);
public static TextualJMLSpecCase.Clause valueOf(java.lang.String name)
name
- the name of the enum constant to be returned.java.lang.IllegalArgumentException
- if this enum type has no constant with the specified namejava.lang.NullPointerException
- if the argument is nullCopyright © 2003-2019 The KeY-Project.