private static final class BlockContractRule.GoalsConfigurator extends Object
Modifier and Type | Field and Description |
---|---|
private BlockContractBuiltInRuleApp |
application |
private BlockContractRule.Instantiation |
instantiation |
private List<Label> |
labels |
private PosInOccurrence |
occurrence |
private BlockContractRule |
rule |
private Services |
services |
private TermLabelState |
termLabelState |
private BlockContract.Variables |
variables |
Constructor and Description |
---|
GoalsConfigurator(BlockContractBuiltInRuleApp application,
TermLabelState termLabelState,
BlockContractRule.Instantiation instantiation,
List<Label> labels,
BlockContract.Variables variables,
PosInOccurrence occurrence,
Services services,
BlockContractRule rule) |
Modifier and Type | Method and Description |
---|---|
private Term |
buildUsageFormula(Goal goal) |
private StatementBlock |
constructAbruptTerminationIfCascade() |
private StatementBlock |
finishTransactionIfModalityIsTransactional(Statement statement) |
private JavaBlock |
replaceBlock(JavaBlock java,
StatementBlock oldBlock,
StatementBlock newBlock) |
void |
setUpPreconditionGoal(Goal goal,
Term update,
Term[] preconditions) |
void |
setUpUsageGoal(Goal goal,
Term[] updates,
Term[] assumptions) |
void |
setUpValidityGoal(Goal goal,
Term[] updates,
Term[] assumptions,
Term[] postconditions,
ProgramVariable exceptionParameter,
BlockContract.Terms terms) |
void |
setUpWdGoal(Goal goal,
BlockContract contract,
Term update,
LocationVariable heap,
Function anonHeap,
ImmutableSet<ProgramVariable> localIns) |
private Statement |
wrapInMethodFrameIfContextIsAvailable(StatementBlock block) |
private final BlockContractBuiltInRuleApp application
private final TermLabelState termLabelState
private final BlockContractRule.Instantiation instantiation
private final BlockContract.Variables variables
private final PosInOccurrence occurrence
private final Services services
private final BlockContractRule rule
public GoalsConfigurator(BlockContractBuiltInRuleApp application, TermLabelState termLabelState, BlockContractRule.Instantiation instantiation, List<Label> labels, BlockContract.Variables variables, PosInOccurrence occurrence, Services services, BlockContractRule rule)
public void setUpWdGoal(Goal goal, BlockContract contract, Term update, LocationVariable heap, Function anonHeap, ImmutableSet<ProgramVariable> localIns)
public void setUpValidityGoal(Goal goal, Term[] updates, Term[] assumptions, Term[] postconditions, ProgramVariable exceptionParameter, BlockContract.Terms terms)
private Statement wrapInMethodFrameIfContextIsAvailable(StatementBlock block)
private StatementBlock finishTransactionIfModalityIsTransactional(Statement statement)
public void setUpPreconditionGoal(Goal goal, Term update, Term[] preconditions)
private JavaBlock replaceBlock(JavaBlock java, StatementBlock oldBlock, StatementBlock newBlock)
private StatementBlock constructAbruptTerminationIfCascade()