Operations and well-formedness rules

This section contains the operations and well-formedness rules of the collection types.
 

Collection

size() : Integer

The number of elements in the collection self.

post: result = self->iterate(elem; acc : Integer = 0 | acc + 1)

includes(object : T) : Boolean

True if object is an element of self, false otherwise.

post: result = (self->count(object) > 0)

excludes(object : T) : Boolean

True if object is not an element of self, false otherwise.

post: result = (self->count(object) = 0)

count(object : T) : Integer

The number of times that object occurs in the collection self.

post: result = self->iterate( elem; acc : Integer = 0 |
    if elem = object then acc + 1 else acc endif)

includesAll(c2 : Collection(T)) : Boolean

Does self contain all the elements of c2 ?

post: result = c2->forAll(elem | self->includes(elem))

excludesAll(c2 : Collection(T)) : Boolean

Does self contain none of the elements of c2 ?

post: result = c2->forAll(elem | self->excludes(elem))

isEmpty() : Boolean

Is self the empty collection?

post: result = ( self->size() = 0 )

notEmpty() : Boolean

Is self not the empty collection?

post: result = ( self->size() <> 0 )

sum() : T

The addition of all elements in self. Elements must be of a type supporting the + operation. The + operation must take one parameter of type T and be both associative: (a+b)+c = a+(b+c), and commutative: a+b = b+a. Integer and Real fulfill this condition.

post: result = self->iterate( elem; acc : T = 0 | acc + elem )

product(c2: Collection(T2)) : Set( Tuple( first: T, second: T2) )

The cartesian product operation of self and c2.

post: result = self->iterate (e1; acc: Set(Tuple(first: T, second: T2)) = Set{} |
    c2->iterate (e2; acc2: Set(Tuple(first: T, second: T2)) = acc |
    acc2->including (Tuple{first = e1, second = e2}) ) )
 

Set

union(s : Set(T)) : Set(T)

The union of self and s.

post: result->forAll(elem | self->includes(elem) or s->includes(elem))
post: self ->forAll(elem | result->includes(elem))
post: s ->forAll(elem | result->includes(elem))

union(bag : Bag(T)) : Bag(T)

The union of self and bag.

post: result->forAll(elem | result->count(elem) = self->count(elem) + bag->count(elem))
post: self->forAll(elem | result->includes(elem))
post: bag ->forAll(elem | result->includes(elem))

= (s : Set(T)) : Boolean

Evaluates to true if self and s contain the same elements.

post: result = (self->forAll(elem | s->includes(elem)) and
    s->forAll(elem | self->includes(elem)) )

intersection(s : Set(T)) : Set(T)

The intersection of self and s (i.e, the set of all elements that are in both self and s).

post: result->forAll(elem | self->includes(elem) and s->includes(elem))
post: self->forAll(elem | s ->includes(elem) = result->includes(elem))
post: s ->forAll(elem | self->includes(elem) = result->includes(elem))

intersection(bag : Bag(T)) : Set(T)

The intersection of self and bag.

post: result = self->intersection( bag->asSet )

­ (s : Set(T)) : Set(T)

The elements of self, which are not in s.

post: result->forAll(elem | self->includes(elem) and s->excludes(elem))
post: self ->forAll(elem | result->includes(elem) = s->excludes(elem))

including(object : T) : Set(T)

The set containing all elements of self plus object.

post: result->forAll(elem | self->includes(elem) or (elem = object))
post: self- >forAll(elem | result->includes(elem))
post: result->includes(object)

excluding(object : T) : Set(T)

The set containing all elements of self without object.

post: result->forAll(elem | self->includes(elem) and (elem <> object))
post: self- >forAll(elem | result->includes(elem) = (object <> elem))
post: result->excludes(object)

symmetricDifference(s : Set(T)) : Set(T)

The sets containing all the elements that are in self or s, but not in both.

post: result->forAll(elem | self->includes(elem) xor s->includes(elem))
post: self->forAll(elem | result->includes(elem) = s ->excludes(elem))
post: s ->forAll(elem | result->includes(elem) = self->excludes(elem))

count(object : T) : Integer

The number of occurrences of object in self.

post: result <= 1

flatten() : Set(T2)

If the element type is not a collection type this result in the same self. If the element type is a collection type, the result is the set containing all the elements of all the elements of self.

post: result = if self.type.elementType.oclIsKindOf(CollectionType) then
                            self->iterate(c; acc : Set() = Set{} |
                                    acc->union(c->asSet() ) )
                    else
                            self
                    endif

asSet() : Set(T)

A Set identical to self. This operation exists for convenience reasons.

post: result = self

asOrderedSet() : OrderedSet(T)

An OrderedSet that contains all the elements from self, in undefined order.

post: result->forAll(elem | self->includes(elem))

asSequence() : Sequence(T)

A Sequence that contains all the elements from self, in undefined order.

post: result->forAll(elem | self->includes(elem))
post: self->forAll(elem | result->count(elem) = 1)

asBag() : Bag(T)

The Bag that contains all the elements from self.

post: result->forAll(elem | self->includes(elem))
post: self->forAll(elem | result->count(elem) = 1)
 

OrderedSet


append (object: T) : OrderedSet(T)

The set of elements, consisting of all elements of self, followed by object.

post: result->size() = self->size() + 1
post: result->at(result->size() ) = object
post: Sequence{1..self->size() }->forAll(index : Integer |
        result->at(index) = self ->at(index))

prepend(object : T) : OrderedSet(T)

The sequence consisting of object, followed by all elements in self.

post: result->size = self->size() + 1
post: result->at(1) = object
post: Sequence{1..self->size()}->forAll(index : Integer |
        self->at(index) = result->at(index + 1))

insertAt(index : Integer, object : T) : OrderedSet(T)

The set consisting of self with object inserted at position index.

post: result->size = self->size() + 1
post: result->at(index) = object
post: Sequence{1..(index - 1)}->forAll(i : Integer |
        self->at(i) = result->at(i))
post: Sequence{(index + 1)..self->size()}->forAll(i : Integer |
        self->at(i) = result->at(i + 1))

subOrderedSet(lower : Integer, upper : Integer) : OrderedSet(T)

The sub-set of self starting at number lower, up to and including element number upper.

pre : 1 <= lower
pre : lower <= upper
pre : upper <= self->size()
post: result->size() = upper -lower + 1
post: Sequence{lower..upper}->forAll( index |
        result->at(index - lower + 1) =
            self->at(index))

at(i : Integer) : T

The i-th element of self.

pre : i >= 1 and i <= self->size()

indexOf(obj : T) : Integer

The index of object obj in the sequence.

pre : self->includes(obj)
post : self->at(i) = obj

first() : T

The first element in self.

post: result = self->at(1)

last() : T

The last element in self.

post: result = self->at(self->size() )
 

Bag

= (bag : Bag(T)) : Boolean

True if self and bag contain the same elements, the same number of times.

post: result = (self->forAll(elem | self->count(elem) = bag->count(elem)) and
        bag->forAll(elem | bag->count(elem) = self->count(elem)) )

union(bag : Bag(T)) : Bag(T)

The union of self and bag.

post: result->forAll( elem | result->count(elem) = self->count(elem) + bag->count(elem))
post: self ->forAll( elem | result->count(elem) = self->count(elem) + bag->count(elem))
post: bag ->forAll( elem | result->count(elem) = self->count(elem) + bag->count(elem))

union(set : Set(T)) : Bag(T)

The union of self and set.

post: result->forAll(elem | result->count(elem) = self->count(elem) + set->count(elem))
post: self ->forAll(elem | result->count(elem) = self->count(elem) + set->count(elem))
post: set ->forAll(elem | result->count(elem) = self->count(elem) + set->count(elem))

intersection(bag : Bag(T)) : Bag(T)

The intersection of self and bag.

post: result->forAll(elem |
    result->count(elem) = self->count(elem).min(bag->count(elem)) )
post: self->forAll(elem |
    result->count(elem) = self->count(elem).min(bag->count(elem)) )
post: bag->forAll(elem |
    result->count(elem) = self->count(elem).min(bag->count(elem)) )

intersection(set : Set(T)) : Set(T)

The intersection of self and set.

post: result->forAll(elem|result->count(elem) = self->count(elem).min(set->count(elem)) )
post: self ->forAll(elem|result->count(elem) = self->count(elem).min(set->count(elem)) )
post: set ->forAll(elem|result->count(elem) = self->count(elem).min(set->count(elem)) )

including(object : T) : Bag(T)

The bag containing all elements of self plus object.

post: result->forAll(elem |
    if elem = object then
        result->count(elem) = self->count(elem) + 1
    else
        result->count(elem) = self->count(elem)
    endif)
post: self->forAll(elem |
    if elem = object then
        result->count(elem) = self->count(elem) + 1
    else
        result->count(elem) = self->count(elem)
     endif)

excluding(object : T) : Bag(T)

The bag containing all elements of self apart from all occurrences of object.

post: result->forAll(elem |
    if elem = object then
        result->count(elem) = 0
    else
        result->count(elem) = self->count(elem)
    endif)
post: self->forAll(elem |
    if elem = object then
        result->count(elem) = 0
    else
        result->count(elem) = self->count(elem)
    endif)

count(object : T) : Integer

The number of occurrences of object in self.

flatten() : Bag(T2)

If the element type is not a collection type this result in the same bag. If the element type is a collection type, the result is the bag containing all the elements of all the elements of self.

post: result = if self.type.elementType.oclIsKindOf(CollectionType) then
                            self->iterate(c; acc : Bag() = Bag{} |
                            acc->union(c->asBag() ) )
                    else
                            self
                    endif

asBag() : Bag(T)

A Bag identical to self. This operation exists for convenience reasons.

post: result = self

asSequence() : Sequence(T)

A Sequence that contains all the elements from self, in undefined order.

post: result->forAll(elem | self->count(elem) = result->count(elem))
post: self ->forAll(elem | self->count(elem) = result->count(elem))

asSet() : Set(T)

The Set containing all the elements from self, with duplicates removed.

post: result->forAll(elem | self ->includes(elem))
post: self ->forAll(elem | result->includes(elem))

asOrderedSet() : OrderedSet(T)

An OrderedSet that contains all the elements from self, in undefined order, with duplicates removed.

post: result->forAll(elem | self ->includes(elem))
post: self ->forAll(elem | result->includes(elem))
post: self ->forAll(elem | result->count(elem) = 1)

Sequence

count(object : T) : Integer

The number of occurrences of object in self.

= (s : Sequence(T)) : Boolean

True if self contains the same elements as s in the same order.

post: result = Sequence{1..self->size()}->forAll(index : Integer |
                self->at(index) = s->at(index))
        and
                self->size() = s->size()

union (s : Sequence(T)) : Sequence(T)

The sequence consisting of all elements in self, followed by all elements in s.

post: result->size() = self->size() + s->size()
post: Sequence{1..self->size()}->forAll(index : Integer |
        self->at(index) = result->at(index))
post: Sequence{1..s->size()}->forAll(index : Integer |
        s->at(index) = result->at(index + self->size() )))

flatten() : Sequence(T2)

If the element type is not a collection type this result in the same self. If the element type is a collection type, the result is the seuqnce containing all the elements of all the elements of self. The order of the elements is partial.

post: result = if self.type.elementType.oclIsKindOf(CollectionType) then
                            self->iterate(c; acc : Sequence() = Sequence{} |
                                acc->union(c->asSequence() ) )
                    else
                            self
                    endif

append (object: T) : Sequence(T)

The sequence of elements, consisting of all elements of self, followed by object.

post: result->size() = self->size() + 1
post: result->at(result->size() ) = object
post: Sequence{1..self->size() }->forAll(index : Integer |
        result->at(index) = self ->at(index))

prepend(object : T) : Sequence(T)

The sequence consisting of object, followed by all elements in self.

post: result->size = self->size() + 1
post: result->at(1) = object
post: Sequence{1..self->size()}->forAll(index : Integer |
        self->at(index) = result->at(index + 1))

insertAt(index : Integer, object : T) : Sequence(T)

The sequence consisting of self with object inserted at position index.

post: result->size = self->size() + 1
post: result->at(index) = object
post: Sequence{1..(index - 1)}->forAll(i : Integer |
            self->at(i) = result->at(i))
post: Sequence{(index + 1)..self->size()}->forAll(i : Integer |
            self->at(i) = result->at(i + 1))

subSequence(lower : Integer, upper : Integer) : Sequence(T)

The sub-sequence of self starting at number lower, up to and including element number upper.

pre : 1 <= lower
pre : lower <= upper
pre : upper <= self->size()
post: result->size() = upper -lower + 1
post: Sequence{lower..upper}->forAll( index |
        result->at(index - lower + 1) =
                self->at(index))

at(i : Integer) : T

The i-th element of sequence.

pre : i >= 1 and i <= self->size()

indexOf(obj : T) : Integer

The index of object obj in the sequence.

pre : self->includes(obj)
post : self->at(i) = obj

first() : T

The first element in self.

post: result = self->at(1)

last() : T

The last element in self.

post: result = self->at(self->size() )

including(object : T) : Sequence(T)

The sequence containing all elements of self plus object added as the last element.

post: result = self.append(object)

excluding(object : T) : Sequence(T)

The sequence containing all elements of self apart from all occurrences of object.
The order of the remaining elements is not changed.

post:result->includes(object) = false
post: result->size() = self->size() - self->count(object)
post: result = self->iterate(elem; acc : Sequence(T)
        = Sequence{}|
            if elem = object then acc else acc->append(elem) endif )

asBag() : Bag(T)

The Bag containing all the elements from self, including duplicates.

post: result->forAll(elem | self->count(elem) = result->count(elem) )
post: self->forAll(elem | self->count(elem) = result->count(elem) )

asSequence() : Sequence(T)

The Sequence identical to the object itself. This operation exists for convenience reasons.

post: result = self

asSet() : Set(T)

The Set containing all the elements from self, with duplicated removed.

post: result->forAll(elem | self ->includes(elem))
post: self ->forAll(elem | result->includes(elem))

asOrderedSet() : OrderedSet(T)

An OrderedSet that contains all the elements from self, in the same order, with duplicates removed.

post: result->forAll(elem | self ->includes(elem))
post: self ->forAll(elem | result->includes(elem))
post: self ->forAll(elem | result->count(elem) = 1)
post: self ->forAll(elem1, elem2 |
        self->indexOf(elem1) < self->indexOf(elem2)
                implies result->indexOf(elem1) < result->indexOf(elem2) )