public class InvariantConfigurator extends Object
Modifier and Type | Field and Description |
---|---|
private static InvariantConfigurator |
configurator |
private static 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 List<Map<String,String>[]> |
invariants |
private HashMap<LoopStatement,List<Map<String,String>[]>> |
mapLoopsToInvariants |
private static int |
MOD_IDX |
private LoopInvariant |
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
|
LoopInvariant |
getLoopInvariant(LoopInvariant loopInv,
Services services,
boolean requiresVariant,
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 String DEFAULT
private static InvariantConfigurator configurator
private int index
private LoopInvariant newInvariant
private boolean userPressedCancel
public static InvariantConfigurator getInstance()
public LoopInvariant getLoopInvariant(LoopInvariant loopInv, Services services, boolean requiresVariant, List<LocationVariable> heapContext) throws RuleAbortException
loopInv
- services
- RuleAbortException