11standard 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 elements, members or items of the collection.
20- * Note: In many programming languages `items` is used but that would be confusing because of the SysML v2 Item concept.
21- */
22-
23- feature elements[0..*] nonunique;
24- }
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+ }
2529
2630 abstract datatype OrderedCollection :> Collection {
27- doc
28- /*
29- * OrderedCollection is the abstract supertype for all ordered collection types .
30- */
31-
32- 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;
3337 }
3438
3539 abstract datatype UniqueCollection :> Collection {
36- doc
37- /*
38- * UniqueCollection is the abstract supertype for all collection types with unique elements.
39- */
40-
41- feature elements[0..*] :>> Collection::elements {
42- /* Note: Redefinition of 'elements' is unique by default. */
43- }
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+ }
4449 }
4550
4651 datatype Array :> OrderedCollection {
47- doc
48- /*
49- * An Array is a fixed size, multi-dimensional Collection of which the elements are nonunique and ordered.
50- * Its dimensions specify how many dimensions the array has, and how many elements there are in each dimension.
51- * The rank is equal to the number of dimensions. The flattenedSize is equal to the total number of elements
52- * in the array.
53- *
54- * Feature elements is a flattened sequence of all elements of an Array and can be accessed by a tuple of indices.
55- * The number of indices is equal to rank. The elements are packed according to row-major convention, as in the C programming language.
56- *
57- * The elements of an Array can be assessed by a tuple of indices. The number of indices in such tuple is equal to rank.
58- * The packing of the elements, i.e. the flattened representation, follows the row-major convention,
59- * as in the C programming language.
60- *
61- * Note 1. Feature dimensions may be empty, which denotes a zero dimensional array, allowing an Array to collapse to a single element.
62- * This is useful to allow for specialization of an Array into a type restricted to represent a scalar.
63- * The flattenedSize of a zero dimensional array is 1.
64- *
65- * Note 2: An Array can represent the generalized mathematical concept of an infinite matrix of any rank, i.e. not limited to rank two.
66- */
67-
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 accessed 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+
6872 feature dimensions: Positive[0..*] ordered nonunique {
69- doc
70- /* Feature `dimensions` defines the N-dimensional shape of the Array
71- * The alternative name `shape` (as used in many programming languages) is not used as it would interfere with a geometric shape feature.
72- */
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+ */
7384 }
74- feature rank: Natural[1] = size(dimensions);
75- 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+
7694 inv { flattenedSize == size(elements) }
7795 }
7896
79- datatype Bag :> Collection {
80- doc
81- /*
82- * Bag is a variable-size, unordered collection of nonunique elements.
83- */
84- }
85-
86- datatype Set :> UniqueCollection {
87- doc
88- /*
89- * Set is a variable-size, unordered collection of unique elements.
90- */
91- }
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+ }
92110
93- datatype OrderedSet :> OrderedCollection, UniqueCollection
94- intersects OrderedCollection, UniqueCollection {
95- doc
96- /*
97- * OrderedSet is a variable-size, ordered collection of unique elements.
98- */
99-
100- feature elements[0..*] ordered :>> OrderedCollection::elements, UniqueCollection::elements {
101- /* Note: Redefinition of `elements` is unique by default. */
102- }
103- }
104-
105- datatype List :> OrderedCollection {
106- doc
107- /*
108- * List is a variable-size, ordered collection of nonunique elements.
109- */
110- }
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+ }
111130
112131 datatype KeyValuePair {
113- doc
114- /*
115- * KeyValuePair is a tuple of a key and a value for use in Map collections.
116- * The key must be immutable .
117- */
118-
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+
119138 feature key: Anything[0..*] ordered nonunique;
120139 feature val: Anything[0..*] ordered nonunique;
121140 }
122141
123142 datatype Map :> Collection {
124- doc
125- /*
126- * Map is a variable-size, unordered collection of elements that are key-value pairs.
127- */
128-
129- feature elements: KeyValuePair[0..*] :>> Collection::elements {
130- /* Note: Redefinition of `elements` is unique by default.
131- * The `key` of any `KeyValuePair` must be unique over the collection of `KeyValuePair`.
132- * The `val` does not need to be unique.
133- */
134- }
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+ }
135160 }
136161
137- datatype OrderedMap :> Map {
138- doc
139- /*
140- * OrderedMap is a variable-size, ordered collection of elements that are key-value pairs.
141- */
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+ */
142171
143- feature elements: KeyValuePair[0..*] ordered :>> Map::elements {
144- /* Note: Redefinition of `elements` is unique by default. */
145- }
172+ feature elements: KeyValuePair[0..*] ordered :>> Map::elements, OrderedCollection::elements {
173+ doc
174+ /* Note: Redefinition of elements is unique by default. */
175+ }
146176 }
147-
148177}
0 commit comments