public final class QuerySideProofRule extends AbstractSideProofRule
A BuiltInRule
which evaluates a query in a side proof.
This rule is applicable on each equality which contains a query:
...(<something> = <query>)...
or...(<query> = <something>)...
The original SequentFormula
which contains the equality is always
removed in the following Goal
. How the result of the query computed
in the side proof is represented depends on the occurrence of the equality:
<something> = <query>
or <query> = <something>
SequentFormula
added to the Sequent
of the form:
<resultCondition> -> <something> = <result>
or <resultCondition> -> <result> = <something>
or<resultCondition> & <something> = <result>
or <resultCondition> & <result> = <something>
<queryCondition> -> <something> = <query>
or <queryCondition> -> <query> = <something>
SequentFormula
added to the Sequent
of the form:
<pre> -> (<resultCondition> -> <something> = <result>)
or <pre> -> (<resultCondition> -> <result> = <something>)
or<pre> -> (<resultCondition> & <something> = <result>)
or <pre> -> (<resultCondition> & <result> = <something>)
...(<something> = <query>)...
or ...(<query> = <something>)...
SequentFormula
is the <query>
replaced by a new constant function named QueryResult
and added to the antecedent/succedent in which it was contained before.
For each possible result value is an additional SequentFormula
added to the antecedent of the form:
<resultCondition> -> QueryResult = <result>
or <resultCondition> -> <result> = QueryResult
SymbolicExecutionUtil#startSideProof(de.uka.ilkd.key.proof.Proof, Sequent, String)
.
In case that at least one result branch has applicable rules an exception is thrown and the rule is aborted.
Modifier and Type | Field and Description |
---|---|
static QuerySideProofRule |
INSTANCE
The singleton instance of this class.
|
Modifier and Type | Method and Description |
---|---|
ImmutableList<Goal> |
apply(Goal goal,
Services services,
RuleApp ruleApp)
the rule is applied on the given goal using the
information of rule application.
|
IBuiltInRuleApp |
createApp(PosInOccurrence pos,
TermServices services) |
java.lang.String |
displayName()
returns the display name of the rule
|
boolean |
isApplicable(Goal goal,
PosInOccurrence pio)
returns true iff a rule is applicable at the given
position.
|
boolean |
isApplicableOnSubTerms() |
protected boolean |
isApplicableQuery(Goal goal,
Term pmTerm,
PosInOccurrence pio)
Checks if the query term is supported.
|
Name |
name()
the name of the rule
|
java.lang.String |
toString() |
computeResultsAndConditions, createResultConstant, createResultFunction, replace
clone, equals, finalize, getClass, hashCode, notify, notifyAll, wait, wait, wait
getOrigin
public static final QuerySideProofRule INSTANCE
public boolean isApplicable(Goal goal, PosInOccurrence pio)
protected boolean isApplicableQuery(Goal goal, Term pmTerm, PosInOccurrence pio)
QueryExpand.isApplicable(Goal, PosInOccurrence)
.goal
- The Goal
.pmTerm
- The Term
to with the query to check.pio
- The PosInOccurrence
in the Goal
.true
is applicable, false
is not applicablepublic IBuiltInRuleApp createApp(PosInOccurrence pos, TermServices services)
public ImmutableList<Goal> apply(Goal goal, Services services, RuleApp ruleApp) throws RuleAbortException
goal
- the Goal on which to apply ruleAppservices
- the Services with the necessary information
about the java programsruleApp
- the rule application to be executedRuleAbortException
public Name name()
public java.lang.String displayName()
public java.lang.String toString()
toString
in class java.lang.Object
public boolean isApplicableOnSubTerms()
isApplicableOnSubTerms
in interface BuiltInRule
isApplicableOnSubTerms
in class AbstractSideProofRule
Copyright © 2003-2019 The KeY-Project.