BasicSnippetData.Key (KeY API Documentation)

java.lang.Object
- java.lang.Enum<BasicSnippetData.Key>
- - de.uka.ilkd.key.informationflow.po.snippet.BasicSnippetData.Key

All Implemented Interfaces:

java.io.Serializable, java.lang.Comparable<BasicSnippetData.Key>

Enclosing class:

BasicSnippetData
```
static enum BasicSnippetData.Key
extends java.lang.Enum<BasicSnippetData.Key>
```
Keys to access the unified contract content.

Enum Constant Summary

Enum Constants
Enum Constant and Description
`BLOCK_SELF` Self term of the transformed block contract
`BLOCK_VARS` Variables originally used during parsing.
`DEPENDENS`
`EXECUTION_CONTEXT`
`FOR_CLASS` Returns the KeYJavaType representing the class/interface to which the specification element belongs.
`INF_FLOW_SPECS`
`LABELS`
`LOOP_INVARIANT`
`LOOP_INVARIANT_TERM`
`MEASURED_BY`
`MODALITY`
`MODIFIES`
`POSTCONDITION`
`PRECONDITION`
`TARGET_BLOCK` Returns the contracted block.
`TARGET_METHOD` Returns the contracted function symbol.

Field Summary

Fields
Modifier and Type Field and Description

private java.lang.Class<?> type

Fields
Modifier and Type	Field and Description
`private java.lang.Class<?>`	`type`

Method Summary

All Methods Static Methods Instance Methods Concrete Methods
Modifier and Type	Method and Description
`java.lang.Class<?>`	`getType()`
`static BasicSnippetData.Key`	`valueOf(java.lang.String name)` Returns the enum constant of this type with the specified name.
`static BasicSnippetData.Key[]`	`values()` Returns an array containing the constants of this enum type, in the order they are declared.

Methods inherited from class java.lang.Enum
clone, compareTo, equals, finalize, getDeclaringClass, hashCode, name, ordinal, toString, valueOf

Methods inherited from class java.lang.Object
getClass, notify, notifyAll, wait, wait, wait

- Enum Constant Detail
  - FOR_CLASS
```
public static final BasicSnippetData.Key FOR_CLASS
```
    Returns the KeYJavaType representing the class/interface to which the specification element belongs.
  - TARGET_METHOD
```
public static final BasicSnippetData.Key TARGET_METHOD
```
    Returns the contracted function symbol.
  - TARGET_BLOCK
```
public static final BasicSnippetData.Key TARGET_BLOCK
```
    Returns the contracted block.
  - PRECONDITION
```
public static final BasicSnippetData.Key PRECONDITION
```
  - POSTCONDITION
```
public static final BasicSnippetData.Key POSTCONDITION
```
  - LOOP_INVARIANT
```
public static final BasicSnippetData.Key LOOP_INVARIANT
```
  - LOOP_INVARIANT_TERM
```
public static final BasicSnippetData.Key LOOP_INVARIANT_TERM
```
  - MODIFIES
```
public static final BasicSnippetData.Key MODIFIES
```
  - DEPENDENS
```
public static final BasicSnippetData.Key DEPENDENS
```
  - MEASURED_BY
```
public static final BasicSnippetData.Key MEASURED_BY
```
  - MODALITY
```
public static final BasicSnippetData.Key MODALITY
```
  - INF_FLOW_SPECS
```
public static final BasicSnippetData.Key INF_FLOW_SPECS
```
  - BLOCK_SELF
```
public static final BasicSnippetData.Key BLOCK_SELF
```
    Self term of the transformed block contract
  - BLOCK_VARS
```
public static final BasicSnippetData.Key BLOCK_VARS
```
    Variables originally used during parsing.
  - LABELS
```
public static final BasicSnippetData.Key LABELS
```
  - EXECUTION_CONTEXT
```
public static final BasicSnippetData.Key EXECUTION_CONTEXT
```
- Field Detail
  - type
```
private final java.lang.Class<?> type
```
- Method Detail
  - values
```
public static BasicSnippetData.Key[] values()
```
    Returns an array containing the constants of this enum type, in the order they are declared. This method may be used to iterate over the constants as follows:
```
for (BasicSnippetData.Key c : BasicSnippetData.Key.values())
    System.out.println(c);
```
    Returns:
    
    an array containing the constants of this enum type, in the order they are declared
  - valueOf
```
public static BasicSnippetData.Key valueOf(java.lang.String name)
```
    Returns the enum constant of this type with the specified name. The string must match exactly an identifier used to declare an enum constant in this type. (Extraneous whitespace characters are not permitted.)
    
    Parameters:
    
    name - the name of the enum constant to be returned.
    
    Returns:
    
    the enum constant with the specified name
    
    Throws:
    
    java.lang.IllegalArgumentException - if this enum type has no constant with the specified name
    
    java.lang.NullPointerException - if the argument is null
  - getType
```
public java.lang.Class<?> getType()
```

Enum BasicSnippetData.Key

Enum Constant Summary

Field Summary

Method Summary

Methods inherited from class java.lang.Enum

Methods inherited from class java.lang.Object

Enum Constant Detail

FOR_CLASS

TARGET_METHOD

TARGET_BLOCK

PRECONDITION

POSTCONDITION

LOOP_INVARIANT

LOOP_INVARIANT_TERM

MODIFIES

DEPENDENS

MEASURED_BY

MODALITY

INF_FLOW_SPECS

BLOCK_SELF

BLOCK_VARS

LABELS

EXECUTION_CONTEXT

Field Detail

type

Method Detail

values

valueOf

getType