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>)
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:
<resultCondition> -> <something> = <result>
or <resultCondition> -> <result> = <something>
or<resultCondition> & <something> = <result>
or <resultCondition> & <result> = <something>
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 ModalitySideProofRule |
INSTANCE
The singleton instance of this class.
|
private static Name |
NAME
The
Name of this rule. |
Modifier | Constructor and Description |
---|---|
private |
ModalitySideProofRule()
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.
|
Name |
name()
the name of the rule
|
java.lang.String |
toString() |
computeResultsAndConditions, createResultConstant, createResultFunction, isApplicableOnSubTerms, replace
public static final ModalitySideProofRule INSTANCE
private ModalitySideProofRule()
public boolean isApplicable(Goal goal, PosInOccurrence pio)
public 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