?)
?)
?)
Sets
Die VDM-Basistypen
Generelle Operationen
Die elementaren Datentypen entsprechen den elementaren Zahlentypen in C. Die VDM-Datentypen sind jedoch (etwas abstrakter) an die mathematischen Bezeichnungen angelehnt. Auch in VDM gibt es die durch Zahlen repräsentierten Datentypen wie das Zeichen und den logischen Wahrheitswert (Bool). Wie sie durch C-Datentypen repräsentiert werden und welche speziellen Anwendungen die verschiedenen Implementationen bieten, erfahren Sie in diesem Abschnitt.
Normalerweise brauchen Sie sich um die Implementation der vordefinierten Datentypen nicht zu kümmern, da VDM sie in jede Applikation einbindet. Sie können daraus aber eigene Datentypen ableiten; wie, das erfahren Sie hier ebenfalls.
Vorweg sei gesagt, daß Sie mit den Zahlentypen wie gewohnt rechnen können -- alle mathematischen Operationen können mit den VDM-Zahlentypen umgehen und auch die logischen Funktionen haben die erwarteten Resultate (bei Bedingungen in den verschiedenen Schleifenstrukturen usw.).
Der Vollständigkeit halber gibt es drei Vergleichsoperationen für die Zahlentypen:
?) ?) ?)
Diese Operationen stehen zum Teil auch für die strukturierten Datentypen zur Verfügung und basieren dann auf dem Vergleich der Elemente mit Hilfe der entsprechenden Operationen für den Elementtyp.
VDM bietet für den Umgang mit Zeichen -- wie auch C -- einen speziellen, recht kleinen Zahlentyp an, der gerade für den Zeichensatz des Computers ausreicht, also 256 Zeichen umfaßt. Char steht in der Implementation ,,unsigned`` zur Verfügung und wird mit dem Datentyp ,,unsigned char`` dargestellt. Natürlich können Sie auch Zahlen in einem Char abspeichern, wenn Sie Speicherplatz sparen möchten; aus Gründen der Verständlichkeit sollten Sie aber davon Abstand nehmen und Zahlen tatsächlich durch Zahlentypen repräsentieren.
In der Zahlentheorie, einem Zweig der Mathematik, werden die verschiedenen
Zahlenarten in einige Mengen unterteilt. Die anschaulichste ist die Menge
der natürlichen Zahlen (ohne die Null), denn sie repräsentiert
alles, was abzählbar ist -- die Objekte, die Null-mal da sind, können ja
nicht gezählt werden.
VDM stellt diese Menge als Datentyp bereit, er heißt Nat1. Sie können ihn mit verschiedenen Implementationen darstellen, am sinnvollsten jedoch ist die Implementation ,,unsigned`` , die den größtmöglichen Wertebereich für Nat1 zur Verfügung stellt -- leider kann die theoretisch unendliche Menge der natürlichen Zahlen per Computer nicht abgebildet werden. Standardmäßig wird Nat1 durch den C-Datentyp ,,unsigned long`` repräsentiert.
Die nächstgrößere zahlentheoretische Menge entsteht durch die Hinzunahme der
Null: 
enthält also alle nicht-negativen ganzen Zahlen.
In VDM wird diese Menge durch den Datentyp Nat0 repräsentiert, der wie Nat1 intern durch ,,unsigned long``-Werte dargestellt wird.
Die ganzen Zahlen bilden die nächstgrößere Zahlenmenge 
. Hinzu kommen
also negative Zahlen.
VDM stellt dafür den Datentyp Intg zur Verfügung. Die Implementation ,,unsigned`` ist dafür natürlich ungeeignet; stattdessen wird die Implementation ,,scalar`` verwendet, die Intg mit dem Datentyp ,,signed long`` darstellt.
Prädikate und Vergleichsoperationen liefern entweder ,,wahr`` oder ,,falsch``. In C werden alle ,,falschen`` Resultate durch die Zahl Null dargestellt, während ein beliebiger Wert ungleich Null ,,wahr`` bedeutet.
VDM bietet Ihnen für logische Daten den Datentyp Bool an, der sich genauso verhält wie die entsprechenden Hilfskonstruktionen in C und demzufolge auch mit diesen kompatibel ist. Häufig wird in C folgendes vereinbart:
typedef BOOL unsigned char;
*
#define TRUE (1 == 1)
*
#define FALSE (0 == 1)
*[1.5ex]
Der VDM-Datentyp Bool sollte an die Stelle von ,,BOOL`` treten; TRUE und FALSE und auch die in C vorhandenen logischen Operatoren können Sie aber auch weiterhin so verwenden. VDM stellt aber auch entsprechende Operationen zur Verfügung, die z.B. in mit Funktionalen erzeugten Funktionen mit einem Bool-Resultat eingesetzt werden können; eine Anwendung dafür finden Sie bei den Sets im Abschnitt 5.4.
`` erreicht werden.Bool-Werte werden durch den kleinstmöglichen Datentyp (,,unsigned char``) in der Implementation ,,bool`` dargestellt, der speziell an logische Werte angepaßt ist (z.B. was die Ausgabe von Bool-Werten betrifft).
Ein strukturierter Datentyp ist im VDM-System immer definiert: Str, die Klasse der Zeichenketten. Sie sind als Tuples implementiert und nutzen einige Besonderheiten der Tuple-Implementation ,,array`` aus; da sie sich von gewöhnlichen C-Strings unterscheiden, werden sie zur Abgrenzung als VDM-Strings bezeichnet. Es stehen Operationen zur Verfügung, um bequem mit diesen VDM-Strings zu arbeiten; außerdem existieren Schnittstellen zu den normalen C-Strings.
Im Abschnitt 5.5 5.5 über Tuples wird näher auf VDM-Strings und ihre Besonderheiten eingegangen.
Wenn Sie nur einen bestimmten Unterbereich einer Zahlenmenge benötigen, können Sie ihn selbst definieren. Sie geben ihm einen Namen, tragen in der Domain-Gleichung den Datentyp ,,ELEMENTARY`` ein und wählen eine der Implementationen ,,unsigned`` (bei einem positiven Unterbereich) oder ,,scalar`` (wenn auch negative Werte im Unterbereich enthalten sind). Zusätzlich setzen Sie die Implementationsparameter ,,LB`` und ,,UB``, die Unter- und die Obergrenze des gewünschten Bereichs. Der VDM-Compiler wählt automatisch den kleinstmöglichen Datentyp aus, mit dem der Unterbereich darstellbar ist.
Beispiel: Sie benötigen den Zahlenbereich von eins bis einunddreißig, um Monatslängen zu verwalten.
DOMAINS
*
Days = ELEMENTARY
*
IMPLEMENTATIONS
*
Days = unsigned(LB=1,UB=31)
*[1ex]
Der Datentyp ,,Days`` wird dann mit Hilfe von ,,unsigned char``-Variablen repräsentiert.
Ein interessanter Sonderfall ist das Token -- es gibt keine Definition, wie es repräsentiert wird, es ist nur sichergestellt, daß zwei Token auf Gleichheit getestet werden können.
Geeignete Implementationen für Token sind ,,unsigned`` und ,,scalar``, denn sie enthalten eine Operation new, mit der ein neuer, vorher noch nie verwendeter Wert erzeugt wird.
Damit können Sie einen Aufzählungstyp definieren, wie er in Pascal existiert: Sie erzeugen in der Applikation die Anzahl benötigter Token in entsprechenden Variablennamen und ordnen auf unterster Ebene der Applikation den darzustellenden Zuständen einen der Token-Namen zu. In den höheren Verarbeitungsfunktionen können Sie dann die Token-Namen statt nichtssagender Zahlencodes benutzen.
Beispiel: Das klingt sehr abstrakt; am Beispiel eines Tischrechners, der die vier Grundrechenarten beherrscht, soll dies verdeutlicht werden. Die Operatoren sollen im Programm durch die Namen PLUS, MINUS, MULT, DIV angesprochen werden. Die Eingabefunktion wertet die eingegebenen Operatoren aus und ordnet ihnen das entsprechende Token zu.
DOMAINS
*
Token = ELEMENTARY
*
IMPLEMENTATIONS
*
Token = unsigned + new
*
In der Applikation:
*
Token PLUS,MINUS,MULT,DIV;
*
PLUS = new_token();
*
MINUS = new_token();
*
MULT = new_token();
*
DIV = new_token();
*
Token input_operator (void)
*
{
*
Einlesen des Operatorsymbols und Abspeichern in op
*
switch (op) {
*
'+': return PLUS;
*
'-': return MINUS;
*
' 
': return MULT;
*
' 
': return DIV;
*
}
*
}
*[3ex]
Heap Eine andere Anwendung für Token ist die Modellierung der Heap-Speicherverwaltung mit einer Map, die ebenso schnell ist wie die ,,direkte`` Verwaltung in C (mit malloc und free). Sie bietet allerdings die Möglichkeit, durch Austausch der Map-Implementation wesentlich mächtigere Operationen und mehr Sicherheit beim Umgang mit Pointern zu erreichen, wenn die Performance-Anforderungen das erlauben. Im Abschnitt 5.6 über Maps erfahren Sie mehr darüber. Da die Token in diesem Fall Adressen von dynamischen Objekten enthalten, sollten Sie die Implementation ,,ptr`` wählen. Den Datentyp, auf den die Pointer weisen, legen Sie mit dem Implementationsparameter ,,ELEM`` fest.
Wenn Sie eine bestehende Applikation mit VDM unterstützen möchten, werden Sie bereits einen Satz an Datenstrukturen mit den Mitteln von C definiert haben. Um diese auch von VDM-Operationen verarbeiten lassen zu können, müssen Sie sie ,,importieren``. Manchmal ist das auch erforderlich, wenn Sie Manipulationen durchführen wollen, für die VDM keine Unterstützung bietet; die Datei-Operationen von VDM sind beispielsweise nur bedingt verwendbar. Hier brauchen Sie eine Schnittstelle, um VDM-Daten an C-Funktionen zu übergeben, die diese Manipulationen durchführen.
Eine Möglichkeit ist die Definition eines elementaren Datentyps in VDM, der die gewünschte Struktur aufnehmen kann, für alle VDM-Operationen aber unteilbar ist. Dies erreichen Sie mit Hilfe der Implementation ,,unsigned`` und dem Parameter ,,CSTRUCT``, der die Typdefinition enthält. Ein Beispiel: Sie möchten eine sequentielle Datei von Datensätzen bearbeiten, die Sie komplett in den Speicher laden und dort in einer Baumstruktur halten, um eine Sortierung der Datensätze zu ermöglichen. Diese Baumstruktur erzeugen Sie mit den VDM-Basistypen Tree und Optional, aber alle Dateioperationen führen Sie mit normalen C-Strukturen aus. Eine DSL-Spezifikation dafür sieht so aus:
#typedef struct { ...} RECORD;
*[1ex]
DOMAINS
*
Btree=[ Node ] ...
*
Node :: s_lt : Btrees_data : Datas_rt : Btree
*
Data = ELEMENTARY
[0.5ex]
IMPLEMENTATIONS
*
Btree = ptelem + ...
*
Node = ptstruct + ...
*
Data = unsigned(CSTRUCT=
"RECORD")
*[1.5ex]
Der Btree enthält außer seinen Verwaltungsinformationen Datenknoten vom Typ Node. Die in einem Node existierenden Daten vom Typ Data sind für die VDM-Operationen unteilbar. Seine interne Struktur ist daher uninteressant, wichtig ist nur die Größe eines Objekts. Für C-Funktionen aber ist ein Data-Objekt eine Struktur und kann mit den üblichen Methoden manipuliert werden.
VDM Class Library