This page is part of the specification language presented on my "The Art of Programming" pages. A separate page deals with value representation and dynamic aspects of the language.
Option(t)The resulting type is defined by the collection of all values of the bases type added with the value void.
Set(t) OrderedSet(t) List(t)
Record(id1:t1, ..., idn:tn)The order in which the pairs occur in the definition does not matter, with respect to the resulting type.
Func(td, tc) Map(td, tc) OrderedFunc(td, tc) OrderedMap(td, tc)Because for practical reasons the domain and codomain types are often record types, the following short hand constructs are introduced:
Func(td -> idc1:tc1, ..., idcn:tcn) Func(idd1:td1, ..., iddn:tdn -> tc) Func(idd1:td1, ..., iddn:tdn -> idc1:tc1, ..., idcn:tcn) Map(td -> idc1:tc1, ..., idcn:tcn) Map(idd1:td1, ..., iddn:tdn -> tc) Map(idd1:td1, ..., iddn:tdn -> idc1:tc1, ..., idcn:tcn) OrderedFunc(td -> idc1:tc1, ..., idcn:tcn) OrderedFunc(idd1:td1, ..., iddn:tdn -> tc) OrderedFunc(idd1:td1, ..., iddn:tdn -> idc1:tc1, ..., idcn:tcn) OrderedMap(td -> idc1:tc1, ..., idcn:tcn) OrderedMap(idd1:td1, ..., iddn:tdn -> tc) OrderedMap(idd1:td1, ..., iddn:tdn -> idc1:tc1, ..., idcn:tcn)Besides this we also introduce the relation type, which is simply a set of records. A relation type can also be viewed as a map type without codomain. A relation type is defined with the following construct:
Relation(id1:t1, ..., idn:tn)can be seen as a map type without codomain. The relation type is simply a set of records. For this reason, it will also be allowed to use "Set" to indicate a relation, especially unary relations.
Named(id,t) NamedRecord(id, id1:t1, ..., idn:tn)
Union(t1, ..., tn)
Record( set_of_num : Set(Num), a_num : Num )This can simply be resolved by adding an additional logical expression to the record definition in the following manner:
Record( set_of_num : Set(Num), a_num : Num | a_num in set_of_num )As these kind of restrictions occur often, it would be natural to introduce the following short hand notation:
Record( set_of_num : Set(Num), a_num : set_of_num )If one wants to define a type which consists of two sets of numbers and a relation between these two sets of numbers, the following type definition would be needed:
Record( a : Set(Num), b : Set(Num), rel : Relation( c : Num, d : Num ) | All e in rel (e.c in a and e.d in b))When the symbol "^" is introduced to refer to the surrounding type, the above could also described as:
Record( a : Set(Num), b : Set(Num), rel : Relation( c : ^a, d : ^b ))It may seem that with the use of fields as types, that only restrictions can be specified. But this is not the case. Take, for example, the case where in the above type definition the set of the field a is replaced by a mapping in the following manner:
Record( a : Map(Num -> Set(^rel)), b : Set(Num), rel : Relation( c : ^a, d : ^b ))The codomain from the mapping is now a subset of the elements of relation rel, which itself makes use of values from the field a, and thus allows the definition of inifinite circular values.
Actually, by introducing fields as types, the "pointer" concept from traditional imperative programming languages has been introduced.
Using predicates, we could model a collection of persons with hands as follows:
Map ( name : string -> hands : Map ( side : string -> owner : string ) | All p in this (All s in p.hands (s.owner eq p.name)))Again, we could introduce a short-hand notation for this using the "^"-symbol as follows:
Map ( name : string -> hands : Map ( side : string -> owner eq ^ ))In this construct, the "^"-symbol is refering to the whole record in the map, not only the name string as before. It thus has the same meaning as in the previous section. But although this is an improvement, it still is rather cumbersome, especially if one bears in mind that component occur often. To solve this, we introduce "CompRecord" to indicate that a record has a owner pointer (accesible through the "^"-symbol) to the surrounding record. For set, relations, list, maps and functions containing components, the name is simply extended with "OfComp". With this the above construct can be written like:
Map ( name : string -> hands : SetOfComp ( side : string ))Now, lets asume that besides hands also the feet are represented. The expression could be extended into:
Map ( name : string -> hands : SetOfComp ( side : string ), feet : SetOfComp ( side : string ))There is a problem with the above construct, when one want to take the union of hands and feets. These are both sets of records (unary relations) with as a hidden value the value of the record. In case both the hands and feets would contain two components with "left" and "right" for the side, the union of these would result in a set of components with two components. This might not have been the intention. To prevent this, one would have to add another element to the record, indicating, if the component belongs to the hands or the feets. To avoid this, we introduce the "Comp" prefix for sets, relations, list, maps and functions inside records, to indicate that it contains components with a unique identifier for the field.
Remark 2. In many kinds of class diagrams the link types aggregration and composition are used. Although the concept of composition is related to the component concept introduced here, it is not possible to say that they are always exactly the same. Much depends on the definition of the semantical model of the particular kind of class diagrams. The first purpose of the component concept introduced here, is to allow us to identify "values" based on the context in which they occur. (Speaking in terms of the above example: The arms of different people can be identified as different.) In most kinds of class diagrams all entities have an unique identification, independently, of whether links are marked with aggregration or composition. In that case the concepts do not match. Often the link type composition means that the "child object" cannot exist without the "parent object".
df id = tWhere t is any type expression, in which the identifier id is also defined. This allows the definition of recursive types. In the specification language id itself is not a name of a type, it should be considered as a short hand of the type expression t. For naming types the named types were introduced.
For local definitions of types, the following where-expression is introduced:
t where ( id1 = t1, ..., idn = tn )In this t, t1 to tn stands for a type expression in which the identifiers id1 to idn can be used.