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 RealFunctions 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 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