public abstract class AbstractLoopInvariantRule extends java.lang.Object implements BuiltInRule
doPreparations(Goal, Services, RuleApp)
directly at the
beginning of the Rule.apply(Goal, Services, RuleApp)
method.LoopScopeInvariantRule
,
WhileInvariantRule
Modifier and Type | Class and Description |
---|---|
protected static class |
AbstractLoopInvariantRule.AdditionalHeapTerms
A container with data for the additional terms with assertions about the
heap; that is, the anonymizing update, the wellformed term, the frame
condition and the reachable state formula.
|
protected static class |
AbstractLoopInvariantRule.AnonUpdateData
A container containing data for the anonymizing update, that is the
actual update and the anonymized heap.
|
protected static class |
AbstractLoopInvariantRule.Instantiation
A container for an instantiation of this
LoopScopeInvariantRule
application; contains the update, the program with post condition, the
While loop the LoopScopeInvariantRule should be applied
to, the LoopSpecification , the the self Term . |
protected static class |
AbstractLoopInvariantRule.LoopInvariantInformation
A container object containing the information required for the concrete
loop invariant rules to create the sequents for the new goals.
|
Modifier and Type | Field and Description |
---|---|
private static Term |
lastFocusTerm
The last formula the loop invariant rule was applied to.
|
private static AbstractLoopInvariantRule.Instantiation |
lastInstantiation
A simple cache which ensures that we don't instantiate the rule multiple
times for the same loop.
|
Constructor and Description |
---|
AbstractLoopInvariantRule() |
Modifier and Type | Method and Description |
---|---|
protected static Term |
and(TermBuilder tb,
Term t1,
Term t2)
Creates a conjunction of t1 and t2 if both are not null, and returns t2
only if t1 is null.
|
protected static Term |
conjunctFreeInv(Services services,
AbstractLoopInvariantRule.Instantiation inst,
java.util.Map<LocationVariable,Term> atPres,
java.util.List<LocationVariable> heapContext)
Creates a conjunction of all free invariant formulas for the
LocationVariable s in heapContext. |
protected static Term |
conjunctInv(Services services,
AbstractLoopInvariantRule.Instantiation inst,
java.util.Map<LocationVariable,Term> atPres,
java.util.List<LocationVariable> heapContext)
Creates a conjunction of all invariant formulas for the
LocationVariable s in heapContext. |
protected static AbstractLoopInvariantRule.AdditionalHeapTerms |
createAdditionalHeapTerms(Services services,
AbstractLoopInvariantRule.Instantiation inst,
java.util.List<LocationVariable> heapContext,
ImmutableSet<ProgramVariable> localOuts,
java.util.Map<LocationVariable,java.util.Map<Term,Term>> heapToBeforeLoop,
java.util.Map<LocationVariable,Term> atPres)
Prepare anon update, wellformed formula, frame condition and reachable
state formula.
|
protected static AbstractLoopInvariantRule.AnonUpdateData |
createAnonUpdate(LocationVariable heap,
Term mod,
LoopSpecification inv,
Services services)
Computes the anonymizing update, the loop heap, the base heap, and the
anonymized heap.
|
IBuiltInRuleApp |
createApp(PosInOccurrence pos,
TermServices services) |
protected static Term |
createBeforeLoopUpdate(Services services,
java.util.List<LocationVariable> heapContext,
ImmutableSet<ProgramVariable> localOuts,
java.util.Map<LocationVariable,java.util.Map<Term,Term>> heapToBeforeLoop)
Creates the "...Before_LOOP" update needed for the variant.
|
protected static Term |
createLocalAnonUpdate(ImmutableSet<ProgramVariable> localOuts,
Services services)
Creates an update for the anonymization of all
ProgramVariable s
in localOuts. |
java.lang.String |
displayName()
returns the display name of the rule
|
AbstractLoopInvariantRule.LoopInvariantInformation |
doPreparations(Goal goal,
Services services,
RuleApp ruleApp)
Constructs the data needed for the currently implemented loop invariants;
also prepares the new set of goals, that is splitting the current goal is
no longer required after calling this method.
|
abstract int |
getNrOfGoals() |
protected static AbstractLoopInvariantRule.Instantiation |
instantiate(LoopInvariantBuiltInRuleApp app,
Services services)
Constructs the
AbstractLoopInvariantRule.Instantiation object containing the relevant
parameters for this LoopScopeInvariantRule application. |
boolean |
isApplicable(Goal goal,
PosInOccurrence pio)
returns true iff a rule is applicable at the given
position.
|
boolean |
isApplicableOnSubTerms() |
protected static boolean |
isModalityTerm(Term progPost)
Checks whether progPost contains a Java program.
|
protected static <T> Term |
mapAndConjunct(Services services,
java.util.function.Function<T,Term> fct,
java.util.List<T> listOfT)
Creates a conjunction of
Term s that are produced by fct from the
elements in listOfT. fct may return null when applied to a T object; in
this case, the result is ignored when constructing the conjunction. |
protected static Pair<Term,Term> |
prepareVariant(AbstractLoopInvariantRule.Instantiation inst,
Term variant,
TermServices services)
Creates the variant proof obligation and update.
|
protected static Pair<Term,Term> |
splitUpdates(Term focusTerm,
TermServices services)
Splits a term into the update and formula part.
|
java.lang.String |
toString() |
private static Term lastFocusTerm
lastInstantiation
can be used instead of doing
a new instantiation.private static AbstractLoopInvariantRule.Instantiation lastInstantiation
public abstract int getNrOfGoals()
public AbstractLoopInvariantRule.LoopInvariantInformation doPreparations(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 executedAbstractLoopInvariantRule.LoopInvariantInformation
object containing the data
for the application of loop invariant rules.RuleAbortException
public boolean isApplicable(Goal goal, PosInOccurrence pio)
BuiltInRule
isApplicable
in interface BuiltInRule
public boolean isApplicableOnSubTerms()
isApplicableOnSubTerms
in interface BuiltInRule
public IBuiltInRuleApp createApp(PosInOccurrence pos, TermServices services)
createApp
in interface BuiltInRule
public java.lang.String displayName()
Rule
displayName
in interface Rule
public java.lang.String toString()
toString
in class java.lang.Object
protected static Term createBeforeLoopUpdate(Services services, java.util.List<LocationVariable> heapContext, ImmutableSet<ProgramVariable> localOuts, java.util.Map<LocationVariable,java.util.Map<Term,Term>> heapToBeforeLoop)
services
- The Services
object.heapContext
- TODOlocalOuts
- TODOheapToBeforeLoop
- TODOprotected static Term createLocalAnonUpdate(ImmutableSet<ProgramVariable> localOuts, Services services)
ProgramVariable
s
in localOuts.localOuts
- The ProgramVariable
s to anonymize.services
- The Services
object.protected static Term conjunctInv(Services services, AbstractLoopInvariantRule.Instantiation inst, java.util.Map<LocationVariable,Term> atPres, java.util.List<LocationVariable> heapContext)
LocationVariable
s in heapContext.services
- The Services
object.inst
- The AbstractLoopInvariantRule.Instantiation
for this rule application.atPres
- TODOheapContext
- The heap formulas to create a conjunction of invariants for.LocationVariable
s in heapContext.protected static Term conjunctFreeInv(Services services, AbstractLoopInvariantRule.Instantiation inst, java.util.Map<LocationVariable,Term> atPres, java.util.List<LocationVariable> heapContext)
LocationVariable
s in heapContext.services
- The Services
object.inst
- The AbstractLoopInvariantRule.Instantiation
for this rule application.atPres
- TODOheapContext
- The heap formulas to create a conjunction of free
invariants for.LocationVariable
s in heapContext.protected static <T> Term mapAndConjunct(Services services, java.util.function.Function<T,Term> fct, java.util.List<T> listOfT)
Term
s that are produced by fct from the
elements in listOfT. fct may return null when applied to a T object; in
this case, the result is ignored when constructing the conjunction.protected static Pair<Term,Term> prepareVariant(AbstractLoopInvariantRule.Instantiation inst, Term variant, TermServices services)
inst
- The AbstractLoopInvariantRule.Instantiation
for this rule application.variant
- The variant term as given by the loop specification.services
- The Services
object.protected static Pair<Term,Term> splitUpdates(Term focusTerm, TermServices services)
focusTerm
- The term to split into update and formula the update is
applied to.services
- The Services
object.protected static boolean isModalityTerm(Term progPost)
progPost
- The Term to check.protected static Term and(TermBuilder tb, Term t1, Term t2)
tb
- The TermBuilder
object.t1
- The first formula of the conjunction; may be null.t2
- The second formula of the conjunction; may not be
null.protected static AbstractLoopInvariantRule.Instantiation instantiate(LoopInvariantBuiltInRuleApp app, Services services) throws RuleAbortException
AbstractLoopInvariantRule.Instantiation
object containing the relevant
parameters for this LoopScopeInvariantRule
application.app
- The LoopInvariantBuiltInRuleApp
object for the
application of the LoopScopeInvariantRule
.services
- The Services
object.AbstractLoopInvariantRule.Instantiation
object containing the relevant
parameters for this LoopScopeInvariantRule
application.RuleAbortException
- If the LoopInvariantBuiltInRuleApp
does not contain a
LoopSpecification
.protected static AbstractLoopInvariantRule.AnonUpdateData createAnonUpdate(LocationVariable heap, Term mod, LoopSpecification inv, Services services)
heap
- The original heap LocationVariable
.mod
- The modifiers term.inv
- The loop invariant.services
- The Services
object.AbstractLoopInvariantRule.AnonUpdateData
object encapsulating the anonymizing
update, the loop heap, the base heap, and the anonymized heap.protected static AbstractLoopInvariantRule.AdditionalHeapTerms createAdditionalHeapTerms(Services services, AbstractLoopInvariantRule.Instantiation inst, java.util.List<LocationVariable> heapContext, ImmutableSet<ProgramVariable> localOuts, java.util.Map<LocationVariable,java.util.Map<Term,Term>> heapToBeforeLoop, java.util.Map<LocationVariable,Term> atPres)
services
- The Services
object.inst
- The AbstractLoopInvariantRule.Instantiation
of parameters for the
LoopScopeInvariantRule
app.heapContext
- TODOlocalOuts
- TODOheapToBeforeLoop
- TODOatPres
- TODOAbstractLoopInvariantRule.AdditionalHeapTerms
object containing the anonymized
update, the wellformed formula, the frame condition formula, and
the reachable state formula.