InvMap

Object
- InvMap

All Implemented Interfaces:

Serializable
```
public class InvMap
extends Object
implements Serializable
```
Maps ppts to lists of invariants. Has an iterator to return the ppts in the order they were inserted.
The ppts are used only as keys in this data structure. Do not attempt to look up invariants stored in the ppts; instead, obtain invariants via the get() method.

See Also:

Serialized Form

Constructor Summary

Constructors
Constructor Description

InvMap()

Method Summary

All Methods Instance Methods Concrete Methods
Modifier and Type	Method	Description
`void`	`add(PptTopLevel ppt, Invariant inv)`
`void`	`addPpt(PptTopLevel ppt)`
`List<Invariant>`	`get(PptTopLevel ppt)`
`Iterator<Invariant>`	`invariantIterator()`	Returns an iterator over the invariants in this.
`Iterable<PptTopLevel>`	`pptIterable()`	Returns an iterable over the ppts, in the order they were added to the map.
`Iterator<PptTopLevel>`	`pptIterator()`	Returns an iterator over the ppts, in the order they were added to the map.
`Iterator<PptTopLevel>`	`pptSortedIterator(Comparator<PptTopLevel> c)`
`void`	`put(PptTopLevel ppt, List<Invariant> invs)`
`int`	`size()`
`String`	`toString()`

Methods inherited from class Object
clone, equals, finalize, getClass, hashCode, notify, notifyAll, wait, wait, wait

Constructor Detail
- InvMap
```
public InvMap()
```

Method Detail

addPpt

public void addPpt(PptTopLevel ppt)

put

public void put(PptTopLevel ppt,
                List<Invariant> invs)

add

public void add(PptTopLevel ppt,
                Invariant inv)

get

public List<Invariant> get(@GuardSatisfied InvMap this,
                           PptTopLevel ppt)

pptIterator
```
public Iterator<PptTopLevel> pptIterator(@GuardSatisfied InvMap this)
```
Returns an iterator over the ppts, in the order they were added to the map. Each element is a PptTopLevel. These ppts are only used as keys: do not look in these Ppts to find the invariants associated with them in the InvMap! Use invariantIterator instead.

See Also:

invariantIterator()

pptIterable
```
public Iterable<PptTopLevel> pptIterable(@GuardSatisfied InvMap this)
```
Returns an iterable over the ppts, in the order they were added to the map. Each element is a PptTopLevel. These ppts are only used as keys: do not look in these Ppts to find the invariants associated with them in the InvMap! Use invariantIterator instead.

See Also:

invariantIterator()

pptSortedIterator

public Iterator<PptTopLevel> pptSortedIterator(Comparator<PptTopLevel> c)

invariantIterator
```
public Iterator<Invariant> invariantIterator()
```
Returns an iterator over the invariants in this.

toString

@SideEffectFree
public String toString(@GuardSatisfied InvMap this)

Overrides:: toString in class Object

size
```
@Pure
public int size()
```