public class LoopScopeInvariantRule extends AbstractLoopInvariantRule
Implementation of the "loop scope invariant" rule as proposed in the PhD thesis by Nathan Wasser.
Basically, the preserves and use case part are combined in one formula; the
loop is transformed to an if statement including a trailing continue, and
wrapped in an "indexed loop scope". The index of the loop scope, a
ProgramVariable
, will be set to TRUE if the loop is left and to FALSE
if it isn't.
Thus, all cases of loop exit, as breaks, returns, "pure" leaving and exceptional behavior, are handled (with some very simple additional taclets setting the index variable according to the situation, thereby eliminating the loop scope).
Important Note: The rule currently does not support (i)
Information Flow proof obligations, (ii) Java Card transactions and (iii) the
wellformedness check. For these things, you currently still have to use the
old WhileInvariantRule
. In the (near) future, these features should
be built in of course..
\Gamma ==> {U}Inv, \Delta \Gamma, {U'}Inv ==> \Delta, {U'}[\pi boolean x = true; loop-scope(x){ if(nse) l: { p x = false; } } \omega] ((x = TRUE -> \phi) & (x = FALSE -> Inv)) ---------------------------------------------------------- loopInvariant \Gamma ==> {U}[\pi l: while (nse) { p } \omega]\phi, Delta
AbstractLoopInvariantRule.AdditionalHeapTerms, AbstractLoopInvariantRule.AnonUpdateData, AbstractLoopInvariantRule.Instantiation, AbstractLoopInvariantRule.LoopInvariantInformation
Modifier and Type | Field and Description |
---|---|
static java.lang.String |
FULL_INVARIANT_TERM_HINT
The hint used to refactor the full invariant.
|
static java.lang.String |
INITIAL_INVARIANT_ONLY_HINT
The hint used to refactor the initial invariant.
|
static LoopScopeInvariantRule |
INSTANCE
The Singleton instance of
LoopScopeInvariantRule . |
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.
|
int |
getNrOfGoals() |
boolean |
isApplicable(Goal goal,
PosInOccurrence pio)
NOTE: The
LoopScopeInvariantRule currently
doesn't support Java Card transactions and information flow proof
obligations. |
Name |
name()
the name of the rule
|
and, conjunctFreeInv, conjunctInv, createAdditionalHeapTerms, createAnonUpdate, createApp, createBeforeLoopUpdate, createLocalAnonUpdate, displayName, doPreparations, instantiate, isApplicableOnSubTerms, isModalityTerm, mapAndConjunct, prepareVariant, splitUpdates, toString
clone, equals, finalize, getClass, hashCode, notify, notifyAll, wait, wait, wait
getOrigin
public static final LoopScopeInvariantRule INSTANCE
LoopScopeInvariantRule
.public static final java.lang.String INITIAL_INVARIANT_ONLY_HINT
public static final java.lang.String FULL_INVARIANT_TERM_HINT
public int getNrOfGoals()
getNrOfGoals
in class AbstractLoopInvariantRule
public boolean isApplicable(Goal goal, PosInOccurrence pio)
NOTE: The LoopScopeInvariantRule
currently
doesn't support Java Card transactions and information flow proof
obligations.
isApplicable
in interface BuiltInRule
isApplicable
in class AbstractLoopInvariantRule
public ImmutableList<Goal> apply(Goal goal, Services services, RuleApp ruleApp) throws RuleAbortException
Rule
goal
- the Goal on which to apply ruleAppservices
- the Services with the necessary information
about the java programsruleApp
- the rule application to be executedRuleAbortException
Copyright © 2003-2019 The KeY-Project.