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 . |
private static Name |
NAME |
private static int |
NR_GOALS
The number of goals generated by the
LoopScopeInvariantRule . |
Modifier | Constructor and Description |
---|---|
private |
LoopScopeInvariantRule()
Singleton constructor.
|
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.
|
private void |
constructInitiallyGoal(Services services,
RuleApp ruleApp,
TermLabelState termLabelState,
Goal initiallyGoal,
AbstractLoopInvariantRule.Instantiation inst,
Term invTerm,
Term reachableState)
Sets the content of the "initially valid" goal.
|
private void |
constructPresrvAndUCGoal(Services services,
RuleApp ruleApp,
Goal presrvAndUCGoal,
AbstractLoopInvariantRule.Instantiation inst,
java.util.Optional<Label> loopLabel,
Statement stmtToReplace,
Term anonUpdate,
Term wellFormedAnon,
Term uAnonInv,
Term frameCondition,
Term variantPO,
TermLabelState termLabelState,
Term invTerm,
Term[] uBeforeLoopDefAnonVariant)
Creates the "Invariant Preserved and Used" goal subsuming the former
preserved and use case goals.
|
private Pair<java.util.Optional<Label>,Statement> |
findLoopLabel(RuleApp ruleApp,
While whileLoop)
If the
While loop has a loop label, returns this and the labeled
statement. |
private Term |
formulaWithLoopScope(Services services,
AbstractLoopInvariantRule.Instantiation inst,
Term anonUpdate,
While loop,
java.util.Optional<Label> loopLabel,
Statement stmtToReplace,
Term frameCondition,
Term variantPO,
TermLabelState termLabelState,
Goal presrvAndUCGoal,
Term[] uBeforeLoopDefAnonVariant,
Term invTerm)
Creates the actual formula by which the original formula containing the
loop is replaced in the "preserves and use case" branch.
|
int |
getNrOfGoals() |
private SequentFormula |
initFormula(TermLabelState termLabelState,
AbstractLoopInvariantRule.Instantiation inst,
Term invTerm,
Term reachableState,
Services services,
Goal initGoal)
Creates the
SequentFormula for the "initially valid" goal. |
boolean |
isApplicable(Goal goal,
PosInOccurrence pio)
NOTE: The
LoopScopeInvariantRule currently
doesn't support Java Card transactions and information flow proof
obligations. |
private ProgramVariable |
loopScopeIdxVar(Services services)
Creates the variable used as a loop scope index.
|
Name |
name()
the name of the rule
|
private ProgramElement |
newProgram(Services services,
While loop,
java.util.Optional<Label> loopLabel,
Statement stmtToReplace,
JavaBlock origProg,
ProgramVariable loopScopeIdxVar)
Creates the new program with the loop scope.
|
and, conjunctFreeInv, conjunctInv, createAdditionalHeapTerms, createAnonUpdate, createApp, createBeforeLoopUpdate, createLocalAnonUpdate, displayName, doPreparations, instantiate, isApplicableOnSubTerms, isModalityTerm, mapAndConjunct, prepareVariant, splitUpdates, toString
private static final int NR_GOALS
LoopScopeInvariantRule
.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
private static final Name NAME
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
private void constructInitiallyGoal(Services services, RuleApp ruleApp, TermLabelState termLabelState, Goal initiallyGoal, AbstractLoopInvariantRule.Instantiation inst, Term invTerm, Term reachableState)
services
- The Services
object.ruleApp
- The RuleApp
for this LoopScopeInvariantRule
application.termLabelState
- The TermLabelState
.initiallyGoal
- The Goal
containing the "initially valid" PO.inst
- The Instantiation
of parameters for the
LoopScopeInvariantRule
app.invTerm
- The loop invariant formula.reachableState
- The reachable state formula.private void constructPresrvAndUCGoal(Services services, RuleApp ruleApp, Goal presrvAndUCGoal, AbstractLoopInvariantRule.Instantiation inst, java.util.Optional<Label> loopLabel, Statement stmtToReplace, Term anonUpdate, Term wellFormedAnon, Term uAnonInv, Term frameCondition, Term variantPO, TermLabelState termLabelState, Term invTerm, Term[] uBeforeLoopDefAnonVariant)
services
- The Services
object.ruleApp
- The LoopInvariantBuiltInRuleApp
object for the current
rule application.presrvAndUCGoal
- The Goal
to serve as container for the new sequent.inst
- The Instantiation
of parameters for the
LoopScopeInvariantRule
app.loopLabel
- The Label
before the While
loop.stmtToReplace
- The Statement
to replace (either a While
loop
or a LabeledStatement
including the While
loop).anonUpdate
- The anonymized update Term
.wellFormedAnon
- The wellformed formula.uAnonInv
- A formula containing the anonymized update and the loop
invariant.frameCondition
- The frame condition.variantPO
- The proof obligation for the variant.termLabelState
- The TermLabelState
.invTerm
- The loop invariant formula.uBeforeLoopDefAnonVariant
- An array containing the original update, the "before the loop"
update for reasoning about the variant, the anonymized update,
and the variant update.private ProgramVariable loopScopeIdxVar(Services services)
services
- The Services
object.private ProgramElement newProgram(Services services, While loop, java.util.Optional<Label> loopLabel, Statement stmtToReplace, JavaBlock origProg, ProgramVariable loopScopeIdxVar)
services
- The Services
object.loop
- The original While
loop that is going to be replaced.loopLabel
- The Label
before the While
loop.stmtToReplace
- The Statement
to replace (either a While
loop
or a LabeledStatement
including the While
loop).origProg
- The whole original program, starting with the While
loop.loopScopeIdxVar
- The variable used as a loop scope index.private SequentFormula initFormula(TermLabelState termLabelState, AbstractLoopInvariantRule.Instantiation inst, Term invTerm, Term reachableState, Services services, Goal initGoal)
SequentFormula
for the "initially valid" goal.termLabelState
- The TermLabelState
.inst
- The Instantiation
for this rule application.invTerm
- The invariant formula.reachableState
- The reachable state formula.services
- The Services
object.initGoal
- The goal containing the "initially valid" PO.SequentFormula
for the "initially valid" goal.private Term formulaWithLoopScope(Services services, AbstractLoopInvariantRule.Instantiation inst, Term anonUpdate, While loop, java.util.Optional<Label> loopLabel, Statement stmtToReplace, Term frameCondition, Term variantPO, TermLabelState termLabelState, Goal presrvAndUCGoal, Term[] uBeforeLoopDefAnonVariant, Term invTerm)
services
- The Services
object.inst
- The Instantiation
of parameters for the
LoopScopeInvariantRule
app.anonUpdate
- The anonymized update Term
.loop
- The original While
loop that is going to be replaced.loopLabel
- The Label
before the While
loop.stmtToReplace
- The Statement
to replace (either a While
loop
or a LabeledStatement
including the While
loop).frameCondition
- The frame condition formula.variantPO
- The proof obligation for the variant.termLabelState
- The TermLabelState
.presrvAndUCGoal
- The Goal
starting the new "preserves and use case"
branch.uBeforeLoopDefAnonVariant
- An array containing the original update, the "before the loop"
update for reasoning about the variant, the anonymized update,
and the variant update.invTerm
- The loop invariant formula Term
.