The Art of Programming
A specification language: Static aspects

By Frans Faase

Introduction

On this page the static aspects of a powerful specification language are presented. Because this specification language is based on simple mathematics, it does have clearly defined semantics. (That something has "simple" semantics, does not mean that it can represtent very complex structure, or that it does not have "unexpected" or counter-intuitive aspects.) The language is basically a type definition language. Each type represents a (possibly infinite) set of values.

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.

Typographic conventions

The use of the bold type face is a purely typographic matter in order to improve readability. The italic type face is used for representing place holders for certain expressions as explained in the running text. Keywords and identifiers are case sensitive.

Basic type constructors

Below the basic type constructors are given.

Elementairy types

The elementary types are:

Void. Always equal to the value void.
Bool. Either true or false.
Num. All the whole numbers.
NatNum. All positive numbers including zero.
PosNum. All positive numbers excluding zero.
NumRange(f, t). All numbers from f to t, f and t included.
RatNum. All rational numbers, which written as a quotient of a Num and a natnum.
RealNum. All real numbers.
Char. All characters.
String. All strings.

Option types

Option types are defined using a base type, using the following construct:

Option(t)

The resulting type is defined by the collection of all values of the bases type added with the value void.

Enumeration types

Enumeration types are simply defined by an enumeration of identifiers using the following construct:

Enum(id₁,..,id_n)

Set and list types

Set types are defined by using a base type. Besides the traditional set we also introduced a ordered set. The ordered set gives a complete ordering over all the elements of the set. The list type is also defined using a base type. In the list type values can occur as often as possible. The ordered set type can also be considered as a list type with an additional constraint. The following constructs are used to define these types:

Set(t)
OrderedSet(t)
List(t)

Record type

Record types are defined by giving a set of identifier type pairs. The construct for defining a record type is:

Record(id₁:t₁, ..., id_n:t_n)

The order in which the pairs occur in the definition does not matter, with respect to the resulting type.

Function and map types

Function types are defined by giving the type of the domain and the codomain. Map types are partial functions. They can also be viewed as a set type, with an additional value added to each value. Just like there are ordered set types, there are also ordered function and map types. All these are defined with the following constructs:

Func(t_d, t_c)
Map(t_d, t_c)
OrderedFunc(t_d, t_c)
OrderedMap(t_d, t_c)

Because for practical reasons the domain and codomain types are often record types, the following short hand constructs are introduced:

Func(t_d -> id_c1:t_c1, ..., id_cn:t_cn)
Func(id_d1:t_d1, ..., id_dn:t_dn -> t_c)
Func(id_d1:t_d1, ..., id_dn:t_dn -> id_c1:t_c1, ..., id_cn:t_cn)
Map(t_d -> id_c1:t_c1, ..., id_cn:t_cn)
Map(id_d1:t_d1, ..., id_dn:t_dn -> t_c)
Map(id_d1:t_d1, ..., id_dn:t_dn -> id_c1:t_c1, ..., id_cn:t_cn)
OrderedFunc(t_d -> id_c1:t_c1, ..., id_cn:t_cn)
OrderedFunc(id_d1:t_d1, ..., id_dn:t_dn -> t_c)
OrderedFunc(id_d1:t_d1, ..., id_dn:t_dn -> id_c1:t_c1, ..., id_cn:t_cn)
OrderedMap(t_d -> id_c1:t_c1, ..., id_cn:t_cn)
OrderedMap(id_d1:t_d1, ..., id_dn:t_dn -> t_c)
OrderedMap(id_d1:t_d1, ..., id_dn:t_dn -> id_c1:t_c1, ..., id_cn:t_cn)

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(id₁:t₁, ..., id_n:t_n)

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 types

Named types simply attach a name to an existing type. We also introduce a short hand for the named record type, which is the most common use. The following constructs are used:

Named(id,t)
NamedRecord(id, id₁:t₁, ..., id_n:t_n)

Unioning of types

Because, each type expression represents a (possibly infinite) set of values, it is also possible to define types that are the union of two or more other types. The following construction is used for this:

Union(t₁, ..., t_n)

Using record fields as types

With the above mentioned constructs a large range of types can be defined. However, it is not possible to express certain restrictions. If for example one want to define a type which consists of a set of numbers and a certain number from this set, this is not possible. The best one can do is the following:

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 occure 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.

Components

A component is a part whoes identity is unseparatable from the thing it belongs to. For example, the left hand of a person, cannot be simply identified as the "left" hand, as there are many "left" hands, it is the "left" hand of a certain person. Part of its identity is determined by the thing it belongs to. This especially becomes clear, if one want to represent which hand is holding which hand when a group of people are standing in a circle. This is modelled as a relation over the union of all the hand of the people standing in the circle.

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 1.

Comp

Value

Remark 2.

aggregration

composition

aggregration

composition

Defining types

Although a large number of types can be specified with the basic type constructors, additional mechanism are needed to make it into a more powerful specification language.

Simple type definitions

To name a certain type expression, the following construct is introduced:

df id = t

Where 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 ( id₁ = t₁, 
...,
id_n = t_n )

In this t, t₁ to t_n stands for a type expression in which the identifiers id₁ to id_n can be used.

Parameterized types

My life as a hacker

The Art of Programming A specification language: Static aspects