public final class LoopSpecImpl extends java.lang.Object implements LoopSpecification
Modifier and Type | Field and Description |
---|---|
private KeYJavaType |
kjt |
private ImmutableList<Term> |
localIns |
private ImmutableList<Term> |
localOuts |
private LoopStatement |
loop |
private java.util.Map<LocationVariable,Term> |
originalAtPres |
private java.util.Map<LocationVariable,Term> |
originalFreeInvariants |
private java.util.Map<LocationVariable,ImmutableList<InfFlowSpec>> |
originalInfFlowSpecs |
private java.util.Map<LocationVariable,Term> |
originalInvariants |
private java.util.Map<LocationVariable,Term> |
originalModifies |
private Term |
originalSelfTerm |
private Term |
originalVariant |
private IProgramMethod |
pm |
Constructor and Description |
---|
LoopSpecImpl(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)
Creates a loop invariant.
|
LoopSpecImpl(LoopStatement loop,
IProgramMethod pm,
KeYJavaType kjt,
Term selfTerm,
java.util.Map<LocationVariable,Term> atPres)
Creates an empty, default loop invariant for the passed loop.
|
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.
|
java.lang.String |
getDisplayName()
Returns the displayed name.
|
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) |
private java.util.Map<Term,Term> |
getInverseReplaceMap(Term selfTerm,
java.util.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,
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.
|
java.lang.String |
getName()
Returns the unique internal name of the specification element.
|
Contract.OriginalVariables |
getOrigVars()
Returns the original Self Variable to replace it easier.
|
java.lang.String |
getPlainText(Services services,
boolean usePrettyPrinting,
boolean useUnicodeSymbols) |
java.lang.String |
getPlainText(Services services,
java.lang.Iterable<LocationVariable> heapContext,
boolean usePrettyPrinting,
boolean useUnicodeSymbols)
Returns the invariant in pretty plain text format.
|
private java.util.Map<Term,Term> |
getReplaceMap(Term selfTerm,
java.util.Map<LocationVariable,Term> atPres,
Services services) |
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.
|
VisibilityModifier |
getVisibility()
Returns the visibility of the invariant (null for default visibility)
|
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) |
java.lang.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 java.util.Map<LocationVariable,Term> originalInvariants
private final java.util.Map<LocationVariable,Term> originalFreeInvariants
private final java.util.Map<LocationVariable,Term> originalModifies
private final java.util.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 java.util.Map<LocationVariable,Term> originalAtPres
public LoopSpecImpl(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 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 LoopSpecImpl(LoopStatement loop, IProgramMethod pm, KeYJavaType kjt, Term selfTerm, java.util.Map<LocationVariable,Term> atPres)
private java.util.Map<Term,Term> getReplaceMap(Term selfTerm, java.util.Map<LocationVariable,Term> atPres, Services services)
private java.util.Map<Term,Term> getInverseReplaceMap(Term selfTerm, java.util.Map<LocationVariable,Term> atPres, Services services)
public LoopStatement getLoop()
LoopSpecification
getLoop
in interface LoopSpecification
public Term getInvariant(LocationVariable heap, Term selfTerm, java.util.Map<LocationVariable,Term> atPres, Services services)
LoopSpecification
getInvariant
in interface LoopSpecification
heap
- the heap variable.selfTerm
- the self term.atPres
- the operators used for the pre-heap.services
- the Services object.public Term getInvariant(Services services)
getInvariant
in interface LoopSpecification
public Term getFreeInvariant(LocationVariable heap, Term selfTerm, java.util.Map<LocationVariable,Term> atPres, Services services)
LoopSpecification
getFreeInvariant
in interface LoopSpecification
public Term getFreeInvariant(Services services)
getFreeInvariant
in interface LoopSpecification
public Term getModifies(LocationVariable heap, Term selfTerm, java.util.Map<LocationVariable,Term> atPres, Services services)
LoopSpecification
getModifies
in interface LoopSpecification
heap
- the heap variable.selfTerm
- the self term.atPres
- the operators used for the pre-heap.services
- the Services object.public Term getModifies(Term selfTerm, java.util.Map<LocationVariable,Term> atPres, Services services)
LoopSpecification
getModifies
in interface LoopSpecification
selfTerm
- the self term.atPres
- the operators used for the pre-heap.services
- the Services object.public ImmutableList<InfFlowSpec> getInfFlowSpecs(LocationVariable heap, Term selfTerm, java.util.Map<LocationVariable,Term> atPres, Services services)
getInfFlowSpecs
in interface LoopSpecification
public ImmutableList<InfFlowSpec> getInfFlowSpecs(LocationVariable heap)
LoopSpecification
getInfFlowSpecs
in interface LoopSpecification
public ImmutableList<InfFlowSpec> getInfFlowSpecs(Services services)
getInfFlowSpecs
in interface LoopSpecification
public Term getVariant(Term selfTerm, java.util.Map<LocationVariable,Term> atPres, Services services)
LoopSpecification
getVariant
in interface LoopSpecification
selfTerm
- the self term.atPres
- the operators used for the pre-heap.services
- the Services object.public java.util.Map<LocationVariable,Term> getInternalInvariants()
LoopSpecification
getInternalInvariants
in interface LoopSpecification
public java.util.Map<LocationVariable,Term> getInternalFreeInvariants()
LoopSpecification
getInternalFreeInvariants
in interface LoopSpecification
public Term getInternalVariant()
LoopSpecification
getInternalVariant
in interface LoopSpecification
public java.util.Map<LocationVariable,Term> getInternalModifies()
LoopSpecification
getInternalModifies
in interface LoopSpecification
public java.util.Map<LocationVariable,ImmutableList<InfFlowSpec>> getInternalInfFlowSpec()
getInternalInfFlowSpec
in interface LoopSpecification
public Term getInternalSelfTerm()
LoopSpecification
getInternalSelfTerm
in interface LoopSpecification
public Term getModifies()
getModifies
in interface LoopSpecification
public java.util.Map<LocationVariable,Term> getInternalAtPres()
LoopSpecification
getInternalAtPres
in interface LoopSpecification
public 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)
LoopSpecification
create
in interface LoopSpecification
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.public 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)
LoopSpecification
create
in interface LoopSpecification
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.public LoopSpecification instantiate(java.util.Map<LocationVariable,Term> invariants, java.util.Map<LocationVariable,Term> freeInvariants, Term variant)
LoopSpecification
instantiate
in interface LoopSpecification
invariants
- the loop invariant clauses for instantiation.freeInvariants
- the "free" loop invariant clauses for instantiation.variant
- the loop variant for instantiation.public 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)
LoopSpecification
configurate
in interface LoopSpecification
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.public LoopSpecification setLoop(LoopStatement loop)
LoopSpecification
setLoop
in interface LoopSpecification
public LoopSpecification setTarget(IProgramMethod newPM)
setTarget
in interface LoopSpecification
public LoopSpecification setInvariant(java.util.Map<LocationVariable,Term> invariants, java.util.Map<LocationVariable,Term> freeInvariants, Term selfTerm, java.util.Map<LocationVariable,Term> atPres, Services services)
LoopSpecification
setInvariant
in interface LoopSpecification
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.public void visit(Visitor v)
LoopSpecification
visit
in interface LoopSpecification
public java.lang.String toString()
toString
in class java.lang.Object
public java.lang.String getPlainText(Services services, boolean usePrettyPrinting, boolean useUnicodeSymbols)
public java.lang.String getPlainText(Services services, java.lang.Iterable<LocationVariable> heapContext, boolean usePrettyPrinting, boolean useUnicodeSymbols)
LoopSpecification
getPlainText
in interface LoopSpecification
services
- the Services object.heapContext
- all corresponding heaps.usePrettyPrinting
- whether the text should be pretty-printed.useUnicodeSymbols
- whether Unicode symbols should be used.public java.lang.String getDisplayName()
SpecificationElement
getDisplayName
in interface SpecificationElement
public IProgramMethod getTarget()
LoopSpecification
getTarget
in interface LoopSpecification
public KeYJavaType getKJT()
SpecificationElement
getKJT
in interface LoopSpecification
getKJT
in interface SpecificationElement
public java.lang.String getName()
SpecificationElement
getName
in interface SpecificationElement
public java.lang.String getUniqueName()
getUniqueName
in interface LoopSpecification
public VisibilityModifier getVisibility()
SpecificationElement
getVisibility
in interface SpecificationElement
public boolean hasInfFlowSpec(Services services)
hasInfFlowSpec
in interface LoopSpecification
public LoopSpecification setTarget(KeYJavaType newKJT, IObserverFunction newPM)
setTarget
in interface LoopSpecification
public Contract.OriginalVariables getOrigVars()
LoopSpecification
getOrigVars
in interface LoopSpecification