Package | Description |
---|---|
de.uka.ilkd.key.informationflow.po | |
de.uka.ilkd.key.informationflow.po.snippet | |
de.uka.ilkd.key.informationflow.rule.tacletbuilder | |
de.uka.ilkd.key.speclang |
This package contains the specification language frontends of KeY.
|
Modifier and Type | Method and Description |
---|---|
InformationFlowContract |
InfFlowContractPO.getContract() |
InformationFlowContract |
SymbolicExecutionPO.getContract() |
Constructor and Description |
---|
InfFlowContractPO(InitConfig initConfig,
InformationFlowContract contract) |
SymbolicExecutionPO(InitConfig initConfig,
InformationFlowContract contract,
ProofObligationVars symbExecVars,
Goal initiatingGoal) |
SymbolicExecutionPO(InitConfig initConfig,
InformationFlowContract contract,
ProofObligationVars symbExecVars,
Goal initiatingGoal,
Services services)
To be used only for auxiliary proofs where the services object of
the actual proof has to be used instead of the initial services form
the InitConfig.
|
Modifier and Type | Method and Description |
---|---|
static BasicPOSnippetFactory |
POSnippetFactory.getBasicFactory(InformationFlowContract contract,
ProofObligationVars vars,
Services services) |
static InfFlowPOSnippetFactory |
POSnippetFactory.getInfFlowFactory(InformationFlowContract contract,
ProofObligationVars vars1,
ProofObligationVars vars2,
Services services) |
Modifier and Type | Method and Description |
---|---|
void |
MethodInfFlowUnfoldTacletBuilder.setContract(InformationFlowContract c) |
Modifier and Type | Class and Description |
---|---|
class |
InformationFlowContractImpl
Standard implementation of the DependencyContract interface.
|
Modifier and Type | Method and Description |
---|---|
InformationFlowContract |
ContractFactory.createInformationFlowContract(KeYJavaType forClass,
IProgramMethod pm,
KeYJavaType specifiedIn,
Modality modality,
Term requires,
Term requiresFree,
Term measuredBy,
Term modifies,
boolean hasMod,
ProgramVariableCollection progVars,
Term accessible,
ImmutableList<InfFlowSpec> infFlowSpecs,
boolean toBeSaved) |
InformationFlowContract |
InformationFlowContractImpl.map(java.util.function.UnaryOperator<Term> op,
Services services) |
InformationFlowContract |
InformationFlowContract.map(java.util.function.UnaryOperator<Term> op,
Services services) |
InformationFlowContract |
InformationFlowContractImpl.setID(int newId) |
InformationFlowContract |
InformationFlowContract.setID(int newId)
Return a new contract which equals this contract except that the id is
set to the new id.
|
InformationFlowContract |
InformationFlowContractImpl.setModality(Modality modality) |
InformationFlowContract |
InformationFlowContract.setModality(Modality modality) |
InformationFlowContract |
InformationFlowContractImpl.setModifies(Term modifies) |
InformationFlowContract |
InformationFlowContract.setModifies(Term modifies) |
InformationFlowContract |
InformationFlowContractImpl.setName(java.lang.String name) |
InformationFlowContract |
InformationFlowContract.setName(java.lang.String name) |
InformationFlowContract |
InformationFlowContractImpl.setTarget(KeYJavaType newKJT,
IObserverFunction newPM) |
InformationFlowContract |
InformationFlowContract.setTarget(KeYJavaType newKJT,
IObserverFunction newPM)
Return a new contract which equals this contract except that the
the KeYJavaType and ObserverFunction are set to the new values.
|
Copyright © 2003-2019 The KeY-Project.