public static enum OriginTermLabel.SpecType extends java.lang.Enum<OriginTermLabel.SpecType>
SpecType
is any type of JML specification which gets translated into JavaDL.OriginTermLabel.Origin
Enum Constant and Description |
---|
ACCESSIBLE
accessible
|
ASSERT
assert
|
ASSIGNABLE
assignable
|
ASSUME
assume
|
BREAKS
breaks
|
CONTINUES
continues
|
DECREASES
decreases
|
ENSURES
ensures
|
ENSURES_FREE
ensures_free
|
INVARIANT
invariant
|
LOOP_INVARIANT
loop_invariant
|
LOOP_INVARIANT_FREE
loop_invariant_free
|
MEASURED_BY
measured_by
|
NONE
None.
|
REQUIRES
requires
|
REQUIRES_FREE
requires_free
|
RETURNS
returns
|
SIGNALS
signals
|
SIGNALS_ONLY
signals_only
|
USER_INTERACTION
Interaction.
|
Modifier and Type | Method and Description |
---|---|
java.lang.String |
toString() |
static OriginTermLabel.SpecType |
valueOf(java.lang.String name)
Returns the enum constant of this type with the specified name.
|
static OriginTermLabel.SpecType[] |
values()
Returns an array containing the constants of this enum type, in
the order they are declared.
|
public static final OriginTermLabel.SpecType ACCESSIBLE
public static final OriginTermLabel.SpecType ASSERT
public static final OriginTermLabel.SpecType ASSIGNABLE
public static final OriginTermLabel.SpecType ASSUME
public static final OriginTermLabel.SpecType DECREASES
public static final OriginTermLabel.SpecType MEASURED_BY
public static final OriginTermLabel.SpecType INVARIANT
public static final OriginTermLabel.SpecType LOOP_INVARIANT
public static final OriginTermLabel.SpecType LOOP_INVARIANT_FREE
public static final OriginTermLabel.SpecType REQUIRES
public static final OriginTermLabel.SpecType REQUIRES_FREE
public static final OriginTermLabel.SpecType ENSURES
public static final OriginTermLabel.SpecType ENSURES_FREE
public static final OriginTermLabel.SpecType SIGNALS
public static final OriginTermLabel.SpecType SIGNALS_ONLY
public static final OriginTermLabel.SpecType BREAKS
public static final OriginTermLabel.SpecType CONTINUES
public static final OriginTermLabel.SpecType RETURNS
public static final OriginTermLabel.SpecType USER_INTERACTION
public static final OriginTermLabel.SpecType NONE
public static OriginTermLabel.SpecType[] values()
for (OriginTermLabel.SpecType c : OriginTermLabel.SpecType.values()) System.out.println(c);
public static OriginTermLabel.SpecType 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 nullpublic java.lang.String toString()
toString
in class java.lang.Enum<OriginTermLabel.SpecType>
Copyright © 2003-2019 The KeY-Project.