3.4.3 Language Constructs for Abstract Types

The language includes the conventional types Boolean and Integer.

The notation [first .. last] stands for the subrange first, first+1, ... , last. The type byte is the subrange [0.. 255].

A sequence is an indexed collection of variables, called the elements of the sequence. The elements all have the same type. The index type of a sequence is a zero-based subrange. S[i] denotes the element of the sequence S that corresponds to the value i of the index type. The number of elements in a sequence S is denoted S.length. Therefore, the index type of a sequence S is [0 .. S.length-1].

A sequence type can be open (index type not specified) or closed (index type specified):

  • type DSNameSeq = sequence of DSName

  • type Digest = sequence [0 .. 15] of byte

A fixed-length sequence can be constructed by using the following notation:

  • [first element, second element, ... , last element]

Therefore:

  • s := []

sets a sequence-valued variable s to the empty sequence. A sequence of bytes can be written in the more compact string form shown in the following example:

  • s := "\x55\x06\x02"

A unicodestring is a sequence of 16-bit Unicode characters.

If S is a sequence, and ji, then S[i .. j] is a new sequence of length j - i + 1, whose first element has value S[i], second element has value S[i + 1], ... , and final element has value S[j]. The index set of the new sequence is [0 .. j - i]. If j < i then S[i .. j] is the empty sequence.

A tuple is a set of name-value pairs: [name1: value1, name2: value2, ... , namen: valuen] where namek is an identifier and valuek is the value bound to that identifier. Tuple types are defined as in the following example:

  • type DSName = [dn: DN, guid: GUID, sid: SID]

This example defines DSName as a tuple type with a DN-valued field dn, a GUID-valued field guid, and a SID-valued field sid.

A tuple constructor is written as in this example:

  • dsName: DSName

  • dsName := [dn: "cn=Peter Houston,ou=NTDEV,dc=microsoft,dc=com"]

Fields that are unspecified in a tuple constructor are assigned null values in the resulting tuple.

Access to the named fields of a tuple uses dot notation. Continuing the example:

  • d: DN; g: GUID; s: SID

  • d := dsName.dn

  • g := dsName.guid

  • s := dsName.sid

The preceding assignments set the variable d to "cn=Peter Houston,ou=NTDEV,dc=microsoft,dc=com", and variables g and s to null values.

A tuple deconstructor can be written anywhere a tuple-valued variable can occur. The preceding assignments are equivalent to the following:

  • [dn: d, guid: g, sid: s] := dsName;

The language includes sets. If S is a set, number(S) is the cardinality of the set S.

A fixed-size set can be constructed using the notation:

  • {one element, another element, ... , yet another element}

Therefore:

  • S := {}

sets a set-valued variable S to the empty set.

If S is a set, the predicate x in S is true if x is a member of S. Therefore, the value of the expression:

  • 13 in {1, 2, 3, 5, 7, 11}

is false.

If A and B are sets, A + B is the set union of A and B, A ∩ B is the set intersection of A and B, and A - B is the set difference of A and B.

The specification uses [KNUTH1] section 2.3.4.2 as a reference for the graph-related terms directed graph, oriented tree, vertex, arc, initial vertex, and final vertex. In pseudocode, graphs are described in terms of their vertex and arc sets, and individual arcs are represented as tuples.

The language supports coercion between abstract and concrete types when the correspondence between the two is clear. For example, if stringSet is a set of unicodestring and stringArrayPtr is a pointer to an array of pointers to null-terminated Unicode strings, the assignment:

  • stringSet := stringArrayPtr^

populates the abstract set of strings by copying from the concrete array of strings.