Skip to content

Commit 428e7a4

Browse files
seidewitzseidewitz
committed
KERML11-144 Made Collections docs in spec and library file consistent.
1 parent 89fad96 commit 428e7a4

1 file changed

Lines changed: 148 additions & 118 deletions

File tree

‎sysml.library/Kernel Libraries/Kernel Data Type Library/Collections.kerml‎

Lines changed: 148 additions & 118 deletions
Original file line numberDiff line numberDiff line change
@@ -1,147 +1,177 @@
11
standard library package Collections {
2-
doc
3-
/*
4-
* This package defines a standard set of Collection data types. Unlike sequences of values
5-
* defined directly using multiplicity, these data types allow for the possibility of collections
6-
* as elements of collections.
7-
*/
2+
doc
3+
/*
4+
* This package defines a standard set of Collection data types. Unlike sequences of values
5+
* defined directly using multiplicity, these data types allow for the possibility of collections
6+
* as elements of collections.
7+
*/
88

9-
private import Base::*;
10-
private import ScalarValues::*;
11-
private import SequenceFunctions::size;
12-
private import IntegerFunctions::*;
13-
private import ControlFunctions::*;
9+
private import Base::*;
10+
private import ScalarValues::*;
11+
private import SequenceFunctions::size;
12+
private import SequenceFunctions::equals;
13+
private import IntegerFunctions::*;
14+
private import ControlFunctions::*;
1415

15-
abstract datatype Collection {
16-
doc
17-
/*
18-
* Collection is the top level abstract supertype of all collection types.
19-
* The name elements is used to denote the members or contents of the collection.
20-
*/
21-
22-
feature elements[0..*] nonunique;
23-
}
16+
abstract datatype Collection {
17+
doc
18+
/*
19+
* A Collection is a DataValue that represents a collection of elements of a given type.
20+
*/
21+
22+
feature elements[0..*] nonunique {
23+
doc
24+
/*
25+
* The contents of the Collection.
26+
*/
27+
}
28+
}
2429

2530
abstract datatype OrderedCollection :> Collection {
26-
doc
27-
/*
28-
* OrderedCollection is the abstract supertype for all ordered collection types.
29-
*/
30-
31-
feature elements[0..*] ordered nonunique :>> Collection::elements;
31+
doc
32+
/*
33+
* An OrderedCollection is a Collection of which the elements are ordered and not necessarily unique.
34+
*/
35+
36+
feature elements[0..*] ordered nonunique :>> Collection::elements;
3237
}
3338

3439
abstract datatype UniqueCollection :> Collection {
35-
doc
36-
/*
37-
* UniqueCollection is the abstract supertype for all collection types with unique elements.
38-
*/
39-
40-
feature elements[0..*] :>> Collection::elements {
41-
/* Note: Redefinition of 'elements' is unique by default. */
42-
}
40+
doc
41+
/*
42+
* A UniqueCollection is a Collection of which the elements are unique and not necessarily ordered.
43+
*/
44+
45+
feature elements[0..*] :>> Collection::elements {
46+
doc
47+
/* Note: Redefinition of 'elements' is unique by default. */
48+
}
4349
}
4450

4551
datatype Array :> OrderedCollection {
46-
doc
47-
/*
48-
* An Array is a fixed size, multi-dimensional Collection of which the elements are nonunique and ordered.
49-
* Its dimensions specify how many dimensions the array has, and how many elements there are in each dimension.
50-
* The rank is equal to the number of dimensions. The flattenedSize is equal to the total number of elements
51-
* in the array.
52-
*
53-
* Feature elements is a flattened sequence of all elements of an Array and can be accessed by a tuple of indices.
54-
* The number of indices is equal to rank. The elements are packed according to row-major convention, as in the C programming language.
55-
*
56-
* The elements of an Array can be assessed by a tuple of indices. The number of indices in such tuple is equal to rank.
57-
* The packing of the elements, i.e. the flattened representation, follows the row-major convention,
58-
* as in the C programming language.
59-
*
60-
* Note 1. Feature dimensions may be empty, which denotes a zero dimensional array, allowing an Array to collapse to a single element.
61-
* This is useful to allow for specialization of an Array into a type restricted to represent a scalar.
62-
* The flattenedSize of a zero dimensional array is 1.
63-
*
64-
* Note 2: An Array can represent the generalized mathematical concept of an infinite matrix of any rank, i.e. not limited to rank two.
65-
*/
66-
52+
doc
53+
/*
54+
* An Array is a fixed size, multi-dimensional Collection of which the elements are nonunique and ordered.
55+
* Its dimensions specify how many dimensions the array has, and how many elements there are in each dimension.
56+
* The rank is equal to the number of dimensions. The flattenedSize is equal to the total number of elements
57+
* in the array.
58+
*
59+
* Feature elements is a flattened sequence of all elements of an Array and can be accessed by a tuple of indices.
60+
* The number of indices is equal to rank. The elements are packed according to row-major convention.
61+
*
62+
* The elements of an Array can be assessed by a tuple of indices. The number of indices in such tuple is equal to rank.
63+
* The elements are packed according to the row-major convention.
64+
*
65+
* Note 1. Feature dimensions may be empty, which denotes a zero dimensional array, allowing an Array to collapse to a single element.
66+
* This is useful to allow for specialization of an Array into a type restricted to represent a scalar.
67+
* The flattenedSize of a zero dimensional array is 1.
68+
*
69+
* Note 2: An Array can represent the generalized mathematical concept of an infinite matrix of any rank, i.e. not limited to rank two.
70+
*/
71+
6772
feature dimensions: Positive[0..*] ordered nonunique {
68-
doc
69-
/* Feature `dimensions` defines the N-dimensional shape of the Array
70-
* The alternative name `shape` (as used in many programming languages) is not used as it would interfere with a geometric shape feature.
71-
*/
73+
doc
74+
/*
75+
* Defines the N-dimensional shape of the Array.
76+
*/
77+
}
78+
79+
feature rank: Natural[1] = size(dimensions) {
80+
doc
81+
/*
82+
* The number of dimensions.
83+
*/
7284
}
73-
feature rank: Natural[1] = size(dimensions);
74-
feature flattenedSize: Positive[1] = dimensions->reduce '*' ?? 1;
85+
86+
feature flattenedSize: Positive[1] = dimensions->reduce '*' ?? 1 {
87+
doc
88+
/*
89+
* The number of elements in the Array, given as the product of the dimensions,
90+
* or 1 if dimensions is empty.
91+
*/
92+
}
93+
7594
inv { flattenedSize == size(elements) }
7695
}
7796

78-
datatype Bag :> Collection {
79-
doc
80-
/*
81-
* Bag is a variable-size, unordered collection of nonunique elements.
82-
*/
83-
}
84-
85-
datatype Set :> UniqueCollection {
86-
doc
87-
/*
88-
* Set is a variable-size, unordered collection of unique elements.
89-
*/
90-
}
97+
datatype Bag :> Collection {
98+
doc
99+
/*
100+
* A Bag is a variable-size Collection of which the elements are unordered and nonunique.
101+
*/
102+
}
103+
104+
datatype Set :> UniqueCollection {
105+
doc
106+
/*
107+
* A Set is a variable-size Collection of which the elements are unique and unordered.
108+
*/
109+
}
91110

92-
datatype OrderedSet :> OrderedCollection, UniqueCollection
93-
intersects OrderedCollection, UniqueCollection {
94-
doc
95-
/*
96-
* OrderedSet is a variable-size, ordered collection of unique elements.
97-
*/
98-
99-
feature elements[0..*] ordered :>> OrderedCollection::elements, UniqueCollection::elements {
100-
/* Note: Redefinition of `elements` is unique by default. */
101-
}
102-
}
103-
104-
datatype List :> OrderedCollection {
105-
doc
106-
/*
107-
* List is a variable-size, ordered collection of nonunique elements.
108-
*/
109-
}
111+
datatype OrderedSet :> OrderedCollection, UniqueCollection
112+
intersects OrderedCollection, UniqueCollection {
113+
doc
114+
/*
115+
* An OrderedSet is a variable-size Collection of which the elements are unique and ordered.
116+
*/
117+
118+
feature elements[0..*] ordered :>> OrderedCollection::elements, UniqueCollection::elements {
119+
doc
120+
/* Note: Redefinition of elements is unique by default. */
121+
}
122+
}
123+
124+
datatype List :> OrderedCollection {
125+
doc
126+
/*
127+
* A List is a variable-size Collection of which the elements are nonunique and ordered.
128+
*/
129+
}
110130

111131
datatype KeyValuePair {
112-
doc
113-
/*
114-
* KeyValuePair is a tuple of a key and a value for use in Map collections.
115-
* The key must be immutable.
116-
*/
117-
132+
doc
133+
/*
134+
* A KeyValuePair is a DataValue that represents a pair of a key and an associated val,
135+
* primarily for use in Maps.
136+
*/
137+
118138
feature key: Anything[0..*] ordered nonunique;
119139
feature val: Anything[0..*] ordered nonunique;
120140
}
121141

122142
datatype Map :> Collection {
123-
doc
124-
/*
125-
* Map is a variable-size, unordered collection of elements that are key-value pairs.
126-
*/
127-
128-
feature elements: KeyValuePair[0..*] :>> Collection::elements {
129-
/* Note: Redefinition of `elements` is unique by default.
130-
* The `key` of any `KeyValuePair` must be unique over the collection of `KeyValuePair`.
131-
* The `val` does not need to be unique.
132-
*/
133-
}
143+
doc
144+
/*
145+
* Map is a variable-size Collection of which the elements are KeyValuePairs.
146+
* The keys must be unique within the Map. The vals need not be unique.
147+
*/
148+
149+
feature elements: KeyValuePair[0..*] :>> Collection::elements {
150+
doc
151+
/* Note: Redefinition of elements is unique by default.*/
152+
}
153+
154+
inv {
155+
elements->forAll{ in e1 : KeyValuePair;
156+
not elements->exists{ in e2 : KeyValuePair;
157+
e1 != e2 and e1.key->equals(e2.key) }
158+
}
159+
}
134160
}
135161

136-
datatype OrderedMap :> Map {
137-
doc
138-
/*
139-
* OrderedMap is a variable-size, ordered collection of elements that are key-value pairs.
140-
*/
162+
datatype OrderedMap :> Map, OrderedCollection {
163+
doc
164+
/*
165+
* An OrderedMap is a variable-size Map that maintains an ordering of its elements.
166+
*
167+
* The ordering may be by key of the KeyValuePair elements, or by order of construction,
168+
* or any other method. The essential aspect is that ordering is maintained and guaranteed across
169+
* accesses to the OrderedMap.
170+
*/
141171

142-
feature elements: KeyValuePair[0..*] ordered :>> Map::elements {
143-
/* Note: Redefinition of `elements` is unique by default. */
144-
}
172+
feature elements: KeyValuePair[0..*] ordered :>> Map::elements, OrderedCollection::elements {
173+
doc
174+
/* Note: Redefinition of elements is unique by default. */
175+
}
145176
}
146-
147177
}

0 commit comments

Comments
 (0)