public interface LoopSpecification extends SpecificationElement
Modifier and Type | Method and Description |
---|---|
LoopSpecification |
configurate(java.util.Map<LocationVariable,Term> invariants,
java.util.Map<LocationVariable,Term> freeInvariants,
java.util.Map<LocationVariable,Term> modifies,
java.util.Map<LocationVariable,ImmutableList<InfFlowSpec>> infFlowSpecs,
Term variant)
Configure the existing loop specification element with new elements,
i.e., loop invariant clauses, a loop variant, modifies clauses,
information flow specification elements, and a loop variant,
possibly together with (if any) "free" loop invariant clauses.
|
LoopSpecification |
create(LoopStatement loop,
IProgramMethod pm,
KeYJavaType kjt,
java.util.Map<LocationVariable,Term> invariants,
java.util.Map<LocationVariable,Term> freeInvariants,
java.util.Map<LocationVariable,Term> modifies,
java.util.Map<LocationVariable,ImmutableList<InfFlowSpec>> infFlowSpecs,
Term variant,
Term selfTerm,
ImmutableList<Term> localIns,
ImmutableList<Term> localOuts,
java.util.Map<LocationVariable,Term> atPres)
Create and return a new loop specification element from the existing one
where the arguments given are replaced.
|
LoopSpecification |
create(LoopStatement loop,
java.util.Map<LocationVariable,Term> invariants,
java.util.Map<LocationVariable,Term> freeInvariants,
java.util.Map<LocationVariable,Term> modifies,
java.util.Map<LocationVariable,ImmutableList<InfFlowSpec>> infFlowSpecs,
Term variant,
Term selfTerm,
ImmutableList<Term> localIns,
ImmutableList<Term> localOuts,
java.util.Map<LocationVariable,Term> atPres)
Create and return a new loop specification element from the existing one
where the arguments given are replaced.
|
Term |
getFreeInvariant(LocationVariable heap,
Term selfTerm,
java.util.Map<LocationVariable,Term> atPres,
Services services)
Returns the free invariant formula.
|
Term |
getFreeInvariant(Services services) |
ImmutableList<InfFlowSpec> |
getInfFlowSpecs(LocationVariable heap)
Returns the information flow specification clause.
|
ImmutableList<InfFlowSpec> |
getInfFlowSpecs(LocationVariable heap,
Term selfTerm,
java.util.Map<LocationVariable,Term> atPres,
Services services) |
ImmutableList<InfFlowSpec> |
getInfFlowSpecs(Services services) |
java.util.Map<LocationVariable,Term> |
getInternalAtPres()
Returns operators internally used for the pre-heap.
|
java.util.Map<LocationVariable,Term> |
getInternalFreeInvariants()
Returns the term internally used for the "free" invariant.
|
java.util.Map<LocationVariable,ImmutableList<InfFlowSpec>> |
getInternalInfFlowSpec() |
java.util.Map<LocationVariable,Term> |
getInternalInvariants()
Returns the term internally used for the invariant.
|
java.util.Map<LocationVariable,Term> |
getInternalModifies()
Returns the term internally used for the modifies clause.
|
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,
java.util.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,
java.util.Map<LocationVariable,Term> atPres,
Services services)
Returns the modifies clause.
|
Term |
getModifies(Term selfTerm,
java.util.Map<LocationVariable,Term> atPres,
Services services)
Returns the modifies clause.
|
Contract.OriginalVariables |
getOrigVars()
Returns the original Self Variable to replace it easier.
|
java.lang.String |
getPlainText(Services services,
java.lang.Iterable<LocationVariable> heapContext,
boolean usePrettyPrinting,
boolean useUnicodeSymbols)
Returns the invariant in pretty plain text format.
|
IProgramMethod |
getTarget()
Returns the contracted function symbol.
|
java.lang.String |
getUniqueName() |
Term |
getVariant(Term selfTerm,
java.util.Map<LocationVariable,Term> atPres,
Services services)
Returns the variant term.
|
boolean |
hasInfFlowSpec(Services services) |
LoopSpecification |
instantiate(java.util.Map<LocationVariable,Term> invariants,
java.util.Map<LocationVariable,Term> freeInvariants,
Term variant)
Instantiate a (raw) loop specification with loop invariant clauses and
a loop variant, possibly together with (if any) "free" loop invariant
clauses.
|
LoopSpecification |
setInvariant(java.util.Map<LocationVariable,Term> invariants,
java.util.Map<LocationVariable,Term> freeInvariants,
Term selfTerm,
java.util.Map<LocationVariable,Term> atPres,
Services services)
Returns a new loop invariant where the invariant formula has been
replaced with the passed one.
|
LoopSpecification |
setLoop(LoopStatement loop)
Returns a new loop invariant where the loop reference has been
replaced with the passed one.
|
LoopSpecification |
setTarget(IProgramMethod newPM) |
LoopSpecification |
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, java.util.Map<LocationVariable,Term> atPres, Services services)
heap
- the heap variable.selfTerm
- the self term.atPres
- the operators used for the pre-heap.services
- the Services object.Term getFreeInvariant(LocationVariable heap, Term selfTerm, java.util.Map<LocationVariable,Term> atPres, Services services)
Term getModifies(LocationVariable heap, Term selfTerm, java.util.Map<LocationVariable,Term> atPres, Services services)
heap
- the heap variable.selfTerm
- the self term.atPres
- the operators used for the pre-heap.services
- the Services object.Term getModifies(Term selfTerm, java.util.Map<LocationVariable,Term> atPres, Services services)
selfTerm
- the self term.atPres
- the operators used for the pre-heap.services
- the Services object.ImmutableList<InfFlowSpec> getInfFlowSpecs(LocationVariable heap)
ImmutableList<InfFlowSpec> getInfFlowSpecs(Services services)
ImmutableList<InfFlowSpec> getInfFlowSpecs(LocationVariable heap, Term selfTerm, java.util.Map<LocationVariable,Term> atPres, Services services)
boolean hasInfFlowSpec(Services services)
Term getVariant(Term selfTerm, java.util.Map<LocationVariable,Term> atPres, Services services)
selfTerm
- the self term.atPres
- the operators used for the pre-heap.services
- the Services object.Term getInternalSelfTerm()
Term getModifies()
java.util.Map<LocationVariable,Term> getInternalAtPres()
java.util.Map<LocationVariable,Term> getInternalInvariants()
java.util.Map<LocationVariable,Term> getInternalFreeInvariants()
Term getInternalVariant()
java.util.Map<LocationVariable,Term> getInternalModifies()
java.util.Map<LocationVariable,ImmutableList<InfFlowSpec>> getInternalInfFlowSpec()
LoopSpecification create(LoopStatement loop, IProgramMethod pm, KeYJavaType kjt, java.util.Map<LocationVariable,Term> invariants, java.util.Map<LocationVariable,Term> freeInvariants, java.util.Map<LocationVariable,Term> modifies, java.util.Map<LocationVariable,ImmutableList<InfFlowSpec>> infFlowSpecs, Term variant, Term selfTerm, ImmutableList<Term> localIns, ImmutableList<Term> localOuts, java.util.Map<LocationVariable,Term> atPres)
loop
- the new loop statement.pm
- the new program method.kjt
- the new KeYJavaType.invariants
- the new loop invariant clauses.freeInvariants
- the new "free" loop invariant clauses.modifies
- the new modifies clauses.infFlowSpecs
- the new information flow specification elements.variant
- the new loop variant term.selfTerm
- the new self term.localIns
- the new local in-variables.localOuts
- the new local out-variables.atPres
- the new operators used for the pre-heap.LoopSpecification create(LoopStatement loop, java.util.Map<LocationVariable,Term> invariants, java.util.Map<LocationVariable,Term> freeInvariants, java.util.Map<LocationVariable,Term> modifies, java.util.Map<LocationVariable,ImmutableList<InfFlowSpec>> infFlowSpecs, Term variant, Term selfTerm, ImmutableList<Term> localIns, ImmutableList<Term> localOuts, java.util.Map<LocationVariable,Term> atPres)
loop
- the new loop statement.invariants
- the new loop invariant clauses.freeInvariants
- the new "free" loop invariant clauses.modifies
- the new modifies clauses.infFlowSpecs
- the new information flow specification elements.variant
- the new loop variant term.selfTerm
- the new self term.localIns
- the new local in-variables.localOuts
- the new local out-variables.atPres
- the new operators used for the pre-heap.LoopSpecification instantiate(java.util.Map<LocationVariable,Term> invariants, java.util.Map<LocationVariable,Term> freeInvariants, Term variant)
invariants
- the loop invariant clauses for instantiation.freeInvariants
- the "free" loop invariant clauses for instantiation.variant
- the loop variant for instantiation.LoopSpecification configurate(java.util.Map<LocationVariable,Term> invariants, java.util.Map<LocationVariable,Term> freeInvariants, java.util.Map<LocationVariable,Term> modifies, java.util.Map<LocationVariable,ImmutableList<InfFlowSpec>> infFlowSpecs, Term variant)
invariants
- the new loop invariant clauses.freeInvariants
- the new "free" loop invariant clauses.modifies
- the new modifies clauses.infFlowSpecs
- the new information flow specification elements.variant
- the new loop variant.LoopSpecification setLoop(LoopStatement loop)
LoopSpecification setTarget(IProgramMethod newPM)
LoopSpecification setInvariant(java.util.Map<LocationVariable,Term> invariants, java.util.Map<LocationVariable,Term> freeInvariants, Term selfTerm, java.util.Map<LocationVariable,Term> atPres, Services services)
invariants
- the loop invariant clauses.freeInvariants
- the "free" loop invariant clauses.selfTerm
- the self term.atPres
- the operators used for the pre-heap.services
- the Services object.void visit(Visitor v)
java.lang.String getPlainText(Services services, java.lang.Iterable<LocationVariable> heapContext, boolean usePrettyPrinting, boolean useUnicodeSymbols)
services
- the Services object.heapContext
- all corresponding heaps.usePrettyPrinting
- whether the text should be pretty-printed.useUnicodeSymbols
- whether Unicode symbols should be used.java.lang.String getUniqueName()
KeYJavaType getKJT()
SpecificationElement
getKJT
in interface SpecificationElement
LoopSpecification setTarget(KeYJavaType newKJT, IObserverFunction newPM)
Contract.OriginalVariables getOrigVars()