public static final class AuxiliaryContractBuilders.GoalsConfigurator
extends java.lang.Object
Constructor and Description |
---|
GoalsConfigurator(AbstractAuxiliaryContractBuiltInRuleApp application,
TermLabelState termLabelState,
AbstractAuxiliaryContractRule.Instantiation instantiation,
java.util.List<Label> labels,
AuxiliaryContract.Variables variables,
PosInOccurrence occurrence,
Services services,
AbstractAuxiliaryContractRule rule) |
Modifier and Type | Method and Description |
---|---|
Term |
setUpLoopValidityGoal(Goal goal,
LoopContract contract,
Term context,
Term remember,
Term rememberNext,
java.util.Map<LocationVariable,Function> anonOutHeaps,
java.util.Map<LocationVariable,Term> modifiesClauses,
Term[] assumptions,
Term decreasesCheck,
Term[] postconditions,
Term[] postconditionsNext,
ProgramVariable exceptionParameter,
AuxiliaryContract.Terms terms,
AuxiliaryContract.Variables nextVars) |
void |
setUpPreconditionGoal(Goal goal,
Term update,
Term[] preconditions)
Sets up the precondition goal.
|
void |
setUpUsageGoal(Goal goal,
Term[] updates,
Term[] assumptions)
Sets up the usage goal.
|
Term |
setUpValidityGoal(Goal goal,
Term[] updates,
Term[] assumptions,
Term[] postconditions,
ProgramVariable exceptionParameter,
AuxiliaryContract.Terms terms) |
Term |
setUpWdGoal(Goal goal,
BlockContract contract,
Term update,
Term anonUpdate,
LocationVariable heap,
Function anonHeap,
ImmutableSet<ProgramVariable> localIns) |
public GoalsConfigurator(AbstractAuxiliaryContractBuiltInRuleApp application, TermLabelState termLabelState, AbstractAuxiliaryContractRule.Instantiation instantiation, java.util.List<Label> labels, AuxiliaryContract.Variables variables, PosInOccurrence occurrence, Services services, AbstractAuxiliaryContractRule rule)
application
- the rule application.termLabelState
- the term label state.instantiation
- the instantiationlabels
- all labels belonging to the block.variables
- the contract's variables.occurrence
- the position at which the rule is applied.services
- services.rule
- the rule being applied.public Term setUpWdGoal(Goal goal, BlockContract contract, Term update, Term anonUpdate, LocationVariable heap, Function anonHeap, ImmutableSet<ProgramVariable> localIns)
goal
- If this is not null
, the returned formula is added to this goal.contract
- the contract being applied.update
- the update.anonUpdate
- the anonymization update.heap
- the heap.anonHeap
- the anonymization heap.localIns
- all free local variables in the block.public Term setUpValidityGoal(Goal goal, Term[] updates, Term[] assumptions, Term[] postconditions, ProgramVariable exceptionParameter, AuxiliaryContract.Terms terms)
goal
- If this is not null
, the returned term is added to this goal.updates
- the updates.assumptions
- the preconditions.postconditions
- the postconditions.exceptionParameter
- the exception variable.terms
- the termified variables.public Term setUpLoopValidityGoal(Goal goal, LoopContract contract, Term context, Term remember, Term rememberNext, java.util.Map<LocationVariable,Function> anonOutHeaps, java.util.Map<LocationVariable,Term> modifiesClauses, Term[] assumptions, Term decreasesCheck, Term[] postconditions, Term[] postconditionsNext, ProgramVariable exceptionParameter, AuxiliaryContract.Terms terms, AuxiliaryContract.Variables nextVars)
goal
- If this is not null
, the returned term is added to this goal.contract
- the contract being applied.context
- the context update.remember
- the remembrance update for the current loop iteration.rememberNext
- the remembrance update for the next loop iteration.anonOutHeaps
- the heaps used in the anonOut update.modifiesClauses
- the modified clauses.assumptions
- the assumptions.decreasesCheck
- the decreases check.postconditions
- the current loop iteration's postconditions.postconditionsNext
- the next loop iteration's postconditions.exceptionParameter
- the exception variable.terms
- the termified variables.nextVars
- the variables for the next loop iteration.public void setUpPreconditionGoal(Goal goal, Term update, Term[] preconditions)
goal
- the precondition goal.update
- the update.preconditions
- the preconditions.Copyright © 2003-2019 The KeY-Project.