public class InvariantConfigurator
extends java.lang.Object
Modifier and Type | Field and Description |
---|---|
private static InvariantConfigurator |
configurator |
private static java.lang.String |
DEFAULT |
private static int |
IF_OO_IDX |
private static int |
IF_POST_IDX |
private static int |
IF_PRE_IDX |
private int |
index |
private static int |
INV_IDX |
private java.util.List<java.util.Map<java.lang.String,java.lang.String>[]> |
invariants |
private java.util.HashMap<LoopStatement,java.util.List<java.util.Map<java.lang.String,java.lang.String>[]>> |
mapLoopsToInvariants |
private static int |
MOD_IDX |
private LoopSpecification |
newInvariant |
private boolean |
userPressedCancel |
private static int |
VAR_IDX |
Modifier | Constructor and Description |
---|---|
private |
InvariantConfigurator()
Singleton
|
Modifier and Type | Method and Description |
---|---|
static InvariantConfigurator |
getInstance()
Returns the single Instance of this class
|
LoopSpecification |
getLoopInvariant(LoopSpecification loopInv,
Services services,
boolean requiresVariant,
java.util.List<LocationVariable> heapContext)
Creates a Dialog.
|
private static final int INV_IDX
private static final int MOD_IDX
private static final int VAR_IDX
private static final int IF_PRE_IDX
private static final int IF_POST_IDX
private static final int IF_OO_IDX
private static final java.lang.String DEFAULT
private static InvariantConfigurator configurator
private java.util.List<java.util.Map<java.lang.String,java.lang.String>[]> invariants
private java.util.HashMap<LoopStatement,java.util.List<java.util.Map<java.lang.String,java.lang.String>[]>> mapLoopsToInvariants
private int index
private LoopSpecification newInvariant
private boolean userPressedCancel
public static InvariantConfigurator getInstance()
public LoopSpecification getLoopInvariant(LoopSpecification loopInv, Services services, boolean requiresVariant, java.util.List<LocationVariable> heapContext) throws RuleAbortException
loopInv
- services
- RuleAbortException