IntVector (Kodkod API)

All Superinterfaces:

IntCollection

All Known Implementing Classes:

AbstractIntVector, ArrayIntVector
```
public interface IntVector
extends IntCollection
```
A resizable array of integers.

Author:

Emina Torlak

Specfields:

length: int

elements: [0..size) ->one int

Method Summary

All Methods Instance Methods Abstract Methods
Modifier and Type	Method and Description
`boolean`	`add(int element)` Adds the specified element to the end of this vector (optional operation), and returns true if this vector has changed as a result of the call.
`void`	`add(int index, int element)` Inserts the specified element at the specified position in this vector (optional operation), and returns true if this vector has changed as a result of the call.
`boolean`	`addAll(IntCollection c)` Appends the specified elements to the end of this vector (optional operation), and returns true if this vector has changed as a result of the call.
`boolean`	`addAll(int index, IntCollection c)` Inserts the specified elements at the specified position in this vector (optional operation), and returns true if this vector has changed as a result of the call.
`void`	`clear()` Removes all of the elements from this vector (optional operation).
`boolean`	`contains(int element)` Returns `true` if this vector contains the specified element.
`boolean`	`equals(Object o)` Compares the specified object with this vector for equality.
`int`	`get(int index)` Returns the element at the specified position in this vector.
`int`	`hashCode()` Returns the hash code value for this vector.
`int`	`indexOf(int element)` Returns the index in this vector of the first occurrence of the specified element, or -1 if this vector does not contain this element.
`boolean`	`isEmpty()` Returns `true` if this vector contains no elements.
`IntIterator`	`iterator()` Returns an iterator over the elements in this vector in proper sequence.
`IntIterator`	`iterator(int fromIndex, int toIndex)` Returns an iterator over the elements in this vector in proper sequence, starting `fromIndex<\tt>, inclusive, and ending at toIndex<\tt>, exclusive.`
`int`	`lastIndexOf(int element)` Returns the index in this vector of the last occurrence of the specified element, or -1 if this vector does not contain this element.
`boolean`	`remove(int i)` Removes the first occurrence of the given integer from this vector, and returns true if this vector has changed as a result of the call.
`boolean`	`removeAll(IntCollection c)` Removes all of this vector's elements that are also contained in the specified collection.
`int`	`removeAt(int index)` Removes the element at the specified position in this vector (optional operation).
`boolean`	`retainAll(IntCollection c)` Retains only the elements in this vector that are contained in the specified collection.
`int`	`set(int index, int element)` Replaces the element at the specified position in this vector with the specified element, and returns the previous element (optional operation).
`int`	`size()` Returns the number of elements in this vector.
`int[]`	`toArray()` Returns an array containing all of the elements in this vector in proper sequence.
`int[]`	`toArray(int[] array)` Copies the components of this vector into the specified array, provided that it is large enough, and returns it.

Methods inherited from interface kodkod.util.ints.IntCollection
containsAll

- Method Detail
  - add
```
boolean add(int element)
```
    Adds the specified element to the end of this vector (optional operation), and returns true if this vector has changed as a result of the call.
    
    Specified by:
    
    add in interface IntCollection
    
    Ensures:
    
    this.length' = this.length + 1 && this.elements' = this.elements + this.length -> element
    
    Returns:
    
    this.elements != this.elements'
    
    Throws:
    
    UnsupportedOperationException - if the add method is not supported by this vector.
    
    IllegalArgumentException - if some aspect of this element prevents it from being added to this vector.
  - add
```
void add(int index,
         int element)
```
    Inserts the specified element at the specified position in this vector (optional operation), and returns true if this vector has changed as a result of the call. Shifts the element currently at that position (if any) and any subsequent elements to the right (adds one to their indices).
    
    Ensures:
    
    this.length' = this.length + 1 && this.elements' = { i: [0..this.length'), e: int | i < index => e = this.elements[i], i = index => e = element, e = this.elements[i-1] }
    
    Throws:
    
    UnsupportedOperationException - if the add method is not supported by this vector.
    
    IllegalArgumentException - if some aspect of the specified element prevents it from being added to this vector.
    
    IndexOutOfBoundsException - if the index is out of range (index < 0 || index > length()).
  - addAll
```
boolean addAll(IntCollection c)
```
    Appends the specified elements to the end of this vector (optional operation), and returns true if this vector has changed as a result of the call.
    
    Specified by:
    
    addAll in interface IntCollection
    
    Ensures:
    
    appends the specified elements to the end of this vector
    
    Returns:
    
    this.elements != this.elements'
    
    Throws:
    
    UnsupportedOperationException - if the add method is not supported by this vector.
    
    IllegalArgumentException - if some aspect of an element in the given vector prevents it from being added to this vector.
  - addAll
```
boolean addAll(int index,
               IntCollection c)
```
    Inserts the specified elements at the specified position in this vector (optional operation), and returns true if this vector has changed as a result of the call. Shifts the element currently at that position (if any) and any subsequent elements to the right.
    
    Ensures:
    
    inserts the specified elements at the specified position in this vector
    
    Returns:
    
    this.elements != this.elements
    
    Throws:
    
    UnsupportedOperationException - if the add method is not supported by this vector.
    
    IllegalArgumentException - if some aspect of an element in the specified collection prevents it from being added to this vector.
    
    IndexOutOfBoundsException - if the index is out of range (index < 0 || index > length()).
  - clear
```
void clear()
```
    Removes all of the elements from this vector (optional operation). This vector will be empty after this call returns (unless it throws an exception).
    
    Specified by:
    
    clear in interface IntCollection
    
    Ensures:
    
    this.length' = 0 && no this.elements'
    
    Throws:
    
    UnsupportedOperationException - if the clear method is not supported by this vector.
  - contains
```
boolean contains(int element)
```
    Returns true if this vector contains the specified element.
    
    Specified by:
    
    contains in interface IntCollection
    
    Returns:
    
    element in this.elements[int]
  - equals
```
boolean equals(Object o)
```
    Compares the specified object with this vector for equality. Returns true if and only if the specified object is also an int vector, both vectors have the same size, and all corresponding pairs of elements in the two vectors are equal.
    
    Overrides:
    
    equals in class Object
    
    Returns:
    
    true if the specified object is equal to this vector.
  - get
```
int get(int index)
```
    Returns the element at the specified position in this vector.
    
    Returns:
    
    this.elements[index]
    
    Throws:
    
    IndexOutOfBoundsException - if the index is out of range (index < 0 || index >= length()).
  - hashCode
```
int hashCode()
```
    Returns the hash code value for this vector. The hash code of an int vector is defined to be the Ints.superFastHash(int[]) of the elements in the vector, taken in the ascending order of indices. This ensures that v1.equals(v2) implies that v1.hashCode()==v2.hashCode() for any two IntVectors v1 and v2, as required by the general contract of the Object.hashCode method.
    
    Overrides:
    
    hashCode in class Object
    
    Returns:
    
    Ints.superFastHash(this.toArray())
  - indexOf
```
int indexOf(int element)
```
    Returns the index in this vector of the first occurrence of the specified element, or -1 if this vector does not contain this element.
    
    Returns:
    
    element in this.elements[int] => min(this.elements.element), -1
  - isEmpty
```
boolean isEmpty()
```
    Returns true if this vector contains no elements.
    
    Specified by:
    
    isEmpty in interface IntCollection
    
    Returns:
    
    no this.elements
  - iterator
```
IntIterator iterator()
```
    Returns an iterator over the elements in this vector in proper sequence.
    
    Specified by:
    
    iterator in interface IntCollection
    
    Returns:
    
    an iterator over the elements in this vector in proper sequence.
  - iterator
```
IntIterator iterator(int fromIndex,
                     int toIndex)
```
    Returns an iterator over the elements in this vector in proper sequence, starting fromIndex<\tt>, inclusive, and ending at toIndex<\tt>, exclusive. If fromIndex<\tt> is less than toIndex<\tt>, then the iterator will return the elements in the descending order.
    Returns: an iterator over the elements in this vector in proper sequence, starting at fromIndex<\tt>, inclusive, and ending at toIndex<\tt>. Throws: IndexOutOfBoundsException - fromIndex !in [0..this.length) || toIndex !in [-1..this.length]
  lastIndexOf int lastIndexOf(int element) Returns the index in this vector of the last occurrence of the specified element, or -1 if this vector does not contain this element. Returns: element in this.elements[int] => max(this.elements.element), -1 remove boolean remove(int i) Removes the first occurrence of the given integer from this vector, and returns true if this vector has changed as a result of the call. Specified by: remove in interface IntCollection Ensures: removes the first occurrence of the given integer from this vector Returns: this.elements != this.elements' Throws: UnsupportedOperationException - this is an unmodifiable collection removeAll boolean removeAll(IntCollection c) Removes all of this vector's elements that are also contained in the specified collection. After this call returns, this collection will contain no elements in common with the specified collection. Returns true if this collection has changed as a result of the call. Specified by: removeAll in interface IntCollection Ensures: removes all of this vector's elements that are also contained in the specified collection Returns: this.elements != this.elements' Throws: NullPointerException - c = null UnsupportedOperationException - this is an unmodifiable collection removeAt int removeAt(int index) Removes the element at the specified position in this vector (optional operation). Shifts any subsequent elements to the left (subtracts one from their indices). Returns the element that was removed from the vector. Ensures: this.length' = this.length - 1 && this.elements' = { i: [0..this.length'), e: int | i < index => e = this.elements[i], e = this.elements[i+1] } Returns: this.elements[index] Throws: UnsupportedOperationException - if the remove method is not supported by this vector. IndexOutOfBoundsException - if the index is out of range (index < 0 || index >= length()). retainAll boolean retainAll(IntCollection c) Retains only the elements in this vector that are contained in the specified collection. In other words, removes from this collection all of its elements that are not contained in the specified collection. Returns true if this collection has changed as a result of the call. Specified by: retainAll in interface IntCollection Ensures: retains only the elements in this vector that are contained in the specified collection Returns: this.elements != this.elements' Throws: NullPointerException - c = null UnsupportedOperationException - this is an unmodifiable collection set int set(int index, int element) Replaces the element at the specified position in this vector with the specified element, and returns the previous element (optional operation). Ensures: this.elements' = this.elements' ++ index -> element Returns: this.elements[index] Throws: UnsupportedOperationException - if the set method is not supported by this vector. IllegalArgumentException - if some aspect of the specified element prevents it from being added to this vector. IndexOutOfBoundsException - if the index is out of range (index < 0 || index >= length()). size int size() Returns the number of elements in this vector. Specified by: size in interface IntCollection Returns: this.length toArray int[] toArray() Returns an array containing all of the elements in this vector in proper sequence. Specified by: toArray in interface IntCollection Returns: an array containing all of the elements in this vector in proper sequence. toArray int[] toArray(int[] array) Copies the components of this vector into the specified array, provided that it is large enough, and returns it. The item at index k in this vector is copied into component k of the given array. If the given array is not large enough, the effect of this method is the same as calling toArray(). Specified by: toArray in interface IntCollection Ensures: array.length>=this.length => all i: [0..this.length) | array'[i] = this.elements[i] Returns: array.length>=this.length => array' else this.toArray() Throws: NullPointerException - array = null

Interface IntVector

Method Summary

Methods inherited from interface kodkod.util.ints.IntCollection

Method Detail

add

add

addAll

addAll

clear

contains

equals

get

hashCode

indexOf

isEmpty

iterator

iterator

lastIndexOf

remove

removeAll

removeAt

retainAll

set

size

toArray

toArray