de.uka.ilkd.key.symbolic_execution.rule

Class ModalitySideProofRule

java.lang.Object

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

de.uka.ilkd.key.symbolic_execution.rule.ModalitySideProofRule

All Implemented Interfaces:

BuiltInRule, Rule

public class ModalitySideProofRule
extends AbstractSideProofRule

A BuiltInRule which evaluates a modality in a side proof.

This rule is applicable on top level terms (SequentFormula) of the form.

• {...}\[...\](<something> = <var>) or
• {...}\<...\>(<something> = <var>) or
• {...}\[...\](<var> = <something>) or
• {...}\<...\>(<var> = <something>)

The leading updates are optional and any Modality is supported.

The original SequentFormula which contains the equality is always removed in the following Goal. 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>

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 ModalitySideProofRule	INSTANCE The singleton instance of this class.
private static Name	NAME The Name of this rule.

Constructor Summary

Constructors

Modifier	Constructor and Description
private	ModalitySideProofRule() 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.
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, isApplicableOnSubTerms, replace

Methods inherited from class java.lang.Object

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

Field Detail

INSTANCE

public static final ModalitySideProofRule INSTANCE

The singleton instance of this class.

NAME

private static final Name NAME

The Name of this rule.

Constructor Detail

ModalitySideProofRule

private ModalitySideProofRule()

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)

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