public final class LoopInvariantImpl extends Object implements LoopInvariant
Modifier and Type | Field and Description |
---|---|
private KeYJavaType |
kjt |
private ImmutableList<Term> |
localIns |
private ImmutableList<Term> |
localOuts |
private LoopStatement |
loop |
private Map<LocationVariable,Term> |
originalAtPres |
private Map<LocationVariable,ImmutableList<InfFlowSpec>> |
originalInfFlowSpecs |
private Map<LocationVariable,Term> |
originalInvariants |
private Map<LocationVariable,Term> |
originalModifies |
private Term |
originalSelfTerm |
private Term |
originalVariant |
private IProgramMethod |
pm |
Constructor and Description |
---|
LoopInvariantImpl(LoopStatement loop,
IProgramMethod pm,
KeYJavaType kjt,
Map<LocationVariable,Term> invariants,
Map<LocationVariable,Term> modifies,
Map<LocationVariable,ImmutableList<InfFlowSpec>> infFlowSpecs,
Term variant,
Term selfTerm,
ImmutableList<Term> localIns,
ImmutableList<Term> localOuts,
Map<LocationVariable,Term> atPres)
Creates a loop invariant.
|
LoopInvariantImpl(LoopStatement loop,
IProgramMethod pm,
KeYJavaType kjt,
Term selfTerm,
Map<LocationVariable,Term> atPres)
Creates an empty, default loop invariant for the passed loop.
|
Modifier and Type | Method and Description |
---|---|
LoopInvariant |
configurate(Map<LocationVariable,Term> invariants,
Map<LocationVariable,Term> modifies,
Map<LocationVariable,ImmutableList<InfFlowSpec>> infFlowSpecs,
Term variant) |
LoopInvariant |
create(LoopStatement loop,
IProgramMethod pm,
KeYJavaType kjt,
Map<LocationVariable,Term> invariants,
Map<LocationVariable,Term> modifies,
Map<LocationVariable,ImmutableList<InfFlowSpec>> infFlowSpecs,
Term variant,
Term selfTerm,
ImmutableList<Term> localIns,
ImmutableList<Term> localOuts,
Map<LocationVariable,Term> atPres) |
LoopInvariant |
create(LoopStatement loop,
Map<LocationVariable,Term> invariants,
Map<LocationVariable,Term> modifies,
Map<LocationVariable,ImmutableList<InfFlowSpec>> infFlowSpecs,
Term variant,
Term selfTerm,
ImmutableList<Term> localIns,
ImmutableList<Term> localOuts,
Map<LocationVariable,Term> atPres) |
String |
getDisplayName()
Returns the displayed name.
|
ImmutableList<InfFlowSpec> |
getInfFlowSpecs(LocationVariable heap)
Returns the information flow specification clause.
|
ImmutableList<InfFlowSpec> |
getInfFlowSpecs(LocationVariable heap,
Term selfTerm,
Map<LocationVariable,Term> atPres,
Services services) |
ImmutableList<InfFlowSpec> |
getInfFlowSpecs(Services services) |
Map<LocationVariable,Term> |
getInternalAtPres()
Returns operators internally used for the pre-heap.
|
Map<LocationVariable,ImmutableList<InfFlowSpec>> |
getInternalInfFlowSpec() |
Map<LocationVariable,Term> |
getInternalInvariants()
Returns the term internally used for the invariant.
|
Map<LocationVariable,Term> |
getInternalModifies() |
Term |
getInternalSelfTerm()
Returns the term internally used for self.
|
Term |
getInternalVariant()
Returns the term internally used for the variant.
|
Term |
getInvariant(LocationVariable heap,
Term selfTerm,
Map<LocationVariable,Term> atPres,
Services services)
Returns the invariant formula.
|
Term |
getInvariant(Services services) |
private Map<Term,Term> |
getInverseReplaceMap(Term selfTerm,
Map<LocationVariable,Term> atPres,
Services services) |
KeYJavaType |
getKJT()
Returns the KeYJavaType representing the class/interface to which the
specification element belongs.
|
LoopStatement |
getLoop()
Returns the loop to which the invariant belongs.
|
Term |
getModifies() |
Term |
getModifies(LocationVariable heap,
Term selfTerm,
Map<LocationVariable,Term> atPres,
Services services)
Returns the modifies clause.
|
Term |
getModifies(Term selfTerm,
Map<LocationVariable,Term> atPres,
Services services) |
String |
getName()
Returns the unique internal name of the specification element.
|
Contract.OriginalVariables |
getOrigVars()
Returns the original Self Variable to replace it easier.
|
String |
getPlainText(Services services,
boolean usePrettyPrinting,
boolean useUnicodeSymbols) |
String |
getPlainText(Services services,
Iterable<LocationVariable> heapContext,
boolean usePrettyPrinting,
boolean useUnicodeSymbols)
Returns the invariant in pretty plain text format.
|
private Map<Term,Term> |
getReplaceMap(Term selfTerm,
Map<LocationVariable,Term> atPres,
Services services) |
IProgramMethod |
getTarget()
Returns the contracted function symbol.
|
String |
getUniqueName() |
Term |
getVariant(Term selfTerm,
Map<LocationVariable,Term> atPres,
Services services)
Returns the variant term.
|
VisibilityModifier |
getVisibility()
Returns the visibility of the invariant (null for default visibility)
|
boolean |
hasInfFlowSpec(Services services) |
LoopInvariant |
instantiate(Map<LocationVariable,Term> invariants,
Term variant) |
LoopInvariant |
setInvariant(Map<LocationVariable,Term> invariants,
Term selfTerm,
Map<LocationVariable,Term> atPres,
Services services)
Returns a new loop invariant where the invariant formula has been
replaced with the passed one.
|
LoopInvariant |
setLoop(LoopStatement loop)
Returns a new loop invariant where the loop reference has been
replaced with the passed one.
|
LoopInvariant |
setTarget(IProgramMethod newPM) |
LoopInvariant |
setTarget(KeYJavaType newKJT,
IObserverFunction newPM) |
String |
toString() |
void |
visit(Visitor v)
Loop invariants can be visited like source elements:
This method calls the corresponding method of a visitor in order to
perform some action/transformation on this element.
|
private final LoopStatement loop
private final IProgramMethod pm
private final KeYJavaType kjt
private final Map<LocationVariable,Term> originalInvariants
private final Map<LocationVariable,Term> originalModifies
private final Map<LocationVariable,ImmutableList<InfFlowSpec>> originalInfFlowSpecs
private final Term originalVariant
private final Term originalSelfTerm
private final ImmutableList<Term> localIns
private final ImmutableList<Term> localOuts
private final Map<LocationVariable,Term> originalAtPres
public LoopInvariantImpl(LoopStatement loop, IProgramMethod pm, KeYJavaType kjt, Map<LocationVariable,Term> invariants, Map<LocationVariable,Term> modifies, Map<LocationVariable,ImmutableList<InfFlowSpec>> infFlowSpecs, Term variant, Term selfTerm, ImmutableList<Term> localIns, ImmutableList<Term> localOuts, Map<LocationVariable,Term> atPres)
loop
- the loop to which the invariant belongsinvariant
- the invariant formulamodifies
- the modifier setinfFlowSpecs
- low variables for information flowvariant
- the variant termselfTerm
- the term used for the receiver objectheapAtPre
- the term used for the at pre heappublic LoopInvariantImpl(LoopStatement loop, IProgramMethod pm, KeYJavaType kjt, Term selfTerm, Map<LocationVariable,Term> atPres)
private Map<Term,Term> getReplaceMap(Term selfTerm, Map<LocationVariable,Term> atPres, Services services)
private Map<Term,Term> getInverseReplaceMap(Term selfTerm, Map<LocationVariable,Term> atPres, Services services)
public LoopStatement getLoop()
LoopInvariant
getLoop
in interface LoopInvariant
public Term getInvariant(LocationVariable heap, Term selfTerm, Map<LocationVariable,Term> atPres, Services services)
LoopInvariant
getInvariant
in interface LoopInvariant
public Term getInvariant(Services services)
getInvariant
in interface LoopInvariant
public Term getModifies(LocationVariable heap, Term selfTerm, Map<LocationVariable,Term> atPres, Services services)
LoopInvariant
getModifies
in interface LoopInvariant
public Term getModifies(Term selfTerm, Map<LocationVariable,Term> atPres, Services services)
getModifies
in interface LoopInvariant
public ImmutableList<InfFlowSpec> getInfFlowSpecs(LocationVariable heap, Term selfTerm, Map<LocationVariable,Term> atPres, Services services)
getInfFlowSpecs
in interface LoopInvariant
public ImmutableList<InfFlowSpec> getInfFlowSpecs(LocationVariable heap)
LoopInvariant
getInfFlowSpecs
in interface LoopInvariant
public ImmutableList<InfFlowSpec> getInfFlowSpecs(Services services)
getInfFlowSpecs
in interface LoopInvariant
public Term getVariant(Term selfTerm, Map<LocationVariable,Term> atPres, Services services)
LoopInvariant
getVariant
in interface LoopInvariant
public Map<LocationVariable,Term> getInternalInvariants()
LoopInvariant
getInternalInvariants
in interface LoopInvariant
public Term getInternalVariant()
LoopInvariant
getInternalVariant
in interface LoopInvariant
public Map<LocationVariable,Term> getInternalModifies()
getInternalModifies
in interface LoopInvariant
public Map<LocationVariable,ImmutableList<InfFlowSpec>> getInternalInfFlowSpec()
getInternalInfFlowSpec
in interface LoopInvariant
public Term getInternalSelfTerm()
LoopInvariant
getInternalSelfTerm
in interface LoopInvariant
public Term getModifies()
getModifies
in interface LoopInvariant
public Map<LocationVariable,Term> getInternalAtPres()
LoopInvariant
getInternalAtPres
in interface LoopInvariant
public LoopInvariant create(LoopStatement loop, IProgramMethod pm, KeYJavaType kjt, Map<LocationVariable,Term> invariants, Map<LocationVariable,Term> modifies, Map<LocationVariable,ImmutableList<InfFlowSpec>> infFlowSpecs, Term variant, Term selfTerm, ImmutableList<Term> localIns, ImmutableList<Term> localOuts, Map<LocationVariable,Term> atPres)
create
in interface LoopInvariant
public LoopInvariant create(LoopStatement loop, Map<LocationVariable,Term> invariants, Map<LocationVariable,Term> modifies, Map<LocationVariable,ImmutableList<InfFlowSpec>> infFlowSpecs, Term variant, Term selfTerm, ImmutableList<Term> localIns, ImmutableList<Term> localOuts, Map<LocationVariable,Term> atPres)
create
in interface LoopInvariant
public LoopInvariant instantiate(Map<LocationVariable,Term> invariants, Term variant)
instantiate
in interface LoopInvariant
public LoopInvariant configurate(Map<LocationVariable,Term> invariants, Map<LocationVariable,Term> modifies, Map<LocationVariable,ImmutableList<InfFlowSpec>> infFlowSpecs, Term variant)
configurate
in interface LoopInvariant
public LoopInvariant setLoop(LoopStatement loop)
LoopInvariant
setLoop
in interface LoopInvariant
public LoopInvariant setTarget(IProgramMethod newPM)
setTarget
in interface LoopInvariant
public LoopInvariant setInvariant(Map<LocationVariable,Term> invariants, Term selfTerm, Map<LocationVariable,Term> atPres, Services services)
LoopInvariant
setInvariant
in interface LoopInvariant
public void visit(Visitor v)
LoopInvariant
visit
in interface LoopInvariant
public String getPlainText(Services services, boolean usePrettyPrinting, boolean useUnicodeSymbols)
public String getPlainText(Services services, Iterable<LocationVariable> heapContext, boolean usePrettyPrinting, boolean useUnicodeSymbols)
LoopInvariant
getPlainText
in interface LoopInvariant
public String getDisplayName()
SpecificationElement
getDisplayName
in interface SpecificationElement
public IProgramMethod getTarget()
LoopInvariant
getTarget
in interface LoopInvariant
public KeYJavaType getKJT()
SpecificationElement
getKJT
in interface LoopInvariant
getKJT
in interface SpecificationElement
public String getName()
SpecificationElement
getName
in interface SpecificationElement
public String getUniqueName()
getUniqueName
in interface LoopInvariant
public VisibilityModifier getVisibility()
SpecificationElement
getVisibility
in interface SpecificationElement
public boolean hasInfFlowSpec(Services services)
hasInfFlowSpec
in interface LoopInvariant
public LoopInvariant setTarget(KeYJavaType newKJT, IObserverFunction newPM)
setTarget
in interface LoopInvariant
public Contract.OriginalVariables getOrigVars()
LoopInvariant
getOrigVars
in interface LoopInvariant