public interface LoopInvariant extends SpecificationElement
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) |
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) |
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) |
Contract.OriginalVariables |
getOrigVars()
Returns the original Self Variable to replace it easier.
|
String |
getPlainText(Services services,
Iterable<LocationVariable> heapContext,
boolean usePrettyPrinting,
boolean useUnicodeSymbols)
Returns the invariant in pretty plain text format.
|
IProgramMethod |
getTarget()
Returns the contracted function symbol.
|
String |
getUniqueName() |
Term |
getVariant(Term selfTerm,
Map<LocationVariable,Term> atPres,
Services services)
Returns the variant term.
|
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) |
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.
|
getDisplayName, getName, getVisibility
LoopStatement getLoop()
IProgramMethod getTarget()
Term getInvariant(LocationVariable heap, Term selfTerm, Map<LocationVariable,Term> atPres, Services services)
Term getModifies(LocationVariable heap, Term selfTerm, Map<LocationVariable,Term> atPres, Services services)
ImmutableList<InfFlowSpec> getInfFlowSpecs(LocationVariable heap)
ImmutableList<InfFlowSpec> getInfFlowSpecs(Services services)
ImmutableList<InfFlowSpec> getInfFlowSpecs(LocationVariable heap, Term selfTerm, Map<LocationVariable,Term> atPres, Services services)
boolean hasInfFlowSpec(Services services)
Term getVariant(Term selfTerm, Map<LocationVariable,Term> atPres, Services services)
Term getInternalSelfTerm()
Term getModifies()
Map<LocationVariable,Term> getInternalAtPres()
Map<LocationVariable,Term> getInternalInvariants()
Term getInternalVariant()
Map<LocationVariable,Term> getInternalModifies()
Map<LocationVariable,ImmutableList<InfFlowSpec>> getInternalInfFlowSpec()
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)
LoopInvariant instantiate(Map<LocationVariable,Term> invariants, Term variant)
LoopInvariant configurate(Map<LocationVariable,Term> invariants, Map<LocationVariable,Term> modifies, Map<LocationVariable,ImmutableList<InfFlowSpec>> infFlowSpecs, Term variant)
LoopInvariant setLoop(LoopStatement loop)
LoopInvariant setTarget(IProgramMethod newPM)
LoopInvariant setInvariant(Map<LocationVariable,Term> invariants, Term selfTerm, Map<LocationVariable,Term> atPres, Services services)
void visit(Visitor v)
String getPlainText(Services services, Iterable<LocationVariable> heapContext, boolean usePrettyPrinting, boolean useUnicodeSymbols)
String getUniqueName()
KeYJavaType getKJT()
SpecificationElement
getKJT
in interface SpecificationElement
LoopInvariant setTarget(KeYJavaType newKJT, IObserverFunction newPM)
Contract.OriginalVariables getOrigVars()