de.uka.ilkd.key.symbolic_execution.rule

Class QuerySideProofRule

java.lang.Object

de.uka.ilkd.key.symbolic_execution.rule.AbstractSideProofRule

de.uka.ilkd.key.symbolic_execution.rule.QuerySideProofRule

All Implemented Interfaces:

BuiltInRule, Rule

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:

1. top level <something> = <query> or <query> = <something>
   For each possible result value is a SequentFormula added to the Sequent of the form:
   • Antecedent: <resultCondition> -> <something> = <result> or
   • Antecedent: <resultCondition> -> <result> = <something> or
   • Succedent: <resultCondition> & <something> = <result> or
   • Succedent: <resultCondition> & <result> = <something>
2. right side of an implication on top level <queryCondition> -> <something> = <query> or <queryCondition> -> <query> = <something>
   For each possible result value is a SequentFormula added to the Sequent of the form:
   • Antecedent: <pre> -> (<resultCondition> -> <something> = <result>) or
   • Antecedent: <pre> -> (<resultCondition> -> <result> = <something>) or
   • Succedent: <pre> -> (<resultCondition> & <something> = <result>) or
   • Succedent: <pre> -> (<resultCondition> & <result> = <something>)
3. everywhere else ...(<something> = <query>)... or ...(<query> = <something>)...
   In the original 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

The side proof uses the default side proof settings (splitting = delayed) and is started via 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.

Author:

Martin Hentschel

Field Summary

Fields

Modifier and Type	Field and Description
static QuerySideProofRule	INSTANCE The singleton instance of this class.
private static Name	NAME The Name of this rule.

Constructor Summary

Constructors

Modifier	Constructor and Description
private	QuerySideProofRule() Constructor to forbid multiple instances.

Method Summary

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()

Methods inherited from class de.uka.ilkd.key.symbolic_execution.rule.AbstractSideProofRule

computeResultsAndConditions, createResultConstant, createResultFunction, replace

Methods inherited from class java.lang.Object

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

Field Detail

INSTANCE

public static final QuerySideProofRule INSTANCE

The singleton instance of this class.

NAME

private static final Name NAME

The Name of this rule.

Constructor Detail

QuerySideProofRule

private QuerySideProofRule()

Constructor to forbid multiple instances.

Method Detail

isApplicable

public boolean isApplicable(Goal goal,
                            PosInOccurrence pio)

returns true iff a rule is applicable at the given position. This does not necessarily mean that a rule application will change the goal (this decision is made due to performance reasons)

isApplicableQuery

protected boolean isApplicableQuery(Goal goal,
                                    Term pmTerm,
                                    PosInOccurrence pio)

Checks if the query term is supported. The functionality is identical to QueryExpand.isApplicable(Goal, PosInOccurrence).

Parameters:

goal - The Goal.

pmTerm - The Term to with the query to check.

pio - The PosInOccurrence in the Goal.

Returns:

true is applicable, false is not applicable

createApp

public IBuiltInRuleApp createApp(PosInOccurrence pos,
                                 TermServices services)

apply

public ImmutableList<Goal> apply(Goal goal,
                                 Services services,
                                 RuleApp ruleApp)
                          throws RuleAbortException

the rule is applied on the given goal using the information of rule application.

Parameters:

goal - the Goal on which to apply ruleApp

services - the Services with the necessary information about the java programs

ruleApp - the rule application to be executed

Returns:

all open goals below \old(goal.node()), i.e. the goals resulting from the rule application

Throws:

RuleAbortException

name

public Name name()

the name of the rule

displayName

public java.lang.String displayName()

returns the display name of the rule

toString

public java.lang.String toString()

Overrides:

toString in class java.lang.Object

isApplicableOnSubTerms

public boolean isApplicableOnSubTerms()

Specified by:

isApplicableOnSubTerms in interface BuiltInRule

Overrides:

isApplicableOnSubTerms in class AbstractSideProofRule