Modifier and Type | Method and Description |
---|---|
Proof |
ProofApi.getProof() |
Constructor and Description |
---|
ProofApi(Proof proof,
KeYEnvironment<?> currentEnv) |
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 . |
Proof |
KeYEnvironment.createProof(ProofOblInput input)
Creates a new
Proof with help of the UserInterfaceControl . |
Proof |
KeYEnvironment.getLoadedProof()
Returns the loaded
Proof if a proof file was loaded. |
Modifier and Type | Method and Description |
---|---|
static java.util.List<Name> |
TermLabelVisibilityManager.getSortedTermLabelNames(Proof proof)
Returns a sorted list of all term label names supported by the given
Proof . |
boolean |
AbstractProofControl.isAutoModeSupported(Proof proof)
Checks if the auto mode of this
UserInterfaceControl supports the given Proof . |
boolean |
ProofControl.isAutoModeSupported(Proof proof)
Checks if the auto mode of this
UserInterfaceControl supports the given Proof . |
void |
InteractionListener.runAutoMode(java.util.List<Node> initialGoals,
Proof proof,
ApplyStrategyInfo info) |
void |
InteractionListener.settingChanged(Proof proof,
Settings settings,
InteractionListener.SettingType type,
java.lang.String message) |
void |
AbstractProofControl.startAndWaitForAutoMode(Proof proof)
Starts the auto mode for the given proof which must be contained
in this user interface and blocks the current thread until it
has finished.
|
void |
ProofControl.startAndWaitForAutoMode(Proof proof)
Starts the auto mode for the given proof which must be contained
in this user interface and blocks the current thread until it
has finished.
|
void |
AbstractProofControl.startAndWaitForAutoMode(Proof proof,
ImmutableList<Goal> goals)
Starts the auto mode for the given proof which must be contained
in this user interface and blocks the current thread until it
has finished.
|
void |
ProofControl.startAndWaitForAutoMode(Proof proof,
ImmutableList<Goal> goals)
Starts the auto mode for the given proof which must be contained
in this user interface and blocks the current thread until it
has finished.
|
void |
AbstractProofControl.startAutoMode(Proof proof)
Starts the auto mode for the given
Proof . |
void |
ProofControl.startAutoMode(Proof proof)
Starts the auto mode for the given
Proof . |
void |
AbstractProofControl.startAutoMode(Proof proof,
ImmutableList<Goal> goals)
|
void |
ProofControl.startAutoMode(Proof proof,
ImmutableList<Goal> goals)
|
void |
DefaultProofControl.startAutoMode(Proof proof,
ImmutableList<Goal> goals,
ProverTaskListener ptl) |
protected abstract void |
AbstractProofControl.startAutoMode(Proof proof,
ImmutableList<Goal> goals,
ProverTaskListener ptl) |
Constructor and Description |
---|
FocussedAutoModeTaskListener(Proof proof) |
KeYEnvironment(U ui,
InitConfig initConfig,
Proof loadedProof,
Pair<java.lang.String,Location> proofScript,
AbstractProblemLoader.ReplayResult replayResult)
Constructor
|
Modifier and Type | Method and Description |
---|---|
Proof |
TacletInstantiationModel.proof() |
Modifier and Type | Method and Description |
---|---|
Proof |
KeYMediator.getSelectedProof()
returns the current selected proof
|
Proof |
KeYSelectionModel.getSelectedProof()
returns the proof that is selected by the user
|
Modifier and Type | Method and Description |
---|---|
javax.swing.DefaultListModel<Proof> |
KeYMediator.getCurrentlyOpenedProofs()
Provides a list of currently opened view.
|
Modifier and Type | Method and Description |
---|---|
void |
KeYMediator.setProof(Proof p)
Selects the specified proof and initializes it.
|
void |
KeYSelectionModel.setProof(Proof p)
Does not take care of GUI effects
|
Modifier and Type | Method and Description |
---|---|
boolean |
TaskTree.containsProof(Proof proof)
Checks if the given
Proof is contained in the model. |
protected static Pair<java.io.File,java.lang.String> |
WindowUserInterfaceControl.fileName(Proof proof,
java.lang.String fileExtension) |
Strategy |
StrategySelectionView.getStrategy(java.lang.String strategyName,
Proof proof,
StrategyProperties properties) |
protected boolean |
WindowUserInterfaceControl.inStopAtFirstUncloseableGoalMode(Proof proof) |
void |
StrategySelectionView.refresh(Proof proof)
performs a refresh of all elements in this tab
|
void |
TaskTree.removeProof(Proof proof)
Removes the given proof from the model.
|
void |
TaskTree.removeTask(Proof p) |
java.io.File |
WindowUserInterfaceControl.saveProof(Proof proof,
java.lang.String fileExtension)
Save proof in file.
|
void |
WindowUserInterfaceControl.saveProofBundle(Proof proof)
Saves the proof as a bundle, i.e., as a zip archive containing all dependencies (Java
sources, classpath and bootclasspath if present, other included key files, e.g., user-defined
taclets).
|
static void |
ProofManagementDialog.showInstance(InitConfig initConfig,
Proof selectedProof)
Shows the dialog and selects the passed proof.
|
Modifier and Type | Method and Description |
---|---|
static java.lang.String |
ShowProofStatistics.getCSVStatisticsMessage(Proof proof)
Gets the CSV statistics message.
|
static java.lang.String |
ShowProofStatistics.getHTMLStatisticsMessage(Proof proof) |
Constructor and Description |
---|
Window(MainWindow mainWindow,
Proof proof)
Creates a new (initially invisible) proof statistics window.
|
Modifier and Type | Method and Description |
---|---|
java.util.List<javax.swing.Action> |
ContextMenuAdapter.getContextActions(KeYMediator mediator,
ContextMenuKind kind,
Proof underlyingObject) |
Constructor and Description |
---|
JoinDialog(java.util.List<ProspectivePartner> partnerList,
Proof proof,
PredicateEstimator estimator,
Services services) |
JoinMenuItem(java.util.List<ProspectivePartner> partner,
Proof proof,
KeYMediator mediator) |
Modifier and Type | Method and Description |
---|---|
java.lang.String |
LemmataAutoModeOptions.createProofPath(Proof p) |
Modifier and Type | Method and Description |
---|---|
Proof |
ProofClosedNotificationEvent.getProof() |
Constructor and Description |
---|
ProofClosedNotificationEvent(Proof proof)
creates a proof closed notification event
|
Modifier and Type | Method and Description |
---|---|
void |
ProofTreeView.removeProofs(Proof[] ps) |
Constructor and Description |
---|
GUIProofTreeModel(Proof p)
construct a GUIProofTreeModel that mirrors the given
Proof.
|
Constructor and Description |
---|
SolverListener(SMTSettings settings,
Proof smtProof) |
Modifier and Type | Method and Description |
---|---|
protected Proof |
CounterExampleAction.MainWindowCounterExampleGenerator.createProof(UserInterfaceControl ui,
Proof oldProof,
Sequent oldSequent,
java.lang.String proofName)
Creates a new
Proof . |
Proof |
TGWorker.getOriginalProof() |
Modifier and Type | Method and Description |
---|---|
protected Proof |
CounterExampleAction.MainWindowCounterExampleGenerator.createProof(UserInterfaceControl ui,
Proof oldProof,
Sequent oldSequent,
java.lang.String proofName)
Creates a new
Proof . |
protected SolverLauncherListener |
CounterExampleAction.NoMainWindowCounterExampleGenerator.createSolverListener(SMTSettings settings,
Proof proof)
Creates the
SolverLauncherListener which handles the results
of the launched SMT solver. |
protected SolverLauncherListener |
CounterExampleAction.MainWindowCounterExampleGenerator.createSolverListener(SMTSettings settings,
Proof proof)
Creates the
SolverLauncherListener which handles the results
of the launched SMT solver. |
Modifier and Type | Method and Description |
---|---|
protected static void |
AbstractFinishAuxiliaryComputationMacro.addContractApplicationTaclets(Goal initiatingGoal,
Proof symbExecProof) |
ProofMacroFinishedInfo |
StartAuxiliaryLoopComputationMacro.applyTo(UserInterfaceControl uic,
Proof proof,
ImmutableList<Goal> goals,
PosInOccurrence posInOcc,
ProverTaskListener listener) |
ProofMacroFinishedInfo |
FinishAuxiliaryLoopComputationMacro.applyTo(UserInterfaceControl uic,
Proof proof,
ImmutableList<Goal> goals,
PosInOccurrence posInOcc,
ProverTaskListener listener) |
ProofMacroFinishedInfo |
StartAuxiliaryBlockComputationMacro.applyTo(UserInterfaceControl uic,
Proof proof,
ImmutableList<Goal> goals,
PosInOccurrence posInOcc,
ProverTaskListener listener) |
ProofMacroFinishedInfo |
FinishAuxiliaryBlockComputationMacro.applyTo(UserInterfaceControl uic,
Proof proof,
ImmutableList<Goal> goals,
PosInOccurrence posInOcc,
ProverTaskListener listener) |
ProofMacroFinishedInfo |
StartAuxiliaryMethodComputationMacro.applyTo(UserInterfaceControl uic,
Proof proof,
ImmutableList<Goal> goals,
PosInOccurrence posInOcc,
ProverTaskListener listener) |
ProofMacroFinishedInfo |
ExhaustiveProofMacro.applyTo(UserInterfaceControl uic,
Proof proof,
ImmutableList<Goal> goals,
PosInOccurrence posInOcc,
ProverTaskListener listener) |
ProofMacroFinishedInfo |
FinishAuxiliaryMethodComputationMacro.applyTo(UserInterfaceControl uic,
Proof proof,
ImmutableList<Goal> goals,
PosInOccurrence posInOcc,
ProverTaskListener listener) |
boolean |
StartAuxiliaryLoopComputationMacro.canApplyTo(Proof proof,
ImmutableList<Goal> goals,
PosInOccurrence posInOcc) |
boolean |
SelfcompositionStateExpansionMacro.canApplyTo(Proof proof,
ImmutableList<Goal> goals,
PosInOccurrence posInOcc)
Can this macro be applied on the given goals?
This method should not make any changes but check if the macro can be
applied or not on the given goals.
|
boolean |
FinishAuxiliaryLoopComputationMacro.canApplyTo(Proof proof,
ImmutableList<Goal> goals,
PosInOccurrence posInOcc) |
boolean |
StartAuxiliaryBlockComputationMacro.canApplyTo(Proof proof,
ImmutableList<Goal> goals,
PosInOccurrence posInOcc) |
boolean |
StateExpansionAndInfFlowContractApplicationMacro.canApplyTo(Proof proof,
ImmutableList<Goal> goals,
PosInOccurrence posInOcc)
Can this macro be applied on the given goals?
This method should not make any changes but check if the macro can be
applied or not on the given goals.
|
boolean |
FullUseInformationFlowContractMacro.canApplyTo(Proof proof,
ImmutableList<Goal> goals,
PosInOccurrence posInOcc)
Can this macro be applied on the given goals?
This method should not make any changes but check if the macro can be
applied or not on the given goals.
|
boolean |
FullInformationFlowAutoPilotMacro.canApplyTo(Proof proof,
ImmutableList<Goal> goals,
PosInOccurrence posInOcc)
Can this macro be applied on the given goals?
This method should not make any changes but check if the macro can be
applied or not on the given goals.
|
boolean |
FinishAuxiliaryBlockComputationMacro.canApplyTo(Proof proof,
ImmutableList<Goal> goals,
PosInOccurrence posInOcc) |
boolean |
StartAuxiliaryMethodComputationMacro.canApplyTo(Proof proof,
ImmutableList<Goal> goals,
PosInOccurrence posInOcc) |
boolean |
ExhaustiveProofMacro.canApplyTo(Proof proof,
ImmutableList<Goal> goals,
PosInOccurrence posInOcc) |
boolean |
FinishAuxiliaryMethodComputationMacro.canApplyTo(Proof proof,
ImmutableList<Goal> goals,
PosInOccurrence posInOcc) |
protected Strategy |
SelfcompositionStateExpansionMacro.createStrategy(Proof proof,
PosInOccurrence posInOcc) |
protected UseInformationFlowContractMacro.PropExpansionStrategy |
UseInformationFlowContractMacro.createStrategy(Proof proof,
PosInOccurrence posInOcc) |
protected void |
UseInformationFlowContractMacro.doPostProcessing(Proof proof) |
protected void |
AbstractFinishAuxiliaryComputationMacro.mergeNamespaces(Proof initiatingProof,
Proof sideProof)
Merge namespaces.
|
Modifier and Type | Method and Description |
---|---|
Proof |
AbstractInfFlowPO.createProof(java.lang.String proofName,
Term poTerm,
InitConfig proofConfig) |
Modifier and Type | Class and Description |
---|---|
class |
InfFlowProof
The proof object used by Information Flow Proofs.
|
Modifier and Type | Method and Description |
---|---|
Proof |
Services.getProof()
Returns the proof to which this object belongs, or null if it does not
belong to any proof.
|
Modifier and Type | Method and Description |
---|---|
Services |
Services.copyProofSpecific(Proof p_proof,
boolean shareCaches) |
void |
Services.setProof(Proof p_proof)
Marks this services as proof specific
Please make sure that the
Services does not not yet belong to an existing proof
or that it is owned by a proof environment. |
Modifier and Type | Method and Description |
---|---|
ProofMacroFinishedInfo |
FinishSymbolicExecutionUntilMergePointMacro.applyTo(UserInterfaceControl uic,
Proof proof,
ImmutableList<Goal> goals,
PosInOccurrence posInOcc,
ProverTaskListener listener) |
ProofMacroFinishedInfo |
SequentialOnLastGoalProofMacro.applyTo(UserInterfaceControl uic,
Proof proof,
ImmutableList<Goal> goals,
PosInOccurrence posInOcc,
ProverTaskListener listener)
Apply this macro on the given goals.
|
ProofMacroFinishedInfo |
SequentialProofMacro.applyTo(UserInterfaceControl uic,
Proof proof,
ImmutableList<Goal> goals,
PosInOccurrence posInOcc,
ProverTaskListener listener)
Apply this macro on the given goals.
|
ProofMacroFinishedInfo |
ProofMacro.applyTo(UserInterfaceControl uic,
Proof proof,
ImmutableList<Goal> goals,
PosInOccurrence posInOcc,
ProverTaskListener listener)
Apply this macro on the given goals.
|
ProofMacroFinishedInfo |
AlternativeMacro.applyTo(UserInterfaceControl uic,
Proof proof,
ImmutableList<Goal> goals,
PosInOccurrence posInOcc,
ProverTaskListener listener)
Apply this macro on the given goals.
|
ProofMacroFinishedInfo |
TryCloseMacro.applyTo(UserInterfaceControl uic,
Proof proof,
ImmutableList<Goal> goals,
PosInOccurrence posInOcc,
ProverTaskListener listener) |
ProofMacroFinishedInfo |
StrategyProofMacro.applyTo(UserInterfaceControl uic,
Proof proof,
ImmutableList<Goal> goals,
PosInOccurrence posInOcc,
ProverTaskListener listener) |
ProofMacroFinishedInfo |
DoWhileFinallyMacro.applyTo(UserInterfaceControl uic,
Proof proof,
ImmutableList<Goal> goals,
PosInOccurrence posInOcc,
ProverTaskListener listener) |
ProofMacroFinishedInfo |
AbstractBlastingMacro.applyTo(UserInterfaceControl uic,
Proof proof,
ImmutableList<Goal> goals,
PosInOccurrence posInOcc,
ProverTaskListener listener) |
ProofMacroFinishedInfo |
SkipMacro.applyTo(UserInterfaceControl uic,
Proof proof,
ImmutableList<Goal> goals,
PosInOccurrence posInOcc,
ProverTaskListener listener) |
boolean |
WellDefinednessMacro.canApplyTo(Proof proof,
ImmutableList<Goal> goals,
PosInOccurrence posInOcc) |
boolean |
SequentialProofMacro.canApplyTo(Proof proof,
ImmutableList<Goal> goals,
PosInOccurrence posInOcc)
Can this macro be applied on the given goals?
This method should not make any changes but check if the macro can be
applied or not on the given goals.
|
boolean |
ProofMacro.canApplyTo(Proof proof,
ImmutableList<Goal> goals,
PosInOccurrence posInOcc)
Can this macro be applied on the given goals?
This method should not make any changes but check if the macro can be
applied or not on the given goals.
|
boolean |
AlternativeMacro.canApplyTo(Proof proof,
ImmutableList<Goal> goals,
PosInOccurrence posInOcc)
Can this macro be applied on the given goals?
This method should not make any changes but check if the macro can be
applied or not on the given goals.
|
boolean |
TryCloseMacro.canApplyTo(Proof proof,
ImmutableList<Goal> goals,
PosInOccurrence posInOcc) |
boolean |
StrategyProofMacro.canApplyTo(Proof proof,
ImmutableList<Goal> goals,
PosInOccurrence posInOcc)
Can this macro be applied on the given goals?
This method should not make any changes but check if the macro can be
applied or not on the given goals.
|
boolean |
DoWhileFinallyMacro.canApplyTo(Proof proof,
ImmutableList<Goal> goals,
PosInOccurrence posInOcc) |
boolean |
SkipMacro.canApplyTo(Proof proof,
ImmutableList<Goal> goals,
PosInOccurrence posInOcc) |
protected Strategy |
FinishSymbolicExecutionMacro.createStrategy(Proof proof,
PosInOccurrence posInOcc) |
protected Strategy |
AbstractPropositionalExpansionMacro.createStrategy(Proof proof,
PosInOccurrence posInOcc) |
protected Strategy |
PrepareInfFlowContractPreBranchesMacro.createStrategy(Proof proof,
PosInOccurrence posInOcc) |
protected Strategy |
FinishSymbolicExecutionUntilMergePointMacro.createStrategy(Proof proof,
PosInOccurrence posInOcc) |
protected Strategy |
WellDefinednessMacro.createStrategy(Proof proof,
PosInOccurrence posInOcc) |
protected Strategy |
AutoPilotPrepareProofMacro.createStrategy(Proof proof,
PosInOccurrence posInOcc) |
protected abstract Strategy |
StrategyProofMacro.createStrategy(Proof proof,
PosInOccurrence posInOcc) |
protected Strategy |
AutoMacro.createStrategy(Proof proof,
PosInOccurrence posInOcc) |
protected Strategy |
OneStepProofMacro.createStrategy(Proof proof,
PosInOccurrence posInOcc) |
protected Strategy |
AbstractBlastingMacro.createStrategy(Proof proof,
PosInOccurrence posInOcc) |
protected Strategy |
TestGenMacro.createStrategy(Proof proof,
PosInOccurrence posInOcc) |
protected void |
FinishSymbolicExecutionUntilMergePointMacro.doPostProcessing(Proof proof) |
protected void |
StrategyProofMacro.doPostProcessing(Proof proof)
Subclasses can use this method to do some postprocessing on the
proof-object after the strategy has finished.
|
static ProofMacroFinishedInfo |
ProofMacroFinishedInfo.getDefaultInfo(ProofMacro macro,
Proof proof) |
protected int |
AbstractProofMacro.getMaxSteps(Proof proof)
Gets the maximum number of rule applications allowed for a macro.
|
Constructor and Description |
---|
ProofMacroFinishedInfo(ProofMacro macro,
Proof proof) |
ProofMacroFinishedInfo(ProofMacro macro,
Proof proof,
boolean cancelled) |
RemovePostStrategy(Proof proof) |
Modifier and Type | Field and Description |
---|---|
protected Proof |
AbstractCommand.proof |
Modifier and Type | Method and Description |
---|---|
Proof |
EngineState.getProof() |
Modifier and Type | Method and Description |
---|---|
void |
ProofScriptEngine.execute(AbstractUserInterfaceControl uiControl,
Proof proof) |
Constructor and Description |
---|
EngineState(Proof proof) |
JavascriptInterface(Proof proof,
EngineState state) |
Modifier and Type | Method and Description |
---|---|
Proof |
ProofAggregate.getFirstProof() |
Proof |
ProofAggregate.getProof(int proofNum) |
Proof[] |
SingleProof.getProofs() |
Proof[] |
CompoundProof.getProofs() |
abstract Proof[] |
ProofAggregate.getProofs() |
Proof |
ProofEvent.getSource()
the proof from where this even to originated
|
Proof |
ProofTreeEvent.getSource() |
Proof |
Goal.proof()
returns the proof the goal belongs to
|
Proof |
Node.proof()
returns the proof the Node belongs to
|
Modifier and Type | Method and Description |
---|---|
static <S extends SVSubstitute,T> |
ReplacementMap.create(TermFactory tf,
Proof proof)
Creates a new replacement map.
|
static <S extends SVSubstitute,T> |
ReplacementMap.create(TermFactory tf,
Proof proof,
java.util.Map<S,T> initialMappings)
Creates a new replacement map.
|
static ProofAggregate |
ProofAggregate.createProofAggregate(Proof[] proofs,
java.lang.String name) |
static ProofAggregate |
ProofAggregate.createProofAggregate(Proof proof,
java.lang.String name) |
static Term |
OpReplacer.replace(Operator toReplace,
Operator with,
Term in,
TermFactory tf,
Proof proof)
Replace an operator.
|
static ImmutableList<Term> |
OpReplacer.replace(Term toReplace,
Term with,
ImmutableList<Term> in,
TermFactory tf,
Proof proof)
Replace a sub-term.
|
static Term |
OpReplacer.replace(Term toReplace,
Term with,
Term in,
TermFactory tf,
Proof proof)
Replace a sub-term.
|
void |
ProofVisitor.visit(Proof proof,
Node visitedNode) |
Constructor and Description |
---|
Node(Proof proof)
creates an empty node that is root and leaf.
|
Node(Proof proof,
Sequent seq)
creates a node with the given contents
|
Node(Proof proof,
Sequent seq,
Node parent)
creates a node with the given contents, the given collection of children (all
elements must be of class Node) and the given parent node.
|
OpReplacer(java.util.Map<? extends SVSubstitute,? extends SVSubstitute> map,
TermFactory tf,
Proof proof)
Creates an
OpReplacer . |
ProofEvent(Proof source)
creates a new proof event the interactive prover where the event initially
occured
|
ProofEvent(Proof source,
RuleAppInfo rai,
ImmutableList<Goal> newGoals)
creates a proof event for a change triggered by a rule applications
|
ProofTreeEvent(Proof source)
Create ProofTreeEvent for an event that happens at
no particular node.
|
ProofTreeEvent(Proof source,
Goal goal)
Create ProofTreeEvent for the event that happened to the
given goal
|
ProofTreeEvent(Proof source,
ImmutableList<Goal> goals)
Create ProofTreeEvent for the event that affects the goals
given in the list.
|
ProofTreeEvent(Proof source,
Node node)
Create ProofTreeEvent for an event that happens at
the specified node.
|
SingleProof(Proof p,
java.lang.String name) |
Modifier and Type | Method and Description |
---|---|
static java.util.LinkedHashSet<IProofReference<?>> |
ProofReferenceUtil.computeProofReferences(Proof proof)
|
static java.util.LinkedHashSet<IProofReference<?>> |
ProofReferenceUtil.computeProofReferences(Proof proof,
ImmutableList<IProofReferencesAnalyst> analysts)
|
Modifier and Type | Method and Description |
---|---|
Proof |
DefaultProofReference.getSource()
Returns the source
Proof . |
Proof |
IProofReference.getSource()
Returns the source
Proof . |
Modifier and Type | Method and Description |
---|---|
Proof |
DelayedCut.getProof() |
Constructor and Description |
---|
DelayedCut(Proof proof,
Node node,
Term formula,
ImmutableList<Node> subtrees,
int sideOfDecisionPredicate,
RuleApp firstAppliedRuleApp) |
DelayedCutProcessor(Proof proof,
Node node,
Term descisionPredicate,
int mode) |
Modifier and Type | Method and Description |
---|---|
Proof |
ProofDisposedEvent.getSource() |
Constructor and Description |
---|
ProofDisposedEvent(Proof source)
Constructor.
|
Modifier and Type | Method and Description |
---|---|
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) |
Modifier and Type | Method and Description |
---|---|
static java.util.Set<Term> |
AbstractOperationPO.getAdditionalUninterpretedPredicates(Proof proof)
Returns the uninterpreted predicate used in the given
Proof if available. |
static Term |
AbstractOperationPO.getUninterpretedPredicate(Proof proof)
Returns the uninterpreted predicate used in the given
Proof if available. |
Modifier and Type | Field and Description |
---|---|
protected Proof |
OutputStreamProofSaver.proof |
Modifier and Type | Method and Description |
---|---|
Proof |
AbstractProblemLoader.getProof()
Returns the instantiate proof or
null if no proof was instantiated during loading process. |
Modifier and Type | Method and Description |
---|---|
static java.io.File |
OutputStreamProofSaver.getJavaSourceLocation(Proof proof)
Extracts java source directory from
header() , if it exists. |
static Term |
IntermediateProofReplayer.parseTerm(java.lang.String value,
Proof proof)
Parses a given term in String representation.
|
static Term |
IntermediateProofReplayer.parseTerm(java.lang.String value,
Proof proof,
Namespace<QuantifiableVariable> varNS,
Namespace<IProgramVariable> progVarNS,
Namespace<Function> functNS)
Parses a given term in String representation.
|
void |
AutoSaver.setProof(Proof p)
Set the proof to be saved.
|
protected void |
AbstractProblemLoader.setProof(Proof proof) |
Constructor and Description |
---|
GZipProofSaver(Proof proof,
java.lang.String fileName,
java.lang.String internalVersion)
Instantiates a new proof saver.
|
IntermediatePresentationProofFileParser(Proof proof) |
IntermediateProofReplayer(AbstractProblemLoader loader,
Proof proof,
de.uka.ilkd.key.proof.io.IntermediatePresentationProofFileParser.Result parserResult)
Constructs a new
IntermediateProofReplayer . |
OutputStreamProofSaver(Proof proof) |
OutputStreamProofSaver(Proof proof,
java.lang.String internalVersion) |
ProofBundleSaver(Proof proof,
java.io.File saveFile)
Creates a new ProofBundleSaver.
|
ProofSaver(Proof proof,
java.io.File file) |
ProofSaver(Proof proof,
java.io.File file,
java.lang.String internalVersion) |
ProofSaver(Proof proof,
java.lang.String fileName,
java.lang.String internalVersion) |
Modifier and Type | Method and Description |
---|---|
protected java.util.Set<Proof> |
AbstractFileRepo.getRegisteredProofs() |
Modifier and Type | Method and Description |
---|---|
void |
AbstractFileRepo.registerProof(Proof proof) |
void |
TrivialFileRepo.registerProof(Proof proof) |
void |
FileRepo.registerProof(Proof proof)
Register the proof in the FileRepo.
|
Modifier and Type | Method and Description |
---|---|
PredicateEstimator.Result |
PredicateEstimator.estimate(ProspectivePartner partner,
Proof proof) |
Constructor and Description |
---|
JoinProcessor(ProspectivePartner partner,
Proof proof) |
Modifier and Type | Method and Description |
---|---|
Proof[] |
EnvNode.allProofs() |
Proof[] |
ProofAggregateTask.allProofs() |
Proof[] |
BasicTask.allProofs()
returns all proofs attached to this basic task
|
Proof[] |
TaskTreeNode.allProofs() |
Proof |
EnvNode.proof() |
Proof |
ProofAggregateTask.proof() |
Proof |
BasicTask.proof() |
Proof |
TaskTreeNode.proof() |
Modifier and Type | Method and Description |
---|---|
ImmutableSet<Proof> |
SpecificationRepository.getAllProofs()
Returns all proofs registered with this specification repository.
|
ImmutableSet<Proof> |
SpecificationRepository.getProofs(Contract atomicContract)
Returns all proofs registered for the passed atomic contract, or for
combined contracts including the passed atomic contract
|
ImmutableSet<Proof> |
SpecificationRepository.getProofs(KeYJavaType kjt,
IObserverFunction target)
Returns all proofs registered for the passed target and its overriding
targets.
|
ImmutableSet<Proof> |
SpecificationRepository.getProofs(ProofOblInput po)
Returns all proofs registered for the passed PO (or stronger POs).
|
Modifier and Type | Method and Description |
---|---|
ContractPO |
SpecificationRepository.getContractPOForProof(Proof proof)
Returns the PO that the passed proof is about, or null.
|
ContractPO |
SpecificationRepository.getPOForProof(Proof proof) |
ProofOblInput |
SpecificationRepository.getProofOblInput(Proof proof)
Returns the
ProofOblInput from which the given Proof was
created. |
IObserverFunction |
SpecificationRepository.getTargetOfProof(Proof proof)
Returns the target that the passed proof is about, or null.
|
TaskTreeNode |
TaskTreeModel.getTaskForProof(Proof p) |
void |
SpecificationRepository.registerProof(ProofOblInput po,
Proof proof)
Registers the passed proof.
|
void |
SpecificationRepository.removeProof(Proof proof)
Unregisters the passed proof.
|
Constructor and Description |
---|
ProofCorrectnessMgt(Proof p) |
Constructor and Description |
---|
NodeChangeJournal(Proof p_proof,
Goal p_goal) |
Modifier and Type | Method and Description |
---|---|
Proof |
TaskFinishedInfo.getProof() |
Modifier and Type | Method and Description |
---|---|
java.lang.String |
StopCondition.getGoalNotAllowedMessage(int maxApplications,
long timeout,
Proof proof,
long startTime,
int countApplied,
Goal goal)
Returns the reason why the previous check via
#isGoalAllowed(ApplyStrategy, int, long, Proof, GoalChooser, long, int, Goal)
has stopped the apply strategy. |
int |
StopCondition.getMaximalWork(int maxApplications,
long timeout,
Proof proof)
Returns the maximal amount of work needed to complete the task,
used to display a progress bar.
|
java.lang.String |
StopCondition.getStopMessage(int maxApplications,
long timeout,
Proof proof,
long startTime,
int countApplied,
SingleRuleApplicationInfo singleRuleApplicationInfo)
Returns a human readable message which explains why the previous
#shouldStop(ApplyStrategy, Proof, GoalChooser, long, int, SingleRuleApplicationInfo)
has stopped the strategy. |
void |
GoalChooser.init(Proof p_proof,
ImmutableList<Goal> p_goals)
Initialise this DefaultGoalChooser for use with a given Proof and a list of goals.
|
boolean |
StopCondition.isGoalAllowed(int maxApplications,
long timeout,
Proof proof,
long startTime,
int countApplied,
Goal goal)
Checks if it is allowed to apply the next rule on the selected
Goal
chosen by the GoalChooser before it is applied. |
boolean |
StopCondition.shouldStop(int maxApplications,
long timeout,
Proof proof,
long startTime,
int countApplied,
SingleRuleApplicationInfo singleRuleApplicationInfo)
Checks after each applied rule if more rules should be applied or if the strategy should stop.
|
ApplyStrategyInfo |
ProverCore.start(Proof proof,
Goal goal)
starts a proof search for a given goals using the given strategy settings
instead the ones configures in the proof
|
ApplyStrategyInfo |
ProverCore.start(Proof proof,
ImmutableList<Goal> goals)
starts a proof search for a set of goals using the given strategy settings
instead the ones configures in the proof
|
ApplyStrategyInfo |
ProverCore.start(Proof proof,
ImmutableList<Goal> goals,
int maxSteps,
long timeout,
boolean stopAtFirstNonCloseableGoal)
This entry point to the proof may provide inconsistent data.
|
ApplyStrategyInfo |
ProverCore.start(Proof proof,
ImmutableList<Goal> goals,
StrategySettings stratSet)
starts a proof search for a set of goals using the given strategy settings
instead the ones configures in the proof
|
Modifier and Type | Field and Description |
---|---|
protected Proof |
DefaultGoalChooser.proof
the proof that is worked with
|
Modifier and Type | Method and Description |
---|---|
Proof |
DefaultTaskFinishedInfo.getProof() |
Proof |
ApplyStrategyInfo.getProof() |
Modifier and Type | Method and Description |
---|---|
java.lang.String |
AppliedRuleStopCondition.getGoalNotAllowedMessage(int maxApplications,
long timeout,
Proof proof,
long startTime,
int countApplied,
Goal goal)
Returns the reason why the previous check via
#isGoalAllowed(ApplyStrategy, int, long, Proof, GoalChooser, long, int, Goal)
has stopped the apply strategy. |
int |
AppliedRuleStopCondition.getMaximalWork(int maxApplications,
long timeout,
Proof proof)
Returns the maximal amount of work needed to complete the task,
used to display a progress bar.
|
java.lang.String |
AppliedRuleStopCondition.getStopMessage(int maxApplications,
long timeout,
Proof proof,
long startTime,
int countApplied,
SingleRuleApplicationInfo singleRuleApplicationInfo)
Returns a human readable message which explains why the previous
#shouldStop(ApplyStrategy, Proof, GoalChooser, long, int, SingleRuleApplicationInfo)
has stopped the strategy. |
void |
DefaultGoalChooser.init(Proof p_proof,
ImmutableList<Goal> p_goals) |
boolean |
AppliedRuleStopCondition.isGoalAllowed(int maxApplications,
long timeout,
Proof proof,
long startTime,
int countApplied,
Goal goal)
Checks if it is allowed to apply the next rule on the selected
Goal
chosen by the GoalChooser before it is applied. |
boolean |
AppliedRuleStopCondition.shouldStop(int maxApplications,
long timeout,
Proof proof,
long startTime,
int countApplied,
SingleRuleApplicationInfo singleRuleApplicationInfo)
Checks after each applied rule if more rules should be applied or if the strategy should stop.
|
ApplyStrategyInfo |
ApplyStrategy.start(Proof proof,
Goal goal) |
ApplyStrategyInfo |
ApplyStrategy.start(Proof proof,
ImmutableList<Goal> goals) |
ApplyStrategyInfo |
ApplyStrategy.start(Proof proof,
ImmutableList<Goal> goals,
int maxSteps,
long timeout,
boolean stopAtFirstNonCloseableGoal) |
ApplyStrategyInfo |
ApplyStrategy.start(Proof proof,
ImmutableList<Goal> goals,
StrategySettings stratSet) |
Constructor and Description |
---|
ApplyStrategyInfo(java.lang.String message,
Proof proof,
java.lang.Throwable error,
Goal nonCloseableGoal,
long timeInMillis,
int appliedRuleAppsCount,
int nrClosedGoals) |
DefaultTaskFinishedInfo(java.lang.Object source,
java.lang.Object result,
Proof proof,
long time,
int appliedRules,
int closedGoals) |
Modifier and Type | Method and Description |
---|---|
static void |
OneStepSimplifier.refreshOSS(Proof proof)
Enables or disables the one step simplification, depending on the
strategy setting made.
|
Modifier and Type | Method and Description |
---|---|
Proof |
SMTSettings.getProof() |
Constructor and Description |
---|
SMTSettings(ProofDependentSMTSettings pdSettings,
ProofIndependentSMTSettings piSettings,
NewSMTTranslationSettings newTransSettings,
Proof proof) |
Modifier and Type | Method and Description |
---|---|
static java.util.Collection<SMTProblem> |
SMTProblem.createSMTProblems(Proof proof)
Creates out of a proof object several SMT problems.
|
Modifier and Type | Method and Description |
---|---|
protected abstract Proof |
AbstractCounterExampleGenerator.createProof(UserInterfaceControl ui,
Proof oldProof,
Sequent oldSequent,
java.lang.String proofName)
Creates a new
Proof . |
protected Proof |
AbstractSideProofCounterExampleGenerator.createProof(UserInterfaceControl ui,
Proof oldProof,
Sequent oldSequent,
java.lang.String proofName)
Creates a new
Proof . |
Modifier and Type | Method and Description |
---|---|
protected abstract Proof |
AbstractCounterExampleGenerator.createProof(UserInterfaceControl ui,
Proof oldProof,
Sequent oldSequent,
java.lang.String proofName)
Creates a new
Proof . |
protected Proof |
AbstractSideProofCounterExampleGenerator.createProof(UserInterfaceControl ui,
Proof oldProof,
Sequent oldSequent,
java.lang.String proofName)
Creates a new
Proof . |
protected abstract SolverLauncherListener |
AbstractCounterExampleGenerator.createSolverListener(SMTSettings settings,
Proof proof)
Creates the
SolverLauncherListener which handles the results
of the launched SMT solver. |
void |
AbstractCounterExampleGenerator.searchCounterExample(UserInterfaceControl ui,
Proof oldProof,
Sequent oldSequent)
Searches a counter example for the given
Sequent . |
Modifier and Type | Method and Description |
---|---|
protected Proof |
AbstractTestGenerator.createProof(UserInterfaceControl ui,
Proof oldProof,
java.lang.String newName,
Sequent newSequent) |
protected Proof |
AbstractTestGenerator.getOriginalProof() |
Modifier and Type | Method and Description |
---|---|
protected java.util.List<Proof> |
AbstractTestGenerator.getProofs() |
Modifier and Type | Method and Description |
---|---|
protected Proof |
AbstractTestGenerator.createProof(UserInterfaceControl ui,
Proof oldProof,
java.lang.String newName,
Sequent newSequent) |
protected void |
AbstractTestGenerator.generateFiles(java.util.Collection<SMTSolver> problemSolvers,
TestGenerationLog log,
Proof originalProof) |
protected void |
AbstractTestGenerator.informAboutNoTestResults(SolverLauncher launcher,
java.util.Collection<SMTSolver> problemSolvers,
TestGenerationLog log,
Proof originalProof)
This method is used in the Eclipse world to show a dialog with the log.
|
protected void |
AbstractTestGenerator.selectProof(UserInterfaceControl ui,
Proof proof) |
Constructor and Description |
---|
AbstractTestGenerator(UserInterfaceControl ui,
Proof originalProof)
Constructor.
|
Modifier and Type | Method and Description |
---|---|
protected Proof |
AbstractFeatureStrategy.getProof() |
Modifier and Type | Method and Description |
---|---|
Strategy |
StrategyFactory.create(Proof proof,
StrategyProperties strategyProperties)
Create strategy for a proof.
|
Strategy |
FIFOStrategy.Factory.create(Proof proof,
StrategyProperties properties) |
Strategy |
JavaCardDLStrategyFactory.create(Proof proof,
StrategyProperties strategyProperties) |
static void |
Strategy.updateStrategySettings(Proof proof,
StrategyProperties p)
Updates the
Strategy for the given Proof by setting the
Strategy 's StrategyProperties to the given ones. |
Constructor and Description |
---|
AbstractFeatureStrategy(Proof proof) |
JavaCardDLStrategy(Proof proof,
StrategyProperties strategyProperties) |
Modifier and Type | Method and Description |
---|---|
Proof |
SymbolicExecutionTreeBuilder.getProof()
Returns the
Proof from which the symbolic execution tree is extracted. |
Proof |
ExecutionNodeReader.AbstractKeYlessExecutionElement.getProof()
Returns the
Proof from which the symbolic execution tree was extracted. |
protected Proof |
AbstractUpdateExtractor.getProof()
|
Modifier and Type | Method and Description |
---|---|
protected java.util.List<ImmutableSet<Term>> |
SymbolicLayoutExtractor.extractAppliedCutsFromGoals(Proof proof)
Extracts the possible memory layouts from the given side proof.
|
Constructor and Description |
---|
SymbolicExecutionTreeBuilder(Proof proof,
boolean mergeBranchConditions,
boolean useUnicode,
boolean usePrettyPrinting,
boolean variablesAreOnlyComputedFromUpdates,
boolean simplifyConditions)
Constructor.
|
Modifier and Type | Method and Description |
---|---|
Proof |
IExecutionElement.getProof()
Returns the
Proof from which the symbolic execution tree was extracted. |
Modifier and Type | Method and Description |
---|---|
Proof |
AbstractExecutionElement.getProof()
Returns the
Proof from which the symbolic execution tree was extracted. |
Modifier and Type | Method and Description |
---|---|
static boolean |
SymbolicExecutionJavaProfile.isTruthValueTracingEnabled(Proof proof)
Checks if truth value evaluation is enabled in the given
Proof . |
Modifier and Type | Method and Description |
---|---|
Strategy |
SymbolicExecutionStrategy.Factory.create(Proof proof,
StrategyProperties sp)
Create strategy for a proof.
|
Strategy |
SimplifyTermStrategy.Factory.create(Proof proof,
StrategyProperties sp)
Create strategy for a proof.
|
java.lang.String |
StepReturnSymbolicExecutionTreeNodesStopCondition.getGoalNotAllowedMessage(int maxApplications,
long timeout,
Proof proof,
long startTime,
int countApplied,
Goal goal)
Returns the reason why the previous check via
#isGoalAllowed(ApplyStrategy, int, long, Proof, GoalChooser, long, int, Goal)
has stopped the apply strategy. |
java.lang.String |
StepOverSymbolicExecutionTreeNodesStopCondition.getGoalNotAllowedMessage(int maxApplications,
long timeout,
Proof proof,
long startTime,
int countApplied,
Goal goal)
Returns the reason why the previous check via
#isGoalAllowed(ApplyStrategy, int, long, Proof, GoalChooser, long, int, Goal)
has stopped the apply strategy. |
java.lang.String |
CompoundStopCondition.getGoalNotAllowedMessage(int maxApplications,
long timeout,
Proof proof,
long startTime,
int countApplied,
Goal goal)
Returns the reason why the previous check via
#isGoalAllowed(ApplyStrategy, int, long, Proof, GoalChooser, long, int, Goal)
has stopped the apply strategy. |
java.lang.String |
ExecutedSymbolicExecutionTreeNodesStopCondition.getGoalNotAllowedMessage(int maxApplications,
long timeout,
Proof proof,
long startTime,
int countApplied,
Goal goal)
Returns the reason why the previous check via
#isGoalAllowed(ApplyStrategy, int, long, Proof, GoalChooser, long, int, Goal)
has stopped the apply strategy. |
java.lang.String |
BreakpointStopCondition.getGoalNotAllowedMessage(int maxApplications,
long timeout,
Proof proof,
long startTime,
int countApplied,
Goal goal)
Returns the reason why the previous check via
#isGoalAllowed(ApplyStrategy, int, long, Proof, GoalChooser, long, int, Goal)
has stopped the apply strategy. |
int |
CompoundStopCondition.getMaximalWork(int maxApplications,
long timeout,
Proof proof)
Returns the maximal amount of work needed to complete the task,
used to display a progress bar.
|
int |
ExecutedSymbolicExecutionTreeNodesStopCondition.getMaximalWork(int maxApplications,
long timeout,
Proof proof)
Returns the maximal amount of work needed to complete the task,
used to display a progress bar.
|
int |
SymbolicExecutionBreakpointStopCondition.getMaximalWork(int maxApplications,
long timeout,
Proof proof)
Returns the maximal amount of work needed to complete the task,
used to display a progress bar.
|
int |
AbstractCallStackBasedStopCondition.getMaximalWork(int maxApplications,
long timeout,
Proof proof)
Returns the maximal amount of work needed to complete the task,
used to display a progress bar.
|
int |
BreakpointStopCondition.getMaximalWork(int maxApplications,
long timeout,
Proof proof)
Returns the maximal amount of work needed to complete the task,
used to display a progress bar.
|
java.lang.String |
CompoundStopCondition.getStopMessage(int maxApplications,
long timeout,
Proof proof,
long startTime,
int countApplied,
SingleRuleApplicationInfo singleRuleApplicationInfo)
Returns a human readable message which explains why the previous
#shouldStop(ApplyStrategy, Proof, GoalChooser, long, int, SingleRuleApplicationInfo)
has stopped the strategy. |
java.lang.String |
ExecutedSymbolicExecutionTreeNodesStopCondition.getStopMessage(int maxApplications,
long timeout,
Proof proof,
long startTime,
int countApplied,
SingleRuleApplicationInfo singleRuleApplicationInfo)
Returns a human readable message which explains why the previous
#shouldStop(ApplyStrategy, Proof, GoalChooser, long, int, SingleRuleApplicationInfo)
has stopped the strategy. |
java.lang.String |
AbstractCallStackBasedStopCondition.getStopMessage(int maxApplications,
long timeout,
Proof proof,
long startTime,
int countApplied,
SingleRuleApplicationInfo singleRuleApplicationInfo)
Returns a human readable message which explains why the previous
#shouldStop(ApplyStrategy, Proof, GoalChooser, long, int, SingleRuleApplicationInfo)
has stopped the strategy. |
java.lang.String |
BreakpointStopCondition.getStopMessage(int maxApplications,
long timeout,
Proof proof,
long startTime,
int countApplied,
SingleRuleApplicationInfo singleRuleApplicationInfo)
Returns a human readable message which explains why the previous
#shouldStop(ApplyStrategy, Proof, GoalChooser, long, int, SingleRuleApplicationInfo)
has stopped the strategy. |
protected void |
ExecutedSymbolicExecutionTreeNodesStopCondition.handleNodeLimitExceeded(int maxApplications,
long timeout,
Proof proof,
long startTime,
int countApplied,
Goal goal,
Node node,
RuleApp ruleApp,
java.lang.Integer executedNumberOfSetNodes)
Handles the state that the node limit is exceeded.
|
protected void |
ExecutedSymbolicExecutionTreeNodesStopCondition.handleNodeLimitNotExceeded(int maxApplications,
long timeout,
Proof proof,
long startTime,
int countApplied,
Goal goal,
Node node,
RuleApp ruleApp,
java.lang.Integer executedNumberOfSetNodes)
Handles the state that the node limit is not exceeded.
|
protected void |
SymbolicExecutionBreakpointStopCondition.handleNodeLimitNotExceeded(int maxApplications,
long timeout,
Proof proof,
long startTime,
int countApplied,
Goal goal,
Node node,
RuleApp ruleApp,
java.lang.Integer executedNumberOfSetNodes)
Handles the state that the node limit is not exceeded.
|
void |
SymbolicExecutionGoalChooser.init(Proof p_proof,
ImmutableList<Goal> p_goals)
Initialise this DefaultGoalChooser for use with a given Proof and a list of goals.
|
protected boolean |
SymbolicExecutionBreakpointStopCondition.isBreakpointHit(SourceElement activeStatement,
RuleApp ruleApp,
Proof proof,
Node node)
Checks if a breakpoint is hit.
|
protected boolean |
BreakpointStopCondition.isBreakpointHit(SourceElement activeStatement,
RuleApp ruleApp,
Proof proof,
Node node)
Checks if a breakpoint is hit.
|
boolean |
CompoundStopCondition.isGoalAllowed(int maxApplications,
long timeout,
Proof proof,
long startTime,
int countApplied,
Goal goal)
Checks if it is allowed to apply the next rule on the selected
Goal
chosen by the GoalChooser before it is applied. |
boolean |
ExecutedSymbolicExecutionTreeNodesStopCondition.isGoalAllowed(int maxApplications,
long timeout,
Proof proof,
long startTime,
int countApplied,
Goal goal)
Checks if it is allowed to apply the next rule on the selected
Goal
chosen by the GoalChooser before it is applied. |
boolean |
SymbolicExecutionBreakpointStopCondition.isGoalAllowed(int maxApplications,
long timeout,
Proof proof,
long startTime,
int countApplied,
Goal goal)
Checks if it is allowed to apply the next rule on the selected
Goal
chosen by the GoalChooser before it is applied. |
boolean |
AbstractCallStackBasedStopCondition.isGoalAllowed(int maxApplications,
long timeout,
Proof proof,
long startTime,
int countApplied,
Goal goal)
Checks if it is allowed to apply the next rule on the selected
Goal
chosen by the GoalChooser before it is applied. |
boolean |
BreakpointStopCondition.isGoalAllowed(int maxApplications,
long timeout,
Proof proof,
long startTime,
int countApplied,
Goal goal)
Checks if it is allowed to apply the next rule on the selected
Goal
chosen by the GoalChooser before it is applied. |
boolean |
CompoundStopCondition.shouldStop(int maxApplications,
long timeout,
Proof proof,
long startTime,
int countApplied,
SingleRuleApplicationInfo singleRuleApplicationInfo)
Checks after each applied rule if more rules should be applied or if the strategy should stop.
|
boolean |
ExecutedSymbolicExecutionTreeNodesStopCondition.shouldStop(int maxApplications,
long timeout,
Proof proof,
long startTime,
int countApplied,
SingleRuleApplicationInfo singleRuleApplicationInfo)
Checks after each applied rule if more rules should be applied or if the strategy should stop.
|
boolean |
AbstractCallStackBasedStopCondition.shouldStop(int maxApplications,
long timeout,
Proof proof,
long startTime,
int countApplied,
SingleRuleApplicationInfo singleRuleApplicationInfo)
Checks after each applied rule if more rules should be applied or if the strategy should stop.
|
boolean |
BreakpointStopCondition.shouldStop(int maxApplications,
long timeout,
Proof proof,
long startTime,
int countApplied,
SingleRuleApplicationInfo singleRuleApplicationInfo)
Checks after each applied rule if more rules should be applied or if the strategy should stop.
|
Modifier and Type | Method and Description |
---|---|
Proof |
AbstractBreakpoint.getProof() |
Modifier and Type | Method and Description |
---|---|
protected boolean |
AbstractConditionalBreakpoint.conditionMet(RuleApp ruleApp,
Proof proof,
Node node)
Checks if the condition, that was given by the user, evaluates to true with the current of the proof
|
protected boolean |
KeYWatchpoint.conditionMet(RuleApp ruleApp,
Proof proof,
Node node) |
boolean |
AbstractHitCountBreakpoint.isBreakpointHit(SourceElement activeStatement,
RuleApp ruleApp,
Proof proof,
Node node)
Determines if the breakpoint represented by this BreakpointStopConition is triggered.
|
boolean |
AbstractConditionalBreakpoint.isBreakpointHit(SourceElement activeStatement,
RuleApp ruleApp,
Proof proof,
Node node)
Determines if the breakpoint represented by this BreakpointStopConition is triggered.
|
boolean |
SymbolicExecutionExceptionBreakpoint.isBreakpointHit(SourceElement activeStatement,
RuleApp ruleApp,
Proof proof,
Node node)
Determines if the breakpoint represented by this BreakpointStopConition is triggered.
|
boolean |
ExceptionBreakpoint.isBreakpointHit(SourceElement activeStatement,
RuleApp ruleApp,
Proof proof,
Node node)
Determines if the breakpoint represented by this BreakpointStopConition is triggered.
|
boolean |
FieldWatchpoint.isBreakpointHit(SourceElement activeStatement,
RuleApp ruleApp,
Proof proof,
Node node)
Determines if the breakpoint represented by this BreakpointStopConition is triggered.
|
boolean |
IBreakpoint.isBreakpointHit(SourceElement activeStatement,
RuleApp ruleApp,
Proof proof,
Node node)
Determines if the breakpoint represented by this BreakpointStopConition is triggered.
|
boolean |
KeYWatchpoint.isBreakpointHit(SourceElement activeStatement,
RuleApp ruleApp,
Proof proof,
Node node) |
boolean |
MethodBreakpoint.isBreakpointHit(SourceElement activeStatement,
RuleApp ruleApp,
Proof proof,
Node node) |
boolean |
LineBreakpoint.isBreakpointHit(SourceElement activeStatement,
RuleApp ruleApp,
Proof proof,
Node node) |
void |
AbstractConditionalBreakpoint.updateState(int maxApplications,
long timeout,
Proof proof,
long startTime,
int countApplied,
Goal goal)
This method is called from
StopCondition.isGoalAllowed(int, long, Proof, long, int, Goal)
and can be used to update the state of the IBreakpoint . |
void |
SymbolicExecutionExceptionBreakpoint.updateState(int maxApplications,
long timeout,
Proof proof,
long startTime,
int countApplied,
Goal goal)
This method is called from
StopCondition.isGoalAllowed(int, long, Proof, long, int, Goal)
and can be used to update the state of the IBreakpoint . |
void |
IBreakpoint.updateState(int maxApplications,
long timeout,
Proof proof,
long startTime,
int countApplied,
Goal goal)
This method is called from
StopCondition.isGoalAllowed(int, long, Proof, long, int, Goal)
and can be used to update the state of the IBreakpoint . |
void |
AbstractBreakpoint.updateState(int maxApplications,
long timeout,
Proof proof,
long startTime,
int countApplied,
Goal goal)
This method is called from
StopCondition.isGoalAllowed(int, long, Proof, long, int, Goal)
and can be used to update the state of the IBreakpoint . |
Constructor and Description |
---|
AbstractBreakpoint(Proof proof,
boolean enabled)
Constructor.
|
AbstractConditionalBreakpoint(int hitCount,
IProgramMethod pm,
Proof proof,
boolean enabled,
boolean conditionEnabled,
int methodStart,
int methodEnd,
KeYJavaType containerType)
Creates a new
AbstractConditionalBreakpoint . |
AbstractHitCountBreakpoint(int hitCount,
Proof proof,
boolean enabled)
Creates a new
AbstractHitCountBreakpoint . |
ExceptionBreakpoint(Proof proof,
java.lang.String exceptionName,
boolean caught,
boolean uncaught,
boolean suspendOnSubclasses,
boolean enabled,
int hitCount)
Creates a new
AbstractHitCountBreakpoint . |
FieldWatchpoint(boolean enabled,
int hitCount,
java.lang.String fieldName,
boolean isAcces,
boolean isModification,
KeYJavaType containerKJT,
Proof proof)
Creates a new
FieldWatchpoint . |
KeYWatchpoint(int hitCount,
Proof proof,
java.lang.String condition,
boolean enabled,
boolean conditionEnabled,
KeYJavaType containerType,
boolean suspendOnTrue)
Creates a new
AbstractConditionalBreakpoint . |
LineBreakpoint(java.lang.String classPath,
int lineNumber,
int hitCount,
IProgramMethod pm,
Proof proof,
java.lang.String condition,
boolean enabled,
boolean conditionEnabled,
int methodStart,
int methodEnd)
Creates a new
LineBreakpoint . |
MethodBreakpoint(java.lang.String classPath,
int lineNumber,
int hitCount,
IProgramMethod pm,
Proof proof,
java.lang.String condition,
boolean enabled,
boolean conditionEnabled,
int methodStart,
int methodEnd,
boolean isEntry,
boolean isExit)
Creates a new
LineBreakpoint . |
SymbolicExecutionExceptionBreakpoint(Proof proof,
java.lang.String exceptionName,
boolean caught,
boolean uncaught,
boolean suspendOnSubclasses,
boolean enabled,
int hitCount)
Creates a new
AbstractHitCountBreakpoint . |
Modifier and Type | Method and Description |
---|---|
Proof |
SideProofStore.Entry.getProof()
Returns the
Proof . |
Proof |
SymbolicExecutionEnvironment.getProof()
Returns the
Proof of SymbolicExecutionEnvironment.getBuilder() . |
Modifier and Type | Method and Description |
---|---|
void |
SideProofStore.addProof(java.lang.String description,
Proof proof)
Adds a new
Proof . |
static ProofEnvironment |
SymbolicExecutionSideProofUtil.cloneProofEnvironmentWithOwnOneStepSimplifier(Proof source,
boolean useSimplifyTermProfile)
Creates a copy of the
ProofEnvironment of the given Proof
which has his own OneStepSimplifier instance. |
static java.util.List<Pair<Term,Node>> |
SymbolicExecutionSideProofUtil.computeResults(Services services,
Proof proof,
ProofEnvironment sideProofEnvironment,
Sequent sequentToProve,
TermLabel label,
java.lang.String description,
java.lang.String methodTreatment,
java.lang.String loopTreatment,
java.lang.String queryTreatment,
java.lang.String splittingOption,
boolean addNamesToServices)
Starts the side proof and extracts the result
Term . |
static java.util.List<Triple<Term,java.util.Set<Term>,Node>> |
SymbolicExecutionSideProofUtil.computeResultsAndConditions(Services services,
Proof proof,
ProofEnvironment sideProofEnvironment,
Sequent sequentToProve,
Operator operator,
java.lang.String description,
java.lang.String methodTreatment,
java.lang.String loopTreatment,
java.lang.String queryTreatment,
java.lang.String splittingOption,
boolean addNamesToServices)
Starts the side proof and extracts the result
Term and conditions. |
static void |
SymbolicExecutionEnvironment.configureProofForSymbolicExecution(Proof proof,
int maximalNumberOfNodesPerBranch)
Configures the given
Proof to use the symbolic execution strategy
by reusing the default StrategyProperties . |
static void |
SymbolicExecutionEnvironment.configureProofForSymbolicExecution(Proof proof,
int maximalNumberOfNodesPerBranch,
boolean methodTreatmentContract,
boolean loopTreatmentInvariant,
boolean blockTreatmentContract,
boolean nonExecutionBranchHidingSideProofs,
boolean aliasChecks)
Configures the given
Proof to use the symbolic execution strategy. |
boolean |
SideProofStore.containsEntry(Proof proof)
Checks if an
SideProofStore.Entry for the given Proof exist. |
static NotationInfo |
SymbolicExecutionUtil.createNotationInfo(Proof proof)
Creates the
NotationInfo for the given Proof . |
static IProgramVariable |
SymbolicExecutionUtil.extractExceptionVariable(Proof proof)
Extracts the exception variable which is used to check if the executed program in proof terminates normally.
|
SideProofStore.Entry |
SideProofStore.getEntry(Proof proof)
Returns the
SideProofStore.Entry for the given Proof . |
static boolean |
SymbolicExecutionUtil.isWeakeningGoalEnabled(Proof proof)
Checks if the weakening goal is enabled or not.
|
static Term |
SymbolicExecutionUtil.simplify(InitConfig initConfig,
Proof parentProof,
Term term)
Simplifies the given
Term in a side proof. |
static Term |
SymbolicExecutionUtil.simplify(Proof parentProof,
Term term)
Simplifies the given
Term in a side proof. |
static ApplyStrategyInfo |
SymbolicExecutionSideProofUtil.startSideProof(Proof proof,
ProofEnvironment sideProofEnvironment,
Sequent sequentToProve)
Starts a site proof for the given
Sequent . |
static ApplyStrategyInfo |
SymbolicExecutionSideProofUtil.startSideProof(Proof proof,
ProofEnvironment sideProofEnvironment,
Sequent sequentToProve,
java.lang.String methodTreatment,
java.lang.String loopTreatment,
java.lang.String queryTreatment,
java.lang.String splittingOption)
Starts a site proof for the given
Sequent . |
static ApplyStrategyInfo |
SymbolicExecutionSideProofUtil.startSideProof(Proof proof,
ProofStarter starter,
java.lang.String methodTreatment,
java.lang.String loopTreatment,
java.lang.String queryTreatment,
java.lang.String splittingOption)
Starts a site proof.
|
static void |
SymbolicExecutionUtil.updateStrategySettings(Proof proof,
boolean useOperationContracts,
boolean useLoopInvariants,
boolean nonExecutionBranchHidingSideProofs,
boolean aliasChecksImmediately)
Configures the proof to use the given settings.
|
static void |
SymbolicExecutionUtil.updateStrategySettings(Proof proof,
StrategyProperties sp)
Configures the proof to use the given
StrategyProperties . |
Constructor and Description |
---|
Entry(java.lang.String description,
Proof proof)
Constructor.
|
Modifier and Type | Method and Description |
---|---|
abstract ProofOblInput |
TacletLoader.getTacletFile(Proof proof)
subclasses give a special proof obligation input per proof.
|
ProofOblInput |
TacletLoader.TacletFromFileLoader.getTacletFile(Proof proof) |
ProofOblInput |
TacletLoader.KeYsTacletsLoader.getTacletFile(Proof proof) |
void |
AutomaticProver.start(Proof proof,
int maxNumberOfRules,
long timeout)
Starts the prover with the following parameters.
|
Constructor and Description |
---|
ProofInfo(Proof proof) |
TestCaseGenerator(Proof proof) |
TestCaseGenerator(Proof proof,
boolean rflAsInternalClass) |
Modifier and Type | Method and Description |
---|---|
boolean |
MediatorProofControl.isAutoModeSupported(Proof proof)
Checks if the auto mode of this
UserInterfaceControl supports the given Proof . |
protected void |
AbstractMediatorUserInterfaceControl.macroSideProofDisposing(ProofMacroFinishedInfo initiatingInfo,
Proof initiatingProof,
Proof sideProof) |
static boolean |
ConsoleUserInterfaceControl.saveProof(java.lang.Object result,
Proof proof,
java.io.File keyProblemFile)
Save proof.
|
void |
MediatorProofControl.startAutoMode(Proof proof,
ImmutableList<Goal> goals,
ProverTaskListener ptl) |
Modifier and Type | Method and Description |
---|---|
Proof |
ProofStarter.getProof()
Returns the managed side
Proof . |
Proof[] |
ProofUserManager.getProofs()
Returns all registered
Proof s. |
Proof[] |
ProofUserManager.getProofs(KeYEnvironment<?> environment)
Returns all known
Proof s of the given KeYEnvironment . |
Modifier and Type | Method and Description |
---|---|
void |
ProofUserManager.addUser(Proof proof,
KeYEnvironment<?> environment,
java.lang.Object user)
Registers the
Proof with the given user if it is not already
registered. |
static ProofEnvironment |
SideProofUtil.cloneProofEnvironmentWithOwnOneStepSimplifier(Proof source,
Choice... enableChoices)
Creates a copy of the
ProofEnvironment of the given Proof
which has his own OneStepSimplifier instance. |
Term |
HelperClassForTests.extractProblemTerm(Proof p) |
static OneStepSimplifier |
MiscTools.findOneStepSimplifier(Proof proof)
Returns the
OneStepSimplifier used in the given Proof . |
KeYEnvironment<?> |
ProofUserManager.getEnvironment(Proof proof)
Returns the known environment of the given
Proof . |
java.lang.Object[] |
ProofUserManager.getUsers(Proof proof)
Returns all registered user of the given
Proof . |
void |
ProofStarter.init(Proof proof) |
static boolean |
HelperClassForTests.isOneStepSimplificationEnabled(Proof proof)
Checks if one step simplification is enabled in the given
Proof . |
void |
ProofUserManager.removeUserAndDispose(Proof proof,
java.lang.Object user)
Removes the user from the registered proof users.
|
static void |
HelperClassForTests.setOneStepSimplificationEnabled(Proof proof,
boolean enabled)
Defines if one step simplification is enabled in general and within the
Proof . |
Modifier and Type | Method and Description |
---|---|
static Term |
MergeRuleUtils.trySimplify(Proof parentProof,
Term term,
boolean countDisjunctions,
int timeout)
Tries to simplifies the given
Term in a side proof with splits. |
Modifier and Type | Method and Description |
---|---|
java.util.concurrent.atomic.AtomicInteger |
ExplorationModeModel.get(Proof p)
Return the number of tainted exploration nodes in a Proof
|
Constructor and Description |
---|
ProofExplorationService(Proof proof,
Services services) |
Modifier and Type | Method and Description |
---|---|
Proof |
ExplorationStepsList.getProof() |
Modifier and Type | Method and Description |
---|---|
void |
ExplorationStepsList.setProof(Proof proof)
Sets the shown proof.
|
Modifier and Type | Method and Description |
---|---|
InteractionLog |
InteractionRecorder.get(Proof proof) |
void |
InteractionRecorder.registerOnSettings(Proof proof) |
void |
InteractionRecorder.runAutoMode(java.util.List<Node> initialGoals,
Proof proof,
ApplyStrategyInfo info) |
void |
InteractionRecorder.settingChanged(Proof proof,
Settings settings,
InteractionListener.SettingType type,
java.lang.String message) |
Modifier and Type | Method and Description |
---|---|
java.util.Optional<Node> |
NodeIdentifier.findNode(Proof proof) |
Node |
NodeInteraction.getNode(Proof proof) |
Constructor and Description |
---|
InteractionLog(Proof proof) |
Copyright © 2003-2019 The KeY-Project.