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 |
---|
BlockContractRule.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 BlockContractRule.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()