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.
|
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
clone, equals, finalize, getClass, hashCode, notify, notifyAll, wait, wait, wait
getOrigin
public static final ModalitySideProofRule INSTANCE
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
Copyright © 2003-2019 The KeY-Project.