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.
|
private static Name |
NAME
The
Name of this rule. |
Modifier | Constructor and Description |
---|---|
private |
QuerySideProofRule()
Constructor to forbid multiple instances.
|
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
public static final QuerySideProofRule INSTANCE
private QuerySideProofRule()
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