Package | Description |
---|---|
de.uka.ilkd.key.rule |
This package contains classes for implementing rules.
|
Modifier and Type | Method and Description |
---|---|
BlockContractInternalBuiltInRuleApp |
BlockContractInternalRule.createApp(PosInOccurrence occurrence,
TermServices services) |
BlockContractInternalBuiltInRuleApp |
BlockContractInternalBuiltInRuleApp.replacePos(PosInOccurrence newOccurrence) |
BlockContractInternalBuiltInRuleApp |
BlockContractInternalBuiltInRuleApp.setIfInsts(ImmutableList<PosInOccurrence> ifInstantiations) |
BlockContractInternalBuiltInRuleApp |
BlockContractInternalBuiltInRuleApp.tryToInstantiate(Goal goal) |
Modifier and Type | Method and Description |
---|---|
protected AbstractBlockContractRule.InfFlowValidityData |
AbstractBlockContractRule.setUpInfFlowValidityGoal(Goal infFlowGoal,
BlockContract contract,
java.util.Map<LocationVariable,Function> anonymisationHeaps,
Services services,
AuxiliaryContract.Variables variables,
ProgramVariable exceptionParameter,
java.util.List<LocationVariable> heaps,
ImmutableSet<ProgramVariable> localInVariables,
ImmutableSet<ProgramVariable> localOutVariables,
BlockContractInternalBuiltInRuleApp application,
AbstractAuxiliaryContractRule.Instantiation instantiation) |
Copyright © 2003-2019 The KeY-Project.