de.uka.ilkd.key.symbolic_execution.util

Class SymbolicExecutionSideProofUtil

java.lang.Object

de.uka.ilkd.key.symbolic_execution.util.SymbolicExecutionSideProofUtil

public final class SymbolicExecutionSideProofUtil
extends java.lang.Object

Provides utility methods for side proofs.

Author:

Martin Hentschel

Nested Class Summary

Nested Classes

Modifier and Type	Class and Description
protected static class	SymbolicExecutionSideProofUtil.ContainsIrrelevantThingsVisitor Utility class used by QuerySideProofRule#containsIrrelevantThings(Services, SequentFormula, Set).
protected static class	SymbolicExecutionSideProofUtil.ContainsModalityOrQueryVisitor Utility method used by QuerySideProofRule#containsModalityOrQuery(Term).

Constructor Summary

Constructors

Modifier	Constructor and Description
private	SymbolicExecutionSideProofUtil() Forbid instances.

Method Summary

Modifier and Type	Method and Description
static void	addNewNamesToNamespace(Services services, Term term) Makes sure that all used Names in the given Term are registered in the Namespaces of the given Services.
static ProofEnvironment	cloneProofEnvironmentWithOwnOneStepSimplifier(InitConfig sourceInitConfig, boolean useSimplifyTermProfile) Creates a copy of the ProofEnvironment of the given Proof which has his own OneStepSimplifier instance.
static ProofEnvironment	cloneProofEnvironmentWithOwnOneStepSimplifier(Proof source, boolean useSimplifyTermProfile) Creates a copy of the ProofEnvironment of the given Proof which has his own OneStepSimplifier instance.
static Sequent	computeGeneralSequentToProve(Sequent goalSequent, SequentFormula currentSF) Computes a general Sequent to prove in a side proof which contains all SequentFormula of the original Sequent except the given current SequentFormula and those which contains modalities and queries.
static java.util.List<Pair<Term,Node>>	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>>	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.
private static Term	constructResultIfContained(Services services, SequentFormula sf, Operator operator)
private static Term	constructResultIfContained(Services services, Term term, Operator operator)
static boolean	containsIrrelevantThings(Services services, SequentFormula sf, java.util.Set<Operator> relevantThings) Checks if the given SequentFormula contains irrelevant things (things which are not contained in the relevantThingsToProve and are no Java types)
static boolean	containsModalityOrQuery(SequentFormula sf) Checks if the given SequentFormula contains a modality or query.
static boolean	containsModalityOrQuery(Term term) Checks if the given Term contains a modality or query.
static ProofStarter	createSideProof(ProofEnvironment sideProofEnvironment, Sequent sequentToProve, java.lang.String proofName) Creates a new ProofStarter which contains a new site proof of the given Proof.
static void	disposeOrStore(java.lang.String description, ApplyStrategyInfo info) Stores or disposes the Proof of the ApplyStrategyInfo in SideProofStore.DEFAULT_INSTANCE.
static Term	extractOperatorTerm(ApplyStrategyInfo info, Operator operator) Extracts the operator term for the formula with the given Operator from the site proof result (ApplyStrategyInfo).
static Term	extractOperatorTerm(Goal goal, Operator operator) Extracts the operator term for the formula with the given Operator from the given Goal.
static Term	extractOperatorTerm(Node node, Operator operator) Extracts the operator term for the formula with the given Operator from the given Node.
static Term	extractOperatorValue(Goal goal, Operator operator) Extracts the value for the formula with the given Operator from the given Goal.
static Term	extractOperatorValue(Node node, Operator operator) Extracts the value for the formula with the given Operator from the given Node.
static java.util.Set<Operator>	extractRelevantThings(Services services, Sequent sequentToProve) Extracts all Operators from the given Sequent which represents relevant things.
static boolean	isIrrelevantCondition(Services services, Sequent initialSequent, java.util.Set<Operator> relevantThingsInSequentToProve, SequentFormula sf) Checks if the given SequentFormula is a relevant condition.
private static boolean	isOperatorASequentFormula(Sequent sequent, Operator operator)
protected static boolean	isRelevantThing(Services services, Term term) Checks if the given Term describes a relevant thing.
static ApplyStrategyInfo	startSideProof(Proof proof, ProofEnvironment sideProofEnvironment, Sequent sequentToProve) Starts a site proof for the given Sequent.
static ApplyStrategyInfo	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	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.

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Constructor Detail

SymbolicExecutionSideProofUtil

private SymbolicExecutionSideProofUtil()

Forbid instances.

Method Detail

computeGeneralSequentToProve

public static Sequent computeGeneralSequentToProve(Sequent goalSequent,
                                                   SequentFormula currentSF)

Computes a general Sequent to prove in a side proof which contains all SequentFormula of the original Sequent except the given current SequentFormula and those which contains modalities and queries.

Parameters:

goalSequent - The original Sequent of the current Goal.

currentSF - The SequentFormula to ignore.

Returns:

The general initial Sequent.

computeResults

public static java.util.List<Pair<Term,Node>> 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)
                                                      throws ProofInputException

Starts the side proof and extracts the result Term.

New used names are automatically added to the Namespace of the Services.

Parameters:

services - The Services to use.

proof - The Proof from on which the side proof si performed.

sideProofEnvironment - The given ProofEnvironment of the side proof.

sequentToProve - The Sequent to prove in a side proof.

label - The TermLabel which is used to compute the result.

description - The side proof description.

splittingOption - The splitting options to use.

addNamesToServices - true defines that used names in result and conditions are added to the namespace of the given Services, false means that names are not added.

Returns:

The found result Term and the conditions.

Throws:

ProofInputException - Occurred Exception.

computeResultsAndConditions

public static java.util.List<Triple<Term,java.util.Set<Term>,Node>> 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)
                                                                                         throws ProofInputException

Starts the side proof and extracts the result Term and conditions.

New used names are automatically added to the Namespace of the Services.

Parameters:

services - The Services to use.

proof - The Proof from on which the side proof si performed.

sideProofEnvironment - The given ProofEnvironment of the side proof.

sequentToProve - The Sequent to prove in a side proof.

operator - The Operator which is used to compute the result.

description - The side proof description.

splittingOption - The splitting options to use.

addNamesToServices - true defines that used names in result and conditions are added to the namespace of the given Services, false means that names are not added.

Returns:

The found result Term and the conditions.

Throws:

ProofInputException - Occurred Exception.

constructResultIfContained

private static Term constructResultIfContained(Services services,
                                               SequentFormula sf,
                                               Operator operator)

constructResultIfContained

private static Term constructResultIfContained(Services services,
                                               Term term,
                                               Operator operator)

isOperatorASequentFormula

private static boolean isOperatorASequentFormula(Sequent sequent,
                                                 Operator operator)

addNewNamesToNamespace

public static void addNewNamesToNamespace(Services services,
                                          Term term)

Makes sure that all used Names in the given Term are registered in the Namespaces of the given Services.

Parameters:

services - The Services to use.

term - The Term to check its Names.

containsModalityOrQuery

public static boolean containsModalityOrQuery(SequentFormula sf)

Checks if the given SequentFormula contains a modality or query.

Parameters:

sf - The SequentFormula to check.

Returns:

true contains at least one modality or query, false contains no modalities and no queries.

containsModalityOrQuery

public static boolean containsModalityOrQuery(Term term)

Checks if the given Term contains a modality or query.

Parameters:

term - The Term to check.

Returns:

true contains at least one modality or query, false contains no modalities and no queries.

extractRelevantThings

public static java.util.Set<Operator> extractRelevantThings(Services services,
                                                            Sequent sequentToProve)

Extracts all Operators from the given Sequent which represents relevant things.

Parameters:

services - The Services to use.

sequentToProve - The Sequent to extract relevant things from.

Returns:

The found relevant things.

isRelevantThing

protected static boolean isRelevantThing(Services services,
                                         Term term)

Checks if the given Term describes a relevant thing. Relevant things are:

• IProgramVariable
• Functions of type Heap
• Functions of a Java type

Parameters:

services - The Services to use.

term - The Term to check.

Returns:

true is relevant thing, false is not relevant.

isIrrelevantCondition

public static boolean isIrrelevantCondition(Services services,
                                            Sequent initialSequent,
                                            java.util.Set<Operator> relevantThingsInSequentToProve,
                                            SequentFormula sf)

Checks if the given SequentFormula is a relevant condition.

Parameters:

services - The Services to use.

initialSequent - The initial Sequent of the side proof.

relevantThingsInSequentToProve - The relevant things found in the initial Sequent.

sf - The SequentFormula to check.

Returns:

true SequentFormula is relevant condition, false SequentFormula is not a relevant condition.

containsIrrelevantThings

public static boolean containsIrrelevantThings(Services services,
                                               SequentFormula sf,
                                               java.util.Set<Operator> relevantThings)

Checks if the given SequentFormula contains irrelevant things (things which are not contained in the relevantThingsToProve and are no Java types)

Parameters:

services - The Services to use.

sf - The SequentFormula to check.

relevantThings - The relevant things.

Returns:

true The SequentFormula contains irrelevant things, false the SequentFormula contains no irrelevant things.

startSideProof

public static ApplyStrategyInfo startSideProof(Proof proof,
                                               ProofEnvironment sideProofEnvironment,
                                               Sequent sequentToProve)
                                        throws ProofInputException

Starts a site proof for the given Sequent.

Parameters:

proof - The parent Proof of the site proof to do.

sideProofEnvironment - The given ProofEnvironment of the side proof.

sequentToProve - The Sequent to prove.

Returns:

The proof result represented as ApplyStrategyInfo instance.

Throws:

ProofInputException - Occurred Exception

startSideProof

public static ApplyStrategyInfo startSideProof(Proof proof,
                                               ProofEnvironment sideProofEnvironment,
                                               Sequent sequentToProve,
                                               java.lang.String methodTreatment,
                                               java.lang.String loopTreatment,
                                               java.lang.String queryTreatment,
                                               java.lang.String splittingOption)
                                        throws ProofInputException

Starts a site proof for the given Sequent.

Parameters:

proof - The parent Proof of the site proof to do.

sideProofEnvironment - The given ProofEnvironment of the side proof.

sequentToProve - The Sequent to prove.

Returns:

The proof result represented as ApplyStrategyInfo instance.

Throws:

ProofInputException - Occurred Exception

createSideProof

public static ProofStarter createSideProof(ProofEnvironment sideProofEnvironment,
                                           Sequent sequentToProve,
                                           java.lang.String proofName)
                                    throws ProofInputException

Creates a new ProofStarter which contains a new site proof of the given Proof.

Parameters:

sideProofEnvironment - The given ProofEnvironment of the side proof.

sequentToProve - The Sequent to proof in a new site proof.

proofName - An optional name for the newly created Proof.

Returns:

The created ProofStarter with the site proof.

Throws:

ProofInputException - Occurred Exception.

startSideProof

public static ApplyStrategyInfo 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.

Parameters:

proof - The original Proof.

starter - The ProofStarter with the site proof.

splittingOption - The splitting option to use.

Returns:

The site proof result.

extractOperatorValue

public static Term extractOperatorValue(Goal goal,
                                        Operator operator)

Extracts the value for the formula with the given Operator from the given Goal.

Parameters:

goal - The Goal to search the Operator in.

operator - The Operator for the formula which should be extracted.

Returns:

The value of the formula with the given Operator.

extractOperatorValue

public static Term extractOperatorValue(Node node,
                                        Operator operator)

Extracts the value for the formula with the given Operator from the given Node.

Parameters:

node - The Node to search the Operator in.

operator - The Operator for the formula which should be extracted.

Returns:

The value of the formula with the given Operator.

extractOperatorTerm

public static Term extractOperatorTerm(ApplyStrategyInfo info,
                                       Operator operator)
                                throws ProofInputException

Extracts the operator term for the formula with the given Operator from the site proof result (ApplyStrategyInfo).

Parameters:

info - The site proof result.

operator - The Operator for the formula which should be extracted.

Returns:

The operator term of the formula with the given Operator.

Throws:

ProofInputException - Occurred Exception.

extractOperatorTerm

public static Term extractOperatorTerm(Goal goal,
                                       Operator operator)

Extracts the operator term for the formula with the given Operator from the given Goal.

Parameters:

goal - The Goal to search the Operator in.

operator - The Operator for the formula which should be extracted.

Returns:

The operator term of the formula with the given Operator.

extractOperatorTerm

public static Term extractOperatorTerm(Node node,
                                       Operator operator)

Extracts the operator term for the formula with the given Operator from the given Node.

Parameters:

node - The Node to search the Operator in.

operator - The Operator for the formula which should be extracted.

Returns:

The operator term of the formula with the given Operator.

cloneProofEnvironmentWithOwnOneStepSimplifier

public static ProofEnvironment cloneProofEnvironmentWithOwnOneStepSimplifier(Proof source,
                                                                             boolean useSimplifyTermProfile)

Creates a copy of the ProofEnvironment of the given Proof which has his own OneStepSimplifier instance. Such copies are required for instance during parallel usage of site proofs because OneStepSimplifier has an internal state.

Parameters:

source - The Proof to copy its ProofEnvironment.

Returns:

The created ProofEnvironment which is a copy of the environment of the given Proof but with its own OneStepSimplifier instance.

cloneProofEnvironmentWithOwnOneStepSimplifier

public static ProofEnvironment cloneProofEnvironmentWithOwnOneStepSimplifier(InitConfig sourceInitConfig,
                                                                             boolean useSimplifyTermProfile)

Creates a copy of the ProofEnvironment of the given Proof which has his own OneStepSimplifier instance. Such copies are required for instance during parallel usage of site proofs because OneStepSimplifier has an internal state.

Parameters:

sourceInitConfig - The InitConfig to copy its ProofEnvironment.

Returns:

The created ProofEnvironment which is a copy of the environment of the given Proof but with its own OneStepSimplifier instance.

disposeOrStore

public static void disposeOrStore(java.lang.String description,
                                  ApplyStrategyInfo info)

Stores or disposes the Proof of the ApplyStrategyInfo in SideProofStore.DEFAULT_INSTANCE.

This method should be called whenever a side proof is no longer needed and should be disposed or stored for debugging purposes.

Parameters:

description - The description.

info - The ApplyStrategyInfo to store or dispose its Proof.