Die Domain-Gleichungen

Für jeden benötigten ADT muß dessen interne Struktur mit Hilfe der VDM-Basistypen, die ja Typgeneratoren darstellen, angegeben werden -- dazu dienen die Domain-Gleichungen.

Nomenklatur Die Nomenklatur empfiehlt für Namen von Domains normale C-Bezeichner mit einigen Einschränkungen: der erste Buchstabe muß groß sein, alle weiteren klein, der Unterstrich darf ebenfalls vorkommen. Die Beispielsnamen wurden entsprechend dieser Regel möglichst ,,sprechend`` gewählt.

Hier sind nun die Formate der Domain-Gleichungen für die VDM-Basistypen, Beispielen. Die Bedeutung der ADT wird dabei kurz beschrieben. Die ADT sind Typgeneratoren , weil die Datentypen ihrer Elemente frei gewählt werden können.

Set Der Set ist die Klasse von Mengen (im mathematischen Sinn) von Elementen.

Map Die Map ist die Klasse von endlichen Mengen von Paaren von Elementen (partielle, funktionale Zuordnung).

Tree Der Tree ist die Klasse von endlichen geordneten Sammlungen einzeln benannter Komponenten eventuell unterschiedlichen Typs.

Selektornamen Alle Komponenten müssen benannt sein. In der VDM-Spezifikation ist das nicht gefordert; Sie müssen dies jetzt nachholen. Ein Komponentenname (Selektorname) beginnt immer mit der Zeichenfolge ,,s_``, darauf folgt zunächst ein Kleinbuchstabe, dann können noch weitere Kleinbuchstaben, Ziffern oder Unterstriche folgen.

Union Die Union ist die Klasse von Objekten, die mehrere Datentypen haben können; zu jeder Zeit enthält ein Union-Objekt genau ein Objekt mit einem der möglichen Datentypen.

Bei Unions ist es erlaubt, die Elemente anonym zu lassen; der VDM-Compiler generiert in diesem Fall Namen, indem er vor den (in Kleinbuchstaben umgewandelten) Elementnamen die Zeichen ,,s_`` stellt. Das ist natürlich nur möglich, wenn nicht eine andere anonyme Union die gleichen Datentypen verwendet, da sonst doppelte Bezeichner auftreten!

Optional Das Optional ist eine Klasse von Objekten, die zu einem bestimmten Zeitpunkt entweder ein Objekt des Elementtyps oder den speziellen Wertnil enthalten.

Elementare Elementare Datentypen (Elementary) gibt es in VDM auch: es sind Zeichen, Zahlen (mit verschiedenen Wertebereichen) und logische Wahrheitswerte. Außerdem gibt es einen vordefinierten Datentyp ,,String``, der als Tuple von Zeichen vereinbart ist; er ist zwar nicht elementar, steht aber immer zur Verfügung.

Nat1 Natürliche Zahlen ab 1

Nat0 Natürliche Zahlen ab 0

Intg Ganze Zahlen

Bool true und false

Char ASCII-Zeichen

Str Zeichenketten

Token Ein Token ist ein Typ, für den nur Konstruktoren und Tests auf Gleichheit / Ungleichheit existieren. Eine Repräsentation ist nicht definiert; Sie können damit z.B. Pointer oder Unterbereichstypen definieren (Anwendungen finden Sie im Abschnitt 5.3.4).

Es gibt eine Restriktion bezüglich der Verschachtelung von Domains innerhalb einer Domain-Gleichung: Komponenten von zusammengesetzten Domains dürfen nicht ebenfalls zusammengesetzt sein. Dies müssen Sie bei der Umsetzung Ihrer VDM-Spezifikation beachten; dort ist die Verschachtelung von ADT ja beliebig möglich. Die Zerlegung sollten Sie trotzdem erst während der Erstellung der DSL-Spezifikation vornehmen, da die Struktur des von Ihnen geschaffenen ADT klarer ist, wenn sie ,,komplett`` in einer Domain-Gleichung vorliegt! Warum müssen Verschachtelungen zerlegt werden ? Weil Sie für jeden beteiligten VDM-Basistyp festlegen müssen, wie er implementiert werden soll -- dafür muß aber jeder VDM-Basistyp auch einen Namen haben!

	Nat1			Natürliche Zahlen ab 1
	Nat0			Natürliche Zahlen ab 0
	Intg			Ganze Zahlen
	Bool			true und false
	Char			ASCII-Zeichen
	Str			Zeichenketten