de.uka.ilkd.key.speclang

Class LoopSpecImpl

java.lang.Object

de.uka.ilkd.key.speclang.LoopSpecImpl

All Implemented Interfaces:

LoopSpecification, SpecificationElement

public final class LoopSpecImpl
extends java.lang.Object
implements LoopSpecification

Standard implementation of the LoopInvariant interface.

Field Summary

Fields

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 Summary

Constructors

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.

Method Summary

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.

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, wait, wait, wait

Field Detail

loop

private final LoopStatement loop

pm

private final IProgramMethod pm

kjt

private final KeYJavaType kjt

originalInvariants

private final java.util.Map<LocationVariable,Term> originalInvariants

originalFreeInvariants

private final java.util.Map<LocationVariable,Term> originalFreeInvariants

originalModifies

private final java.util.Map<LocationVariable,Term> originalModifies

originalInfFlowSpecs

private final java.util.Map<LocationVariable,ImmutableList<InfFlowSpec>> originalInfFlowSpecs

originalVariant

private final Term originalVariant

originalSelfTerm

private final Term originalSelfTerm

localIns

private final ImmutableList<Term> localIns

localOuts

private final ImmutableList<Term> localOuts

originalAtPres

private final java.util.Map<LocationVariable,Term> originalAtPres

Constructor Detail

LoopSpecImpl

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)

Creates a loop invariant.

Parameters:

loop - the loop to which the invariant belongs

invariant - the invariant formula

modifies - the modifier set

infFlowSpecs - low variables for information flow

variant - the variant term

selfTerm - the term used for the receiver object

heapAtPre - the term used for the at pre heap

LoopSpecImpl

public 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.

Method Detail

getReplaceMap

private java.util.Map<Term,Term> getReplaceMap(Term selfTerm,
                                               java.util.Map<LocationVariable,Term> atPres,
                                               Services services)

getInverseReplaceMap

private java.util.Map<Term,Term> getInverseReplaceMap(Term selfTerm,
                                                      java.util.Map<LocationVariable,Term> atPres,
                                                      Services services)

getLoop

public LoopStatement getLoop()

Description copied from interface: LoopSpecification

Returns the loop to which the invariant belongs.

Specified by:

getLoop in interface LoopSpecification

getInvariant

public Term getInvariant(LocationVariable heap,
                         Term selfTerm,
                         java.util.Map<LocationVariable,Term> atPres,
                         Services services)

Description copied from interface: LoopSpecification

Returns the invariant formula.

Specified by:

getInvariant in interface LoopSpecification

Parameters:

heap - the heap variable.

selfTerm - the self term.

atPres - the operators used for the pre-heap.

services - the Services object.

Returns:

The invariant formula as a term.

getInvariant

public Term getInvariant(Services services)

Specified by:

getInvariant in interface LoopSpecification

getFreeInvariant

public Term getFreeInvariant(LocationVariable heap,
                             Term selfTerm,
                             java.util.Map<LocationVariable,Term> atPres,
                             Services services)

Description copied from interface: LoopSpecification

Returns the free invariant formula.

Specified by:

getFreeInvariant in interface LoopSpecification

getFreeInvariant

public Term getFreeInvariant(Services services)

Specified by:

getFreeInvariant in interface LoopSpecification

getModifies

public Term getModifies(LocationVariable heap,
                        Term selfTerm,
                        java.util.Map<LocationVariable,Term> atPres,
                        Services services)

Description copied from interface: LoopSpecification

Returns the modifies clause.

Specified by:

getModifies in interface LoopSpecification

Parameters:

heap - the heap variable.

selfTerm - the self term.

atPres - the operators used for the pre-heap.

services - the Services object.

Returns:

The modifies clause as a term.

getModifies

public Term getModifies(Term selfTerm,
                        java.util.Map<LocationVariable,Term> atPres,
                        Services services)

Description copied from interface: LoopSpecification

Returns the modifies clause.

Specified by:

getModifies in interface LoopSpecification

Parameters:

selfTerm - the self term.

atPres - the operators used for the pre-heap.

services - the Services object.

Returns:

The modifies clause as a term.

getInfFlowSpecs

public ImmutableList<InfFlowSpec> getInfFlowSpecs(LocationVariable heap,
                                                  Term selfTerm,
                                                  java.util.Map<LocationVariable,Term> atPres,
                                                  Services services)

Specified by:

getInfFlowSpecs in interface LoopSpecification

getInfFlowSpecs

public ImmutableList<InfFlowSpec> getInfFlowSpecs(LocationVariable heap)

Description copied from interface: LoopSpecification

Returns the information flow specification clause.

Specified by:

getInfFlowSpecs in interface LoopSpecification

getInfFlowSpecs

public ImmutableList<InfFlowSpec> getInfFlowSpecs(Services services)

Specified by:

getInfFlowSpecs in interface LoopSpecification

getVariant

public Term getVariant(Term selfTerm,
                       java.util.Map<LocationVariable,Term> atPres,
                       Services services)

Description copied from interface: LoopSpecification

Returns the variant term.

Specified by:

getVariant in interface LoopSpecification

Parameters:

selfTerm - the self term.

atPres - the operators used for the pre-heap.

services - the Services object.

Returns:

The variant term.

getInternalInvariants

public java.util.Map<LocationVariable,Term> getInternalInvariants()

Description copied from interface: LoopSpecification

Returns the term internally used for the invariant. Use with care - it is likely that this is *not* the right "self" for you.

Specified by:

getInternalInvariants in interface LoopSpecification

Returns:

The map with an invariant for each heap location.

getInternalFreeInvariants

public java.util.Map<LocationVariable,Term> getInternalFreeInvariants()

Description copied from interface: LoopSpecification

Returns the term internally used for the "free" invariant. Use with care - it is likely that this is *not* the right "self" for you.

Specified by:

getInternalFreeInvariants in interface LoopSpecification

Returns:

The map with a "free" invariant for each heap location.

getInternalVariant

public Term getInternalVariant()

Description copied from interface: LoopSpecification

Returns the term internally used for the variant. Use with care - it is likely that this is *not* the right "self" for you.

Specified by:

getInternalVariant in interface LoopSpecification

Returns:

The variant clause as a term.

getInternalModifies

public java.util.Map<LocationVariable,Term> getInternalModifies()

Description copied from interface: LoopSpecification

Returns the term internally used for the modifies clause. Use with care - it is likely that this is *not* the right "self" for you.

Specified by:

getInternalModifies in interface LoopSpecification

Returns:

The map with a modifies clause for each heap location.

getInternalInfFlowSpec

public java.util.Map<LocationVariable,ImmutableList<InfFlowSpec>> getInternalInfFlowSpec()

Specified by:

getInternalInfFlowSpec in interface LoopSpecification

getInternalSelfTerm

public Term getInternalSelfTerm()

Description copied from interface: LoopSpecification

Returns the term internally used for self. Use with care - it is likely that this is *not* the right "self" for you.

Specified by:

getInternalSelfTerm in interface LoopSpecification

getModifies

public Term getModifies()

Specified by:

getModifies in interface LoopSpecification

getInternalAtPres

public java.util.Map<LocationVariable,Term> getInternalAtPres()

Description copied from interface: LoopSpecification

Returns operators internally used for the pre-heap.

Specified by:

getInternalAtPres in interface LoopSpecification

Returns:

The map storing the operators.

create

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)

Description copied from interface: LoopSpecification

Create and return a new loop specification element from the existing one where the arguments given are replaced.

Specified by:

create in interface LoopSpecification

Parameters:

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.

Returns:

The new loop specification element.

create

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)

Description copied from interface: LoopSpecification

Create and return a new loop specification element from the existing one where the arguments given are replaced.

Specified by:

create in interface LoopSpecification

Parameters:

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.

Returns:

The new loop specification element.

instantiate

public LoopSpecification instantiate(java.util.Map<LocationVariable,Term> invariants,
                                     java.util.Map<LocationVariable,Term> freeInvariants,
                                     Term variant)

Description copied from interface: LoopSpecification

Instantiate a (raw) loop specification with loop invariant clauses and a loop variant, possibly together with (if any) "free" loop invariant clauses.

Specified by:

instantiate in interface LoopSpecification

Parameters:

invariants - the loop invariant clauses for instantiation.

freeInvariants - the "free" loop invariant clauses for instantiation.

variant - the loop variant for instantiation.

Returns:

the instantiated loop specification.

configurate

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)

Description copied from interface: LoopSpecification

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.

Specified by:

configurate in interface LoopSpecification

Parameters:

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.

Returns:

The configured loop specification.

setLoop

public LoopSpecification setLoop(LoopStatement loop)

Description copied from interface: LoopSpecification

Returns a new loop invariant where the loop reference has been replaced with the passed one.

Specified by:

setLoop in interface LoopSpecification

setTarget

public LoopSpecification setTarget(IProgramMethod newPM)

Specified by:

setTarget in interface LoopSpecification

setInvariant

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)

Description copied from interface: LoopSpecification

Returns a new loop invariant where the invariant formula has been replaced with the passed one. Take care: the variables used for the receiver, parameters, and local variables must stay the same!

Specified by:

setInvariant in interface LoopSpecification

Parameters:

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.

Returns:

The new loop invariant.

visit

public void visit(Visitor v)

Description copied from interface: LoopSpecification

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.

Specified by:

visit in interface LoopSpecification

toString

public java.lang.String toString()

Overrides:

toString in class java.lang.Object

getPlainText

public java.lang.String getPlainText(Services services,
                                     boolean usePrettyPrinting,
                                     boolean useUnicodeSymbols)

getPlainText

public java.lang.String getPlainText(Services services,
                                     java.lang.Iterable<LocationVariable> heapContext,
                                     boolean usePrettyPrinting,
                                     boolean useUnicodeSymbols)

Description copied from interface: LoopSpecification

Returns the invariant in pretty plain text format.

Specified by:

getPlainText in interface LoopSpecification

Parameters:

services - the Services object.

heapContext - all corresponding heaps.

usePrettyPrinting - whether the text should be pretty-printed.

useUnicodeSymbols - whether Unicode symbols should be used.

Returns:

a String containing the plain text representation of this invariant.

getDisplayName

public java.lang.String getDisplayName()

Description copied from interface: SpecificationElement

Returns the displayed name.

Specified by:

getDisplayName in interface SpecificationElement

getTarget

public IProgramMethod getTarget()

Description copied from interface: LoopSpecification

Returns the contracted function symbol.

Specified by:

getTarget in interface LoopSpecification

getKJT

public KeYJavaType getKJT()

Description copied from interface: SpecificationElement

Returns the KeYJavaType representing the class/interface to which the specification element belongs.

Specified by:

getKJT in interface LoopSpecification

Specified by:

getKJT in interface SpecificationElement

getName

public java.lang.String getName()

Description copied from interface: SpecificationElement

Returns the unique internal name of the specification element.

Specified by:

getName in interface SpecificationElement

getUniqueName

public java.lang.String getUniqueName()

Specified by:

getUniqueName in interface LoopSpecification

getVisibility

public VisibilityModifier getVisibility()

Description copied from interface: SpecificationElement

Returns the visibility of the invariant (null for default visibility)

Specified by:

getVisibility in interface SpecificationElement

hasInfFlowSpec

public boolean hasInfFlowSpec(Services services)

Specified by:

hasInfFlowSpec in interface LoopSpecification

setTarget

public LoopSpecification setTarget(KeYJavaType newKJT,
                                   IObserverFunction newPM)

Specified by:

setTarget in interface LoopSpecification

getOrigVars

public Contract.OriginalVariables getOrigVars()

Description copied from interface: LoopSpecification

Returns the original Self Variable to replace it easier.

Specified by:

getOrigVars in interface LoopSpecification