Natural
BitString
PrimitiveTypes
b
public
n
public
public
return
IsSet
false
public
return
BitLength
false
n
public
public
return
ToBitString
false
b
public
public
return
ToInteger
false
b
public
public
return
ToHexString
false
b
public
public
return
ToOctalString
false
b
public
public
return
~
false
b1
public
b2
public
public
return
&
false
b1
public
b2
public
public
return
^
false
b1
public
b2
public
public
return
|
false
b
public
n
public
public
return
<<
false
b
public
n
public
public
return
>>
false
b
public
n
public
public
return
>>>
false
BitStringFunctions
&
!
|
^
BooleanFunctions
/
%
x
public
public
return
ToNatural
false
IntegerFunctions
+
StringFunctions
UnlimitedNaturalFunctions
*
true
false
seq
public
public
return
Size
false
*
true
false
seq
public
element
public
public
return
Includes
false
*
true
false
seq
public
element
public
public
return
Excludes
false
*
true
false
seq
public
element
public
public
return
Count
false
*
true
false
seq
public
public
return
IsEmpty
false
*
true
false
seq
public
public
return
NotEmpty
false
*
true
false
seq1
public
*
true
false
seq2
public
public
return
IncludesAll
false
*
true
false
seq1
public
*
true
false
seq2
public
public
return
ExcludesAll
false
*
true
false
seq1
public
*
true
false
seq2
public
public
return
Equals
false
*
true
false
seq
public
index
public
public
return
At
false
*
true
false
seq
public
element
public
public
return
IndexOf
false
*
true
false
seq
public
public
return
First
false
*
true
false
seq
public
public
return
Last
false
*
true
false
seq1
public
*
true
false
seq2
public
*
true
false
public
return
Union
false
*
true
false
seq1
public
*
true
false
seq2
public
*
true
false
public
return
Intersection
false
*
true
false
seq1
public
*
true
false
seq2
public
*
true
false
public
return
Difference
false
*
true
false
seq
public
element
public
*
true
false
public
return
Including
false
*
true
false
seq
public
element
public
index
public
*
true
false
public
return
IncludeAt
false
*
true
false
seq
public
element
public
index
public
*
true
false
public
return
InsertAt
false
*
true
false
seq1
public
*
true
false
seq2
public
index
public
*
true
false
public
return
IncludeAllAt
false
*
true
false
seq
public
element
public
*
true
false
public
return
Excluding
false
*
true
false
seq
public
element
public
*
true
false
public
return
ExcludingOne
false
*
true
false
seq
public
index
public
*
true
false
public
return
ExcludeAt
false
*
true
false
seq
public
element
public
newElement
public
*
true
false
public
return
Replacing
false
*
true
false
seq
public
index
public
element
public
*
true
false
public
return
ReplacingAt
false
*
true
false
seq
public
element
public
newElement
public
*
true
false
public
return
ReplacingOne
false
*
true
false
seq
public
lower
public
upper
public
*
true
false
public
return
Subsequence
false
*
true
false
seq
public
*
true
public
return
ToOrderedSet
false
SequenceFunctions
PrimitiveBehaviors
BasicInputOutput
Concrete unordered, non-unique collection. Supports duplicate entries.
T
false
public
false
Binds Bag<T> to Collection<T>.
Collection<T>
private
true
Bag<T>
Construct a bag and add all elements in the given sequence. post: result.toSequence()->asBag() = seq->asBag()
Elements to be added to the new bag.
*
true
false
seq
public
public
return
Bag
public
true
Destroy this bag.
destroy
public
true
Insert the given element into this bag. Always returns true. post: self.toSequence()->asBag() = self@pre.toSequence()->asBag()->including(element)
Element to be appended to this collection.
element
public
create
public
return
add
public
true
Insert all elements in the given sequence into this bag. Return true if the given sequence is not empty. post: self.toSequence()->asBag() = self@pre.toSequence()->asBag()->union(seq->asBag())
*
true
false
seq
public
public
return
addAll
public
true
Return true if the content of this bag is equal to the given sequence considered as a bag. post: result = (self@pre.toSequence()->asBag() = seq->asBag())
*
true
false
seq
public
public
return
equals
public
true
true
Bag
true
An abstract collection of elements of a specified type <T>. Various concrete subclasses support ordered and unordered collections, with and without duplicates allowed.
T
false
public
Insert the given element into this collection. Return true if a new element is actually inserted. post: result = self.size() > self@pre.size() and result implies self.count(element) = self@pre.count(element)+1 lement)+1
public
return
create
Element to be added to this collection.
element
public
create
add
public
true
Insert all elements in the given sequence into this collection. Returns true if this collection increased in size. post: result = self.size() > self@pre.size() and self.includesAll(seq) sAll(seq)
Elements to be added to this collection.
*
true
false
seq
public
public
return
addAll
public
true
Remove all elements from this collection. post: result = self.isEmpty()
clear
public
true
Return the number of elements in this collection that match a specified element. post: result = self.toSequence()->count(element)
Element to be counted.
element
public
create
public
return
create
count
public
true
true
Return true if the content of this collection is equal to the given sequence. post: result implies self.includesAll(seq)
The elements to which the content of this collection is to be compared.
*
true
false
seq
public
public
return
equals
public
true
true
Return true if this collection does not contain the given element. post: result = self.toSequence()->excludes(element)
Element to be tested for containment.
element
public
create
public
return
create
excludes
public
true
true
Return true if all elements in the given sequence are not in this collection. post: result = self.toSequence()->excludesAll(seq)
Elements to be tested for containment.
*
true
false
seq
public
public
return
excludesAll
public
true
true
Return true if this collection contains the given element. post: result = self.toSequence()->includes(element)
Element to be tested for containment.
element
public
create
public
return
create
includes
public
true
true
Return true if all elements in the given sequence are also in this collection. post: result = self.toSequence()->includesAll(seq)
Elements to be tested for containment.
*
true
false
seq
public
public
return
includesAll
public
true
true
Return true if this collection contains no elements. post: result = self.toSequence()->isEmpty()
public
return
create
isEmpty
public
true
true
Return true if this collection contains at least one element. post: result = self.toSequence()->notEmpty()
public
return
notEmpty
public
true
true
Remove all occurrences of the given element from this collection and return the count of elements removed removed. post: result = self@pre.count(element) and self.size() = self@pre.size() - result and self@pre.toSequence()->forAll(e | self.count(e) = if e = element then 0 else self@pre.count(e) endif ) hen 0
else self@pre.count(e) endif )
element
public
public
return
remove
public
true
Remove all occurrences of all elements in the given sequence from this collection. Return true if the size of this collection changes. post: result = self.size() < self@pre.size() and self.toSequence()->asSet() = self@pre.toSequence()->asSet() - seq->asSet() and self.toSequence()->forAll(e | self.count(e) = self@pre.count(e)) count(e))
Elements to be removed from the collection.
*
true
false
seq
public
public
return
removeAll
public
true
Remove one occurrence of the given element from this collection and return true if an occurrence of element was removed. If the collection is ordered, the first element will be removed. post: result = self@pre.includes(element) and self.size() = self@pre.size() - (if result then 1 else 0) endif and self@pre.toSequence()->forAll(e | self.count(e) = if result and e = element then self@pre.count(e)-1 else self@pre.count(e) endif ) (e)-1
else self@pre.count(e) endif )
Element to be removed from this collection.
element
public
create
public
return
removeOne
public
true
Replace all occurrences of the given element with a new element and return the count of replaced elements. post: result = if element<>newElement then self@pre.count(element) else 0 endif and self.size() = self@pre.size() and self.toSequence()->forAll(e | self.count(e) = if e = newElement then self@pre.count(e)+result else self@pre.count(e) endif ) result
else self@pre.count(e) endif )
Element to be replaced.
element
public
create
Element to replace original element.
newElement
public
create
public
return
replace
public
true
Replace one occurrence of the given element with newElement and return true if an element was replaced. If the collection is ordered, this will be the first occurrence. post: result = (self@pre.includes(element) and element<>newElement) and self.size() = self@pre.size() and self.toSequence()->forAll(e | self.count(e) = if result and e = element then self@pre.count(e)-1 else if result and e = newElement then self@pre.count(e)+1 else self@pre.count(e) endif endif ) f@pre.count(e)+1
else self@pre.count(e) endif endif )
Element to be replaced.
element
public
create
Element to replace the original element.
newElement
public
create
public
return
replaceOne
public
true
Remove all instances of all elements in this collection that are NOT in the given sequence. Return true if the size of this collection changes. post: result = self.size() < self@pre.size() and self.toSequence()->asBag() = self@pre.toSequence()->asBag()->intersection(seq->asSet()) asSet())
Elements to retain.
*
true
false
seq
public
public
return
retainAll
public
true
Return the number of elements contained in this collection. post: result = self@pre.toSequence()->size()
public
return
create
size
public
true
true
Return a sequence (UML ordered, non-unique collection) containing the elements of this collection. If the specific kind of collection orders its elements, then the returned sequence will have this order. Otherwise the order of the elements in the returned sequence is arbitrary. (The requirements on the returned sequence from this operation are specified implicitly by the required behavior of the mutating operations on the various Collection subclasses.)
*
true
false
public
return
create
toSequence
public
true
true
Collection
true
Double-Ended Queue (pronounced "deck"). Concrete ordered, nonunique collection. Supports duplicate entries. Ordered by position. Insertion and removal can occur at the front or the back of a deque. Can operate as FIFO (in at back, out at front). Can operate as Stack (in at front/back, out at front/back).
T
false
public
false
Class to bind Deque<T> to Queue<T>.
Queue<T>
private
true
Deque<T>
Construct a deque and add the elements in the given sequence. post: self.toSequence() = seq
*
true
false
seq
public
create
public
return
Deque
public
true
Destroy this deque.
destroy
public
true
Add element into this deque at the front. Always returns true. post: result = true and self.toSequence() = self@pre.toSequence()->prepend(element) (element)
Element to be added to this collection
element
public
create
public
return
addFirst
public
true
Return, but do not remove, the element at the back of the queue, if one exists. pre: self.notEmpty() post: result = self.toSequence()->last() )
public
return
last
public
true
true
Remove and return the element at the back of the deque if one exists. pre: self.notEmpty() post: result = self@pre.toSequence()->last() and self.toSequence() = self@pre.toSequence->subSequence(1,self@pre.size()-1) .size()-1)
public
return
removeLast
public
true
Remove and return the last occurrence of the given element in this deque. If this deque is empty or the element is not found in this queue, return nothing. pre: self.includes(element) post: result = element and let revSeq = self@pre.toSequence()->reverse() in let index = revSeq.indexOf(element) in self.toSequence() = revSeq->subSequence(1,index-1)->union(revSeq->subSequence(index+1,revSeq->size()))->reverse() revSeq->size()))->reverse()
The element to remove and return from this deque
element
public
create
public
return
removeLastOne
public
true
Deque
true
Concrete ordered, nonunique collection. Supports duplicate entries. Ordered by position in list.
T
false
public
false
Binds List<T> to Bag<T>.
Bag<T>
private
true
List<T>
Construct a list and add all elements in the given sequence post: result.toSequence() = seq
*
true
false
seq
public
create
public
return
List
public
true
Destroy this list
destroy
public
true
Append the given element into this list at the end. Always returns true. post: self.toSequence() = self@pre.toSequence()->append(element) )
Element to be appended to this collection
element
public
create
public
return
add
public
true
Append all elements in the given sequence onto the end of this list. Return true if the given collection is not empty. post: self.toSequence() = self@pre.toSequence()->union(seq) )
*
true
false
seq
public
public
return
addAll
public
true
Insert all elements in the given sequence into this list at the given position index. Return true if the given collection is not empty. pre: index >= 1 and index <= self.size()+1 post: result = self.size() > self@pre.size() and self.toSequence() = Sequence{1..seq->size()}->iterate(i; s = self@pre.toSequence() | s->insertAt(index+i-1, sequence->at(i)) e->at(i))
index
public
*
true
false
seq
public
public
return
addAllAt
public
true
Insert an element into this list at the given position index. Always return true. pre: index > 1 and index <= self.size()+1 post: result = true and self.toSequence() = self@pre.toSequence()->insertAt(index,element) )
index
public
create
element
public
create
public
return
addAt
public
true
Return the element at the given position index or nothing if there is no element at the given position. pre: index > 0 and index <= self.size() post: result = self@pre.toSequence()->at(index) )
The position of the element to be returned
index
public
create
public
return
at
public
true
true
Return true if the content of this list is equal to the given sequence. post: result = (self@pre.toSequence() = seq)
*
true
false
seq
public
public
return
equals
public
true
true
Returns the first element in this list, if one exists pre: self.notEmpty() post: result = self@pre.toSequence()->first()
public
return
first
public
true
true
Return the position of the first occurrence of the given element in this list or nothing if the element is not included in this collection. pre: self.includes(element) post: result = self@pre.toSequence() -> indexOf(element) )
Element for which to retrieve the position post: result = self.toSequence()->indexOf(element)
element
public
create
public
return
indexOf
public
true
true
Returns the last element in this list, if one exists pre: self.notEmpty() post: result = self@pre.toSequence()->first()
public
return
last
public
true
true
Remove all occurrences of the given element from this list and return the count of elements removed. post: self.toSequence() = self@pre.toSequence()->excluding(element)
Element to be removed from this collection
element
public
create
public
return
remove
public
true
Remove all elements in the given sequence from this list. Return true if the size of this list changes. post: self.toSequence() = seq->iterate(element; s = self@pre.toSequence() | s->excluding(element)) )
*
true
false
seq
public
public
return
removeAll
public
true
Remove first occurrence of the given element from this list and return true if an occurrence of element was removed. post: self.toSequence() = let preSeq = self@pre.toSequence() in if result then let index = self@pre.indexOf(element) in self.toSequence() = preSeq->subSequence(1, index-1)-> union(preSeq->subSequence(index+1, self@pre.size())) else preSeq endif (index+1, self@pre.size()))
else preSeq endif
Element to be removed from this collection
element
public
create
public
return
removeOne
public
true
Remove the element at the given position index and shift all trailing elements left by one position. Return the removed element, or nothing if the index is out of bounds. pre: index > 0 and index <= self.size() post: result = self@pre.at(index) and let preSeq = self@pre.toSequence() in self.toSequence() = preSeq->subSequence(1, index-1)->union(preSeq->subSequence(index+1, self@pre.size())) re.size()))
The position of the element to remove
index
public
create
public
return
removeAt
public
true
Replace all occurrences of the given element with a new element and return the count of replaced elements. post: Sequence{1..self.size()}->forAll(i | self.at(i) = if self@pre.at(i) = element then newElement else self@pre.at(i) endif) else self@pre.at(i) endif) i) endif)
Element to be replaced
element
public
create
Element to replace element
newElement
public
create
public
return
replace
public
true
Replace one occurrence of the given element with newElement and return true if an element was replaced. post: Sequence{1..self.size()}->forAll(i | self.at(i) = if result and i = self@pre.indexOf(element) then newElement else self@pre.at(i) endif) else self@pre.at(i) endif) ) endif)
element to replace (first occurrence)
element
public
create
new element to replace first occurrence of element
newElement
public
create
public
return
replaceOne
public
true
Replace the element at the given position index with the given new element. Return the replaced element, or nothing if the index is out of bounds pre: index > 0 and index <= self.size() post: result = self@pre.at(index) and let preSeq = self@pre.toSequence() in self.toSequence() = preSeq->subSequence(1, index-1)->append(newElement)->union(preSeq->subSequence(index+1, self@pre.size())) re.size()))
The position of the element to be replaced by element
index
public
create
Element to replace the element at position index
element
public
create
public
return
replaceAt
public
true
Remove all instances of all elements in this list that are NOT in the given collection. Return true if the size of this collection changes. post: self.toSequence() = (self@pre.toSequence()->asSet() - seq->asSet())->iterate(element; a = self@pre.toSequence() | seq->excluding(element))
*
true
false
seq
public
public
return
retainAll
public
true
Return a new list containing all elements of this list from the lower position index up to and including the upper position index. post: if lower < 1 or upper > self.size() then result.toSequence()->empty() else result.toSequence() = self.toSequence()->subSequence(lower,upper) endif e()->subSequence(lower,upper)
endif
fromIndex
public
create
toIndex
public
create
public
return
subList
public
true
true
List
true
Dictionary of key and value pairs called "entries". Concrete unordered, unique (by key) collection.
Key
false
Value
false
public
A Set of type Set<Map.Entry> for the purpose of returning a set view of entries in a map
Set<Entry>
A Set of type Set<T->Key> for the purpose of returning a set view of keys in a map
Set<Key>
A List of type <T->Value> for the purpose of returning a list view of values n a map
Bag<Value>
An association of value to key. Note that entries are data values that are always passed by copy. Changing an entry returned outside of a map will NOT effect the association within the map.
The key for this association, used for lookup
key
public
An optional value for this association
value
public
Entry
Map<Key,Value>
Construct a map and add the given entries. No two entries may have the same key. pre: entries->isUnique(key) post: result.toSequence()->asSet() = sequence->asSet()
*
entries
public
public
return
Map
public
true
Destroy this map.
destroy
public
true
Remove all entries in this map. post: self.isEmpty()
clear
public
true
Return a set of copies of the entries in this map. post: result.equals(self.toSequence())
public
return
entries
public
true
true
Returns true if this map contains none of the given entries. post: result = self.toSequence()->excludesAll(entries)
Entries to be tested for containment.
*
entries
public
public
return
excludesAll
public
true
true
Returns the value associated with the given key, or nothing if there is no entry in this map with its key equal to key. pre: self.keys().toSequence()->includes(key) post: result = self.toSequence()->select(e | e.key = key).value e
The key for which the value is desired.
key
public
create
public
return
create
get
public
true
true
Return a set of copies of the keys in this map. post: result.equals(self.toSequence().key)
public
return
keys
public
true
true
Returns true if this map contains all of the given entries. post: result = self.entries().includesAll(entries)
The entries to be tested for containment.
*
entries
public
public
return
includesAll
public
true
true
Return true if this map contains an entry with its key equal to the given key post: result = self.keys().includes(key)
A key to be searched for in this map.
key
public
create
public
return
create
includesKey
public
true
true
Return true if an entry in this map has its value equal to value. post: result = self.toSequence()->exists(e | e.value = value ) )
A value to be found in the map.
value
public
create
public
return
includesValue
public
true
true
Return true if this map contains no entries. post: result = self.toSequence()->isEmpty()
public
return
create
isEmpty
public
true
true
Return true if this map contains at least one entry. post: result = self.toSequence()->notEmpty()
public
return
notEmpty
public
true
true
Associate a value with a key, creating a new entry if necessary. Return the previously associated value, or nothing if this is a new entry. post: result = self@pre.get(key) and self.toSequence().key->asSet() = self@pre.toSequence().key->asSet()->including(key) and self.toSequence()->isUnique(key) and self.keys().toSequence()->forAll(k | self.get(k) = if e.key = key then value else self@pre.get(k)) ey = key then value else self@pre.get(k))
Key with which the value is to be associated.
key
public
create
Value to be associated with the key.
value
public
create
public
return
put
public
true
Add all the given entries to this map. Any entry with a key already present in this map replaces the previous entry in this map. No two of the given entries may have the same key. pre: entries->isUnique(key) post: self.toSequence().key->asSet() = self@pre.toSequence().key->asSet()->union(entries->asSet()) and self.toSequence()->isUnique(key) and self.keys().toSequence()->forAll(k | self.get(k) = if entries.key->includes(k) then entries->select(key=k) else self@pre.get(k))
else self@pre.get(k))
The entries to be added.
*
entries
public
putAll
public
true
Remove any association of a value to the given key. Return the value previously associated with the key, or nothing if there was no previous entry for the key pre: self.includesKey(key) post: result = self@pre.get(key) and self.toSequence()->isUnique(key) and self.toSequence()->asSet() = self@pre.toSequence()->reject(e | e.key = key)->asSet() ey)->asSet()
The key that defines the entry to remove.
key
public
create
The value previously associated to key, if there was an entry with its key equal to key
public
return
create
remove
public
true
Remove all associations of a value to any of the given keys. post: self.toSequence()->isUnique(key) and self.toSequence()->asSet() = self@pre.toSequence()->reject(e | keys->includes(e.key))->asSet() ->asSet()
The keys all of whose entries are to be removed.
*
keys
public
removeAll
public
true
Returns the number of entries in this map. post: result = self.toSequence()->size()
public
return
create
size
public
true
true
Return a sequence (UML ordered, non-unique collection) containing copies all entries in this map. The order is arbitrary. (The requirements on the returned sequence from this operation are specified implicitly by the required behavior of the mutating operations of the Map class.)
*
true
false
public
return
create
toSequence
public
true
true
Return a bag of copies of the values in this map. (A bag is returned, since a single value may be associated with more than one entry in the map.) post: result.equals(self.toSequence().value)
public
return
create
values
public
true
true
Map
true
Concrete ordered, unique collection. Does not support duplicate entries. Ordered by position.
T
false
public
false
Binds OrderedSet<T> to Set<T>.
Set<T>
private
true
OrderedSet<T>
private
Constructs an ordered set and adds all elements in the given sequence, in order. post: result.toSequence()->asOrderedSet() = seq->asOrderedSet()
A sequence of entries to be added to this set
*
true
false
seq
public
create
public
return
OrderedSet
public
true
Destroy this ordered set.
destroy
public
true
Append the given element into this ordered set at the end. Return true if a new element is actually inserted. post: self.toSequence()->asOrderedSet() = self@pre.toSequence()->asOrderedSet()->append(element)
True if the element was successfully appended to this collection
public
return
create
Element to be appended to this collection
element
public
create
add
public
true
Append all elements in the given sequence onto the end of this ordered set. Returns true if this collection increased in size. post: self.toSequence()->asOrderedSet() = self@pre.toSequence()->union(seq->asOrderedSet()) )
self.toSequence()->size()
OCL
*
true
false
seq
public
public
return
addAll
public
true
Insert all elements in the given sequence into this ordered set at the given position index. Returns true if the size of the ordered set increases (that is, if at least some of the inserted elements were not duplicates of elements already in the set). pre: index >= 1 and index <= self.size()+1 post: result = self.size() > self@pre.size() and self.toSequence()->asOrderedSet() = Sequence{1..seq->size()}->iterate(i; set = self@pre.toSequence()->asOrderedSet() | set->insertAt(index+i-1, seq->at(i)) eq->at(i))
index
public
create
*
true
false
seq
public
public
return
addAllAt
public
true
Insert an element into this ordered set at the given position index. Return true if the element was actually added to the set. pre: index > 1 and index <= self.size()+1 post: result = (self.size() = self@pre.size() + 1) and self.toSequence()->asOrderedSet() = self@pre.toSequence()->asOrderedSet()->insertAt(index,element) )
index
public
create
element
public
create
public
return
addAt
public
true
Return the element at the given position index or nothing if there is no element at the given position. pre: index > 0 and index <= self.size() post: result = self@pre.toSequence()->at(index) )
The position of the element to be returned
index
public
create
public
return
at
public
true
true
Return true if the content of this ordered set is equal to the given sequence considered as an ordered set. post: result = (self@pre.toSequence()->asOrderedSet() = seq->asOrderedSet())
*
true
false
seq
public
public
return
equals
public
true
true
Returns the first element in this ordered set, if one exists pre: self.notEmpty() post: result = self@pre.toSequence()->first()
public
return
first
public
true
true
Return the position of the first occurrence of the given element in this ordered set or nothing if the element is not included in this collection. pre: self.includes(element) post: result = self@pre.toSequence() -> indexOf(element) )
Element for which to retrieve the position
element
public
create
public
return
indexOf
public
true
true
Returns the last element in this ordered set, if one exists pre: self.notEmpty() post: result = self@pre.toSequence()->last()
public
return
last
public
true
true
Remove all occurrences of the given element from this ordered set and return the count of elements removed. (For an ordered set, this has the same effect as removeOne, since duplicates are not allowed.) post: self.toSequence()->asOrderedSet() = self@pre.toSequence()->asOrderedSet()->excluding(element)
element
public
public
return
remove
public
true
Remove all elements in the given sequence from this ordered set. Return true if the size of this ordered set changes. post: self.toSequence() = seq->iterate(element; s = self@pre.toSequence() | s->excluding(element))
*
true
false
seq
public
public
return
removeAll
public
true
Remove one occurrence of the given element from this ordered set and return true if an occurrence of element was removed. (For an ordered set, this has the same effect as remove, since duplicates are not allowed.) post: self.toSequence()->asOrderedSet() = self@pre.toSequence()->asOrderedSet()->excluding(element)
Element to be removed from this collection
element
public
create
public
return
removeOne
public
true
Remove the element at the given position index and shift all trailing elements left by one position. Return the removed element, or nothing if the index is out of bounds. pre: index > 0 and index <= self.size() post: result = self@pre.at(index) and self.toSequence() = self@pre.toSequence()->excluding(result) )
The position of the element to remove
index
public
create
public
return
removeAt
public
true
Replace all occurrences of the given element with newElement and return the count of replaced elements. (For an ordered set, this has the same effect as replaceOne, since duplicates are not allowed.) post: self.toSequence() = if result then self@pre.toSequence()->excluding(element)->insertAt(newElement, self@pre.indexOf(element)) else self@pre.toSequence() endif self@pre.toSequence()
endif
element to replace (first occurrence)
element
public
create
new element to replace first occurrence of element
newElement
public
create
public
return
replace
public
true
Replace the element at the given position index with the given new element. Return the replaced element, or nothing is the index is out of bounds pre: index > 0 and index <= self.size() post: result = self@pre.at(index) and self.toSequence() = self@pre.toSequence()->excluding(result)->insertAt(index,newElement) ment)
The position of the element to be replaced by element
index
public
create
newElement
public
public
return
replaceAt
public
true
Replace one occurrence of the given element with newElement and return true if an element was replaced. (For an ordered set, this has the same effect as replace, since duplicates are not allowed.) post: self.toSequence() = if result then self@pre.toSequence()->excluding(element)->insertAt(newElement, self@pre.indexOf(element)) else self@pre.toSequence() endif self@pre.toSequence()
endif
element
public
newElement
public
public
return
replaceOne
public
true
Remove all instances of all elements in this ordered set that are NOT in the given sequence. Return true if the size of this collection changes. post: self.toSequence() = (self@pre.toSequence()->asSet() - seq->asSet())->iterate(element; s = self@pre.toSequence() | s->excluding(element))
*
true
false
seq
public
public
return
retainAll
public
true
Return a new ordered set containing all elements of this ordered set from the lower position index up to and including the upper position index. post: if lower < 1 or upper > self.size() then result.toSequence()->empty() else result.toSequence() = self.toSequence()->subSequence(lower,upper) endif e()->subSequence(lower,upper)
endif
lower
public
upper
public
public
return
subOrderedSet
public
true
true
true
OrderedSet
true
First In First Out Queue. Concrete ordered, nonunique collection. Supports duplicate entries. Ordered by position. Considering the queue as a sequence, insertion occurs at the back of the queue, removal at the front.
T
false
public
false
Binds Queue<T> to Collection<T>..
Collection<T>
private
true
Queue<T>
Construct a queue and add all elements in the given sequence. post: result.toSequence() = seq
A sequence of elements of type <T> to be added to the queue
*
true
false
seq
public
create
public
return
Queue
public
true
Destroys this queue.
destroy
public
true
Add the given element into this queue at the back. Always returns true. post: self.toSequence() = self@pre.toSequence()->append(element)
Element to be added to this queue
element
public
create
public
return
add
public
true
Add all elements in the given sequence to this queue at the back. Return true if the given collection is not empty. post: self.toSequence() = self@pre.toSequence()->union(seq)
*
true
false
seq
public
public
return
addAll
public
true
Add the given element into this queue at the back. Always returns true. (This is the same functionality as the add operation.) post: result = true and self.toSequence() = self@pre.toSequence()->append(element) (element)
Element to be added to this collection
element
public
create
public
return
addLast
public
true
Return true if the content of this queue is equal to the given sequence. post: result = self@pre.toSequence() = seq
*
true
false
seq
public
public
return
equals
public
true
true
Return, but do not remove, the element at the front of the queue, if one exists. pre: self.notEmpty() post: result = self.toSequence()->first() )
public
return
first
public
true
true
Remove all occurrences of the given element from this queue and return the count of elements removed. post: self.toSequence() = self@pre.toSequence()->excluding(element)
Element to be removed from this collection
element
public
create
public
return
remove
public
true
Remove all elements in the given collection from this queue. Return true if the size of this queue changes. post: self.toSequence() = seq->iterate(element; s = self@pre.toSequence() | s->excluding(element)) )
*
true
false
seq
public
public
return
removeAll
public
true
Remove the first occurrence of the given element from this queue and return true if an occurrence of element was removed. post: self.toSequence() = let preSeq = self@pre.toSequence() in if result then let index = self@pre.indexOf(element) in self.toSequence() = preSeq->subSequence(1, index-1)-> union(preSeq->subSequence(index+1, self@pre.size())) else preSeq endif (index+1, self@pre.size()))
else preSeq endif
Element to be removed from this collection
element
public
create
public
return
removeOne
public
true
Remove and return the element at the front of the queue if one exists. pre: self.notEmpty() post: result = self@pre.toSequence()->first() and self.toSequence()->self@pre.toSequence()->subSequence(2,self@pre.size()) re.size())
public
return
removeFirst
public
true
Remove and return the first occurrence of the given element in this queue. If this queue is empty or the element is not found in this queue, return nothing. pre: self.includes(element) post: result = element and let preSeq = self@pre.toSequence() in let index = preSeq.indexOf(element) in self.toSequence() = preSeq->subSequence(1,index-1)->union(preSeq->subSequence(index+1,preSeq->size())) ce(index+1,preSeq->size()))
The element to remove and return from this deque
element
public
create
public
return
removeFirstOne
public
true
Replace all occurrences of the given element with a new element and return the count of replaced elements. post: Sequence{1..self.size()}->forAll(i | self.at(i) = if self@pre.at(i) = element then newElement else self@pre.at(i) endif) else self@pre.at(i) endif) i) endif)
Element to be replaced
element
public
create
Element to replace element
newElement
public
create
public
return
replace
public
true
Replace one occurrence of the given element with newElement and return true if an element was replaced. post: Sequence{1..self.size()}->forAll(i | self.at(i) = if result and i = self@pre.indexOf(element) then newElement else self@pre.at(i) endif) else self@pre.at(i) endif) ) endif)
element to replace (first occurrence)
element
public
create
new element to replace first occurrence of element
newElement
public
create
public
return
replaceOne
public
true
Remove all instances of all elements in this queue that are NOT in the given collection. Return true if the size of this collection changes. post: self.toSequence() = (self@pre.toSequence()->asSet() - seq->asSet())->iterate(element; s = self@pre.toSequence() | s->excluding(element))
*
true
false
seq
public
public
return
retainAll
public
true
Queue
true
A concrete unordered, unique collection. Does not support duplicate entries.
T
false
public
false
Binds Set<T> to Collection<T>.
Collection<T>
private
true
Set<T>
Construct a set and add all elements in the given sequence. post: result.toSequence()->asSet() = seq->asSet()
A sequence of elements of type <T> to be added to the set
*
true
false
seq
public
create
public
return
Set
public
true
Destroy this set.
destroy
public
true
Insert the given element into this set. Return true if a new element is actually inserted. post: self.toSequence()->asSet() = self@pre.toSequence()->asSet()->including(element)
Element to be appended to this collection
element
public
create
public
return
add
public
true
Insert all elements in the given sequence into this set. Returns true if this collection increased in size. post: self.toSequence()->asSet() = self@pre.toSequence()->asSet()->union(seq->asSet())
self.toSequence()->size()
OCL
*
true
false
seq
public
public
return
addAll
public
true
The number of elements in this set that match a specified element. post: result = if self@pre.includes(element) then 1 else 0 endif
The element to be counted
element
public
create
public
return
count
public
true
true
Return true if the content of this set is equal to the given sequence considered as a set. post: result = (self@pre.toSequence()->asSet() = seq->asSet())
*
true
false
seq
public
public
return
equals
public
true
true
Set
true
The concrete implementation of the standard library template Set class.
T
false
public
Set<T>
*
true
false
seq
public
public
return
Set
public
destroy
public
public
return
create
element
public
create
add
public
*
true
false
seq
public
public
return
addAll
public
clear
public
element
public
create
public
return
create
count
public
true
*
true
false
seq
public
public
return
equals
public
true
element
public
create
public
return
create
excludes
public
true
*
true
false
seq
public
public
return
excludesAll
public
true
element
public
create
public
return
create
includes
public
true
*
true
false
seq
public
public
return
includesAll
public
true
public
return
create
isEmpty
public
true
public
return
notEmpty
public
true
element
public
public
return
remove
public
*
true
false
seq
public
public
return
removeAll
public
element
public
create
public
return
removeOne
public
element
public
create
newElement
public
create
public
return
replace
public
element
public
create
newElement
public
create
public
return
replaceOne
public
*
true
false
seq
public
public
return
retainAll
public
public
return
create
size
public
true
*
true
false
public
return
create
toSequence
public
true
Set
The concrete implementation of the standard library template OrderedSet class.
T
false
public
OrderedSet<T>
*
true
false
seq
public
public
return
OrderedSet
public
destroy
public
public
return
create
element
public
create
add
public
*
true
false
seq
public
public
return
addAll
public
index
public
create
*
true
false
seq
public
public
return
addAllAt
public
index
public
create
element
public
create
public
return
addAt
public
index
public
create
public
return
at
public
true
clear
public
element
public
create
public
return
create
count
public
true
*
true
false
seq
public
public
return
equals
public
true
element
public
create
public
return
create
excludes
public
true
*
true
false
seq
public
public
return
excludesAll
public
true
public
return
first
public
true
element
public
create
public
return
create
includes
public
true
*
true
false
seq
public
public
return
includesAll
public
true
element
public
create
public
return
indexOf
public
true
public
return
create
isEmpty
public
true
public
return
last
public
true
public
return
notEmpty
public
true
element
public
public
return
remove
public
*
true
false
seq
public
public
return
removeAll
public
index
public
create
public
return
removeAt
public
element
public
create
public
return
removeOne
public
element
public
create
newElement
public
create
public
return
replace
public
index
public
create
newElement
public
public
return
replaceAt
public
element
public
create
newElement
public
create
public
return
replaceOne
public
*
true
false
seq
public
public
return
retainAll
public
public
return
create
size
public
true
lower
public
upper
public
public
return
subOrderedSet
public
true
*
true
false
public
return
create
toSequence
public
true
OrderedSet
The concrete implementation of the standard library template Bag class.
T
false
public
Bag<T>
*
true
false
seq
public
public
return
Bag
public
destroy
public
public
return
create
element
public
create
add
public
*
true
false
seq
public
public
return
addAll
public
clear
public
element
public
create
public
return
create
count
public
true
*
true
false
seq
public
public
return
equals
public
true
element
public
create
public
return
create
excludes
public
true
*
true
false
seq
public
public
return
excludesAll
public
true
element
public
create
public
return
create
includes
public
true
*
true
false
seq
public
public
return
includesAll
public
true
public
return
create
isEmpty
public
true
public
return
notEmpty
public
true
element
public
public
return
remove
public
*
true
false
seq
public
public
return
removeAll
public
element
public
create
public
return
removeOne
public
element
public
create
newElement
public
create
public
return
replace
public
element
public
create
newElement
public
create
public
return
replaceOne
public
*
true
false
seq
public
public
return
retainAll
public
public
return
create
size
public
true
*
true
false
public
return
create
toSequence
public
true
Bag
The concrete implementation of the standard library template List class.
T
false
public
List<T>
*
true
false
seq
public
public
return
List
public
destroy
public
public
return
create
element
public
create
add
public
*
true
false
seq
public
public
return
addAll
public
index
public
create
*
true
false
seq
public
public
return
addAllAt
public
index
public
create
element
public
create
public
return
addAt
public
index
public
create
public
return
at
public
true
clear
public
element
public
create
public
return
create
count
public
true
*
true
false
seq
public
public
return
equals
public
true
element
public
create
public
return
create
excludes
public
true
*
true
false
seq
public
public
return
excludesAll
public
true
public
return
first
public
true
element
public
create
public
return
create
includes
public
true
*
true
false
seq
public
public
return
includesAll
public
true
element
public
create
public
return
indexOf
public
true
public
return
create
isEmpty
public
true
public
return
last
public
true
public
return
notEmpty
public
true
element
public
public
return
remove
public
*
true
false
seq
public
public
return
removeAll
public
index
public
create
public
return
removeAt
public
element
public
create
public
return
removeOne
public
element
public
create
newElement
public
create
public
return
replace
public
index
public
create
newElement
public
public
return
replaceAt
public
element
public
create
newElement
public
create
public
return
replaceOne
public
*
true
false
seq
public
public
return
retainAll
public
public
return
create
size
public
true
lower
public
upper
public
public
return
subList
public
true
*
true
false
public
return
create
toSequence
public
true
List
The concrete implementation of the standard library template Queue class.
T
false
public
Queue<T>
*
true
false
seq
public
public
return
Queue
public
destroy
public
public
return
create
element
public
create
add
public
*
true
false
seq
public
public
return
addAll
public
element
public
create
public
return
addLast
public
clear
public
element
public
create
public
return
create
count
public
true
*
true
false
seq
public
public
return
equals
public
true
element
public
create
public
return
create
excludes
public
true
*
true
false
seq
public
public
return
excludesAll
public
true
element
public
create
public
return
create
includes
public
true
*
true
false
seq
public
public
return
includesAll
public
true
public
return
create
isEmpty
public
true
public
return
notEmpty
public
true
element
public
public
return
remove
public
*
true
false
seq
public
public
return
removeAll
public
public
return
removeFirst
public
element
public
create
public
return
removeFirstOne
public
element
public
create
public
return
removeOne
public
element
public
create
newElement
public
create
public
return
replace
public
element
public
create
newElement
public
create
public
return
replaceOne
public
*
true
false
seq
public
public
return
retainAll
public
public
return
create
size
public
true
*
true
false
public
return
create
toSequence
public
true
Queue
The concrete implementation of the standard library template Deque class.
T
false
public
Deque<T>
*
true
false
seq
public
public
return
Deque
public
destroy
public
public
return
create
element
public
create
add
public
*
true
false
seq
public
public
return
addAll
public
clear
public
Element to be added to this collection
element
public
create
public
return
addFirst
public
element
public
create
public
return
addLast
public
element
public
create
public
return
create
count
public
true
*
true
false
seq
public
public
return
equals
public
true
element
public
create
public
return
create
excludes
public
true
*
true
false
seq
public
public
return
excludesAll
public
true
element
public
create
public
return
create
includes
public
true
*
true
false
seq
public
public
return
includesAll
public
true
public
return
create
isEmpty
public
true
public
return
last
public
true
public
return
notEmpty
public
true
element
public
public
return
remove
public
*
true
false
seq
public
public
return
removeAll
public
public
return
removeFirst
public
element
public
create
public
return
removeFirstOne
public
public
return
removeLast
public
The element to remove and return from this deque
element
public
create
public
return
removeLastOne
public
element
public
create
public
return
removeOne
public
element
public
create
newElement
public
create
public
return
replace
public
element
public
create
newElement
public
create
public
return
replaceOne
public
*
true
false
seq
public
public
return
retainAll
public
public
return
create
size
public
true
*
true
false
public
return
create
toSequence
public
true
Deque
The concrete implementation of the standard library template Map class.
Key
false
Value
false
public
A Set of type Set<Map.Entry> for the purpose of returning a set view of entries in a map
Set<Entry>
A Set of type Set<T->Key> for the purpose of returning a set view of keys in a map
Set<Key>
A List of type <T->Value> for the purpose of returning a list view of values n a map
Bag<Value>
An association of value to key. Note that entries are data values that are always passed by copy. Changing an entry returned outside of a map will NOT effect the association within the map.
The key for this association, used for lookup
key
public
An optional value for this association
value
public
Entry
Map<Key,Value>
*
entries
public
public
return
Map
public
destroy
public
clear
public
public
return
entries
public
true
*
entries
public
public
return
excludesAll
public
true
key
public
create
The value that is associated with key, or nothing if no entry exists with its key equal to key
public
return
create
get
public
true
public
return
keys
public
true
*
entries
public
public
return
includesAll
public
true
key
public
create
True if this map contains an entry with its key equal to key
public
return
create
includesKey
public
true
value
public
create
public
return
includesValue
public
true
public
return
create
isEmpty
public
true
public
return
notEmpty
public
true
key
public
create
value
public
create
public
return
put
public
*
entries
public
putAll
public
key
public
create
public
return
create
remove
public
*
keys
public
removeAll
public
public
return
create
size
public
true
*
true
false
public
return
create
toSequence
public
true
public
return
create
values
public
true
Map
Impl
CollectionClasses
T
false
public
*
true
false
seq
public
index
public
public
return
at
false
T
false
public
*
true
false
seq
public
element
public
public
return
count
false
T
false
public
*
true
false
seq1
public
*
true
false
seq2
public
*
true
false
public
return
difference
false
T
false
public
*
true
false
seq1
public
*
true
false
seq2
public
public
return
equals
false
T
false
public
*
true
false
seq
public
index
public
*
true
false
public
return
excludeAt
false
T
false
public
*
true
false
seq
public
element
public
public
return
excludes
false
T
false
public
*
true
false
seq1
public
*
true
false
seq2
public
public
return
excludesAll
false
T
false
public
*
true
false
seq
public
element
public
*
true
false
public
return
excluding
false
T
false
public
*
true
false
seq
public
element
public
*
true
false
public
return
excludingOne
false
T
false
public
*
true
false
seq
public
public
return
first
false
T
false
public
*
true
false
seq1
public
*
true
false
seq2
public
index
public
*
true
false
public
return
includeAllAt
false
T
false
public
*
true
false
seq
public
element
public
index
public
*
true
false
public
return
includeAt
false
T
false
public
*
true
false
seq
public
element
public
public
return
includes
false
T
false
public
*
true
false
seq1
public
*
true
false
seq2
public
public
return
includesAll
false
T
false
public
*
true
false
seq
public
element
public
*
true
false
public
return
including
false
T
false
public
*
true
false
seq
public
element
public
public
return
indexOf
false
T
false
public
*
true
false
seq
public
element
public
index
public
*
true
false
public
return
insertAt
false
T
false
public
*
true
false
seq1
public
*
true
false
seq2
public
*
true
false
public
return
intersection
false
T
false
public
*
true
false
seq
public
public
return
isEmpty
false
T
false
public
*
true
false
seq
public
public
return
last
false
T
false
public
*
true
false
seq
public
public
return
notEmpty
false
T
false
public
*
true
false
seq
public
element
public
newElement
public
*
true
false
public
return
replacing
false
T
false
public
*
true
false
seq
public
index
public
element
public
*
true
false
public
return
replacingAt
false
T
false
public
*
true
false
seq
public
element
public
newElement
public
*
true
false
public
return
replacingOne
false
T
false
public
*
true
false
seq
public
public
return
size
false
T
false
public
*
true
false
seq
public
lower
public
upper
public
*
true
false
public
return
subsequence
false
T
false
public
*
true
false
seq
public
*
true
public
return
toOrderedSet
false
T
false
public
*
true
false
seq1
public
*
true
false
seq2
public
*
true
false
public
return
union
false
T
false
public
*
true
false
seq
public
inout
element
public
*
true
false
public
return
add
false
T
false
public
*
true
false
seq1
public
*
true
false
seq2
public
index
public
*
true
false
public
return
addAll
false
T
false
public
*
true
false
seq
public
inout
element
public
index
public
*
true
false
public
return
addAt
false
T
false
public
*
true
false
seq1
public
inout
*
true
false
seq2
public
index
public
*
true
false
public
return
addAllAt
false
T
false
public
*
true
false
seq
public
inout
element
public
*
true
false
public
return
remove
false
T
false
public
*
true
false
seq1
public
inout
*
true
false
seq2
public
*
true
false
public
return
removeAll
false
T
false
public
*
true
false
seq
public
inout
element
public
*
true
false
public
return
removeOne
false
T
false
public
*
true
false
seq
public
inout
index
public
*
true
false
public
return
removeAt
false
T
false
public
*
true
false
seq
public
inout
element
public
newElement
public
*
true
false
public
return
replace
false
T
false
public
*
true
false
seq
public
inout
index
public
element
public
*
true
false
public
return
replaceAt
false
T
false
public
*
true
false
seq
public
inout
element
public
newElement
public
*
true
false
public
return
replaceOne
false
T
false
public
*
true
false
seq
public
inout
clear
false
CollectionFunctions
Library
Alf