Modifier and Type | Method and Description |
---|---|
InitConfig |
KeYEnvironment.getInitConfig()
Returns the loaded project.
|
Modifier and Type | Method and Description |
---|---|
Proof |
AbstractUserInterfaceControl.createProof(InitConfig initConfig,
ProofOblInput input)
Instantiates a new
Proof in this UserInterfaceControl for the given
ProofOblInput based on the InitConfig . |
Proof |
UserInterfaceControl.createProof(InitConfig initConfig,
ProofOblInput input)
Instantiates a new
Proof in this UserInterfaceControl for the given
ProofOblInput based on the InitConfig . |
protected abstract ProofEnvironment |
AbstractUserInterfaceControl.createProofEnvironmentAndRegisterProof(ProofOblInput proofOblInput,
ProofAggregate proofList,
InitConfig initConfig)
registers the proof aggregate at the UI
|
ProofEnvironment |
DefaultUserInterfaceControl.createProofEnvironmentAndRegisterProof(ProofOblInput proofOblInput,
ProofAggregate proofList,
InitConfig initConfig)
registers the proof aggregate at the UI
|
boolean |
DefaultUserInterfaceControl.selectProofObligation(InitConfig initConfig)
This method is called if no
IPersistablePO.LoadedPOContainer was created
via AbstractProblemLoader.createProofObligationContainer() and can be overwritten
for instance to open the proof management dialog as done by ProblemLoader . |
Constructor and Description |
---|
KeYEnvironment(U ui,
InitConfig initConfig)
Constructor
|
KeYEnvironment(U ui,
InitConfig initConfig,
Proof loadedProof,
Pair<java.lang.String,Location> proofScript,
AbstractProblemLoader.ReplayResult replayResult)
Constructor
|
Modifier and Type | Method and Description |
---|---|
boolean |
WindowUserInterfaceControl.selectProofObligation(InitConfig initConfig) |
static boolean |
ProofManagementDialog.showInstance(InitConfig initConfig)
Shows the dialog.
|
static void |
ProofManagementDialog.showInstance(InitConfig initConfig,
KeYJavaType selectedKJT,
IObserverFunction selectedTarget)
Shows the dialog and selects the passed
KeYJavaType and its
IObserverFunction . |
static void |
ProofManagementDialog.showInstance(InitConfig initConfig,
Proof selectedProof)
Shows the dialog and selects the passed proof.
|
Modifier and Type | Method and Description |
---|---|
Proof |
AbstractInfFlowPO.createProof(java.lang.String proofName,
Term poTerm,
InitConfig proofConfig) |
InfFlowProof |
AbstractInfFlowPO.createProofObject(java.lang.String proofName,
java.lang.String proofHeader,
Term poTerm,
InitConfig proofConfig) |
static IPersistablePO.LoadedPOContainer |
InfFlowContractPO.loadFrom(InitConfig initConfig,
java.util.Properties properties)
Instantiates a new proof obligation with the given settings.
|
Constructor and Description |
---|
AbstractInfFlowPO(InitConfig initConfig,
java.lang.String name) |
BlockExecutionPO(InitConfig initConfig,
BlockContract contract,
ProofObligationVars symbExecVars,
Goal initiatingGoal,
ExecutionContext context) |
BlockExecutionPO(InitConfig initConfig,
BlockContract contract,
ProofObligationVars symbExecVars,
Goal initiatingGoal,
ExecutionContext context,
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.
|
InfFlowContractPO(InitConfig initConfig,
InformationFlowContract contract) |
LoopInvExecutionPO(InitConfig initConfig,
LoopSpecification loopInv,
ProofObligationVars symbExecVars,
Goal initiatingGoal,
ExecutionContext context,
Term guardTerm) |
LoopInvExecutionPO(InitConfig initConfig,
LoopSpecification loopInv,
ProofObligationVars symbExecVars,
Goal initiatingGoal,
ExecutionContext context,
Term guardTerm,
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.
|
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.
|
Constructor and Description |
---|
InfFlowProof(java.lang.String name,
InitConfig initConfig) |
InfFlowProof(java.lang.String name,
Sequent sequent,
java.lang.String header,
TacletIndex rules,
BuiltInRuleIndex builtInRules,
InitConfig initConfig) |
InfFlowProof(java.lang.String name,
Term problem,
java.lang.String header,
InitConfig initConfig) |
Modifier and Type | Method and Description |
---|---|
InitConfig |
Proof.getInitConfig() |
Constructor and Description |
---|
Proof(java.lang.String name,
InitConfig initConfig)
constructs a new empty proof with name
|
Proof(java.lang.String name,
Sequent sequent,
java.lang.String header,
TacletIndex rules,
BuiltInRuleIndex builtInRules,
InitConfig initConfig) |
Proof(java.lang.String name,
Term problem,
java.lang.String header,
InitConfig initConfig) |
Modifier and Type | Field and Description |
---|---|
protected InitConfig |
AbstractPO.environmentConfig |
protected InitConfig |
AbstractOperationPO.proofConfig |
Modifier and Type | Method and Description |
---|---|
InitConfig |
InitConfig.copy()
returns a copy of this initial configuration copying the namespaces,
the contained JavaInfo while using the immutable set of taclets in the
copy
|
InitConfig |
InitConfig.copyWithServices(Services services)
returns a copy of this initial configuration copying the namespaces,
the contained JavaInfo while using the immutable set of taclets in the
copy
|
InitConfig |
InitConfig.deepCopy()
returns a copy of this initial configuration copying the namespaces,
the contained JavaInfo while using the immutable set of taclets in the
copy
|
protected InitConfig |
DependencyContractPO.getCreatedInitConfigForSingleProof() |
protected InitConfig |
FunctionalBlockContractPO.getCreatedInitConfigForSingleProof() |
protected InitConfig |
WellDefinednessPO.getCreatedInitConfigForSingleProof() |
protected InitConfig |
FunctionalLoopContractPO.getCreatedInitConfigForSingleProof() |
protected InitConfig |
AbstractOperationPO.getCreatedInitConfigForSingleProof() |
protected abstract InitConfig |
AbstractPO.getCreatedInitConfigForSingleProof() |
InitConfig |
ProblemInitializer.prepare(EnvInput envInput)
Creates an initConfig / a proof environment and reads an EnvInput into it
|
Modifier and Type | Method and Description |
---|---|
protected void |
AbstractPO.collectClassAxioms(KeYJavaType selfKJT,
InitConfig proofConfig) |
protected Proof |
AbstractPO.createProof(java.lang.String proofName,
Term poTerm,
InitConfig proofConfig)
Creates a Proof (helper for getPO()).
|
protected Proof |
AbstractPO.createProofObject(java.lang.String proofName,
java.lang.String proofHeader,
Term poTerm,
InitConfig proofConfig) |
static IPersistablePO.LoadedPOContainer |
DependencyContractPO.loadFrom(InitConfig initConfig,
java.util.Properties properties)
Instantiates a new proof obligation with the given settings.
|
static IPersistablePO.LoadedPOContainer |
FunctionalBlockContractPO.loadFrom(InitConfig initConfig,
java.util.Properties properties)
Instantiates a new proof obligation with the given settings.
|
static IPersistablePO.LoadedPOContainer |
WellDefinednessPO.loadFrom(InitConfig initConfig,
java.util.Properties properties)
Instantiates a new proof obligation with the given settings.
|
static IPersistablePO.LoadedPOContainer |
FunctionalLoopContractPO.loadFrom(InitConfig initConfig,
java.util.Properties properties)
Instantiates a new proof obligation with the given settings.
|
static IPersistablePO.LoadedPOContainer |
FunctionalOperationContractPO.loadFrom(InitConfig initConfig,
java.util.Properties properties)
Instantiates a new proof obligation with the given settings.
|
Term |
POExtension.modifyPostTerm(InitConfig proofConfig,
Services services,
Term postTerm)
Modifies the post condition.
|
void |
ProblemInitializer.readEnvInput(EnvInput envInput,
InitConfig initConfig) |
ProofAggregate |
ProblemInitializer.startProver(InitConfig initConfig,
ProofOblInput po) |
Constructor and Description |
---|
AbstractOperationPO(InitConfig initConfig,
java.lang.String name)
Constructor.
|
AbstractOperationPO(InitConfig initConfig,
java.lang.String name,
boolean addUninterpretedPredicate,
boolean addSymbolicExecutionLabel)
Constructor.
|
AbstractPO(InitConfig initConfig,
java.lang.String name) |
DependencyContractPO(InitConfig initConfig,
DependencyContract contract) |
FunctionalBlockContractPO(InitConfig initConfig,
FunctionalBlockContract contract) |
FunctionalLoopContractPO(InitConfig initConfig,
FunctionalLoopContract contract) |
FunctionalOperationContractPO(InitConfig initConfig,
FunctionalOperationContract contract)
Constructor.
|
FunctionalOperationContractPO(InitConfig initConfig,
FunctionalOperationContract contract,
boolean addUninterpretedPredicate,
boolean addSymbolicExecutionLabel)
Constructor.
|
WellDefinednessPO(InitConfig initConfig,
WellDefinednessCheck check)
Constructor
|
Modifier and Type | Field and Description |
---|---|
protected InitConfig |
AbstractEnvInput.initConfig |
protected InitConfig |
KeYFile.initConfig |
Modifier and Type | Method and Description |
---|---|
protected InitConfig |
AbstractProblemLoader.createInitConfig()
Creates the
InitConfig . |
InitConfig |
AbstractProblemLoader.getInitConfig()
Returns the instantiated
InitConfig which provides access to the loaded source elements and specifications. |
Modifier and Type | Method and Description |
---|---|
protected void |
AbstractProblemLoader.selectAndLoadProof(ProblemLoaderControl control,
InitConfig initConfig)
Asks the user to select a proof obligation and loads it.
|
protected void |
ProblemLoader.selectAndLoadProof(ProblemLoaderControl control,
InitConfig initConfig) |
boolean |
ProblemLoaderControl.selectProofObligation(InitConfig initConfig)
This method is called if no
IPersistablePO.LoadedPOContainer was created
via AbstractProblemLoader.createProofObligationContainer() and can be overwritten
for instance to open the proof management dialog as done by ProblemLoader . |
void |
AbstractEnvInput.setInitConfig(InitConfig initConfig) |
void |
LDTInput.setInitConfig(InitConfig conf) |
void |
KeYFile.setInitConfig(InitConfig conf) |
void |
EnvInput.setInitConfig(InitConfig initConfig)
Sets the initial configuration the read environment input should be
added to.
|
Modifier and Type | Method and Description |
---|---|
InitConfig |
ProofEnvironment.getInitConfigForEnvironment()
returns the initial configuration of which a copy can be
used to load proofs belonging to this environment.
|
Constructor and Description |
---|
ProofEnvironment(InitConfig initConfig)
constructs a proof environment with the given initial
configuration of the proofs contained in the environment.
|
Modifier and Type | Method and Description |
---|---|
ContractPO |
FunctionalOperationContractImpl.createProofObl(InitConfig initConfig) |
ContractPO |
InformationFlowContractImpl.createProofObl(InitConfig initConfig) |
ContractPO |
FunctionalBlockContract.createProofObl(InitConfig initConfig) |
ContractPO |
DependencyContractImpl.createProofObl(InitConfig initConfig) |
ContractPO |
WellDefinednessCheck.createProofObl(InitConfig initConfig) |
ContractPO |
Contract.createProofObl(InitConfig initConfig)
Returns a proof obligation to the passed initConfig.
|
ContractPO |
FunctionalLoopContract.createProofObl(InitConfig initConfig) |
ProofOblInput |
FunctionalAuxiliaryContract.createProofObl(InitConfig initConfig,
Contract contract) |
ProofOblInput |
FunctionalOperationContractImpl.createProofObl(InitConfig initConfig,
Contract contract) |
ProofOblInput |
InformationFlowContractImpl.createProofObl(InitConfig initConfig,
Contract contract) |
ProofOblInput |
FunctionalBlockContract.createProofObl(InitConfig initConfig,
Contract contract) |
ProofOblInput |
DependencyContractImpl.createProofObl(InitConfig initConfig,
Contract contract) |
ProofOblInput |
WellDefinednessCheck.createProofObl(InitConfig initConfig,
Contract contract) |
ProofOblInput |
Contract.createProofObl(InitConfig initConfig,
Contract contract)
Returns a proof obligation to the passed contract and initConfig.
|
ProofOblInput |
FunctionalLoopContract.createProofObl(InitConfig initConfig,
Contract contract) |
ProofOblInput |
FunctionalAuxiliaryContract.createProofObl(InitConfig initConfig,
Contract contract,
boolean supportSymbolicExecutionAPI) |
ProofOblInput |
FunctionalOperationContractImpl.createProofObl(InitConfig initConfig,
Contract contract,
boolean addSymbolicExecutionLabel) |
ProofOblInput |
InformationFlowContractImpl.createProofObl(InitConfig initConfig,
Contract contract,
boolean addSymbolicExecutionLabel) |
ProofOblInput |
FunctionalBlockContract.createProofObl(InitConfig initConfig,
Contract contract,
boolean supportSymbolicExecutionAPI) |
ProofOblInput |
DependencyContractImpl.createProofObl(InitConfig initConfig,
Contract contract,
boolean addSymbolicExecutionLabel) |
ProofOblInput |
WellDefinednessCheck.createProofObl(InitConfig initConfig,
Contract contract,
boolean addSymbolicExecutionLabel) |
ProofOblInput |
Contract.createProofObl(InitConfig initConfig,
Contract contract,
boolean supportSymbolicExecutionAPI)
Returns a proof obligation to the passed contract and initConfig.
|
ProofOblInput |
FunctionalLoopContract.createProofObl(InitConfig initConfig,
Contract contract,
boolean supportSymbolicExecutionAPI) |
Modifier and Type | Method and Description |
---|---|
InitConfig |
ExecutionNodeReader.AbstractKeYlessExecutionElement.getInitConfig()
Returns the
InitConfig used by IExecutionElement.getProof() . |
Modifier and Type | Method and Description |
---|---|
InitConfig |
IExecutionElement.getInitConfig()
Returns the
InitConfig used by IExecutionElement.getProof() . |
Modifier and Type | Method and Description |
---|---|
InitConfig |
AbstractExecutionElement.getInitConfig()
Returns the
InitConfig used by IExecutionElement.getProof() . |
Modifier and Type | Method and Description |
---|---|
protected Term |
ExecutionVariable.computeValueCondition(TermBuilder tb,
java.util.List<Goal> valueGoals,
InitConfig initConfig)
|
protected ExecutionValue[] |
ExecutionVariable.instantiateValuesFromSideProof(InitConfig initConfig,
Services services,
TermBuilder tb,
ApplyStrategyInfo info,
Operator resultOperator,
Term siteProofSelectTerm,
Term siteProofCondition)
Analyzes the side proof defined by the
ApplyStrategyInfo
and creates ExecutionValue s from it. |
Modifier and Type | Method and Description |
---|---|
static IProgramMethod |
ProgramMethodPO.getProgramMethod(InitConfig initConfig,
java.util.Properties properties)
Searches the
IProgramMethod defined by the given Properties . |
static IPersistablePO.LoadedPOContainer |
ProgramMethodPO.loadFrom(InitConfig initConfig,
java.util.Properties properties)
Instantiates a new proof obligation with the given settings.
|
static IPersistablePO.LoadedPOContainer |
ProgramMethodSubsetPO.loadFrom(InitConfig initConfig,
java.util.Properties properties)
Instantiates a new proof obligation with the given settings.
|
Term |
TruthValuePOExtension.modifyPostTerm(InitConfig proofConfig,
Services services,
Term postTerm)
Modifies the post condition.
|
Constructor and Description |
---|
ProgramMethodPO(InitConfig initConfig,
java.lang.String name,
IProgramMethod pm,
java.lang.String precondition)
Constructor.
|
ProgramMethodPO(InitConfig initConfig,
java.lang.String name,
IProgramMethod pm,
java.lang.String precondition,
boolean addUninterpretedPredicate,
boolean addSymbolicExecutionLabel)
Constructor.
|
ProgramMethodSubsetPO(InitConfig initConfig,
java.lang.String name,
IProgramMethod pm,
java.lang.String precondition,
Position startPosition,
Position endPosition)
Constructor.
|
ProgramMethodSubsetPO(InitConfig initConfig,
java.lang.String name,
IProgramMethod pm,
java.lang.String precondition,
Position startPosition,
Position endPosition,
boolean addUninterpretedPredicate,
boolean addSymbolicExecutionLabel)
Constructor.
|
Modifier and Type | Method and Description |
---|---|
static boolean |
SymbolicExecutionJavaProfile.isTruthValueEvaluationEnabled(InitConfig initConfig)
Checks if truth value evaluation is enabled in the given
InitConfig . |
Modifier and Type | Method and Description |
---|---|
static ProofEnvironment |
SymbolicExecutionSideProofUtil.cloneProofEnvironmentWithOwnOneStepSimplifier(InitConfig sourceInitConfig,
boolean useSimplifyTermProfile)
Creates a copy of the
ProofEnvironment of the given Proof
which has his own OneStepSimplifier instance. |
static Term |
SymbolicExecutionUtil.simplify(InitConfig initConfig,
Proof parentProof,
Term term)
Simplifies the given
Term in a side proof. |
static Term |
SymbolicExecutionUtil.simplify(InitConfig initConfig,
Term term)
Simplifies the given
Term in a side proof. |
Constructor and Description |
---|
SymbolicExecutionEnvironment(U ui,
InitConfig initConfig,
SymbolicExecutionTreeBuilder builder)
Constructor.
|
Modifier and Type | Method and Description |
---|---|
ProofAggregate |
ProofObligationCreator.create(ImmutableSet<Taclet> taclets,
InitConfig[] initConfigs,
ImmutableSet<Taclet> axioms,
java.util.Collection<TacletSoundnessPOLoader.LoaderListener> listeners)
Creates for each taclet in
taclets a proof obligation
containing the corresponding FOL formula of the taclet. |
static IPersistablePO.LoadedPOContainer |
TacletProofObligationInput.loadFrom(InitConfig initConfig,
java.util.Properties properties) |
void |
TacletLoader.manageAvailableTaclets(InitConfig initConfig,
Taclet tacletToProve)
When proving existing system taclets, all rules which occurred prior to
the desired taclet need to be elminated from the set of available taclets
to avoid circular proofs.
|
Constructor and Description |
---|
TacletFromFileLoader(ProgressMonitor pm,
ProblemInitializer.ProblemInitializerListener listener,
ProblemInitializer problemInitializer,
java.io.File fileForTaclets,
java.util.Collection<java.io.File> filesForAxioms,
InitConfig initConfig) |
TacletFromFileLoader(TacletLoader.TacletFromFileLoader loader,
InitConfig initConfig) |
TacletProofObligationInput(java.lang.String tacletName,
InitConfig initConfig)
Instantiates a new taclet proof obligation input object.
|
TacletSoundnessPOLoader(TacletSoundnessPOLoader.LoaderListener listener,
TacletSoundnessPOLoader.TacletFilter filter,
boolean loadAsLemmata,
TacletLoader loader,
InitConfig originalConfig,
boolean isOnlyUsedForProvingTaclets) |
Modifier and Type | Field and Description |
---|---|
protected InitConfig |
ConsoleProofObligationSelector.initConfig |
Modifier and Type | Method and Description |
---|---|
ProofEnvironment |
AbstractMediatorUserInterfaceControl.createProofEnvironmentAndRegisterProof(ProofOblInput proofOblInput,
ProofAggregate proofList,
InitConfig initConfig)
registers the proof aggregate at the UI
|
boolean |
ConsoleUserInterfaceControl.selectProofObligation(InitConfig initConfig) |
Constructor and Description |
---|
ConsoleProofObligationSelector(ConsoleUserInterfaceControl ui,
InitConfig initConfig) |
NIProofObligationSelector(ConsoleUserInterfaceControl ui,
InitConfig initConfig) |
Copyright © 2003-2019 The KeY-Project.