Sets Die VDM-Basistypen Generelle Operationen

Elementare Datentypen

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.

Die vordefinierten Zahlentypen

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.

Der Datentyp Char

 

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.

Der Datentyp Nat1

 

In der Zahlentheorie, einem Zweig der Mathematik, werden die verschiedenen Zahlenarten in einige Mengen unterteilt. Die anschaulichste ist die Menge tex2html_wrap_inline7017 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.

Der Datentyp Nat0

 

Die nächstgrößere zahlentheoretische Menge entsteht durch die Hinzunahme der Null: tex2html_wrap_inline7021 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.

Der Datentyp Intg

 

Die ganzen Zahlen bilden die nächstgrößere Zahlenmenge tex2html_wrap_inline7024 . 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.

Der logische Datentyp Bool

 

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.

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

Der vordefinierte Datentyp Str

  

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.

Selbstdefinierte elementare Datentypen

 

Unterbereiche von Zahlenmengen

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.

Token

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
* tex2html_wrap_inline6814
In der Applikation:
* Token PLUS,MINUS,MULT,DIV;
* PLUS = new_token();
* MINUS = new_token();
* MULT = new_token();
* DIV = new_token();
* tex2html_wrap_inline6814
Token input_operator (void)
* {
* Einlesen des Operatorsymbols und Abspeichern in op
* switch (op) {
* '+': return PLUS;
* '-': return MINUS;
* ' tex2html_wrap_inline7065 ': return MULT;
* ' tex2html_wrap_inline7067 ': 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.

Selbstdefinierte C-Strukturen

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.

Sets Die VDM-Basistypen Generelle Operationen

VDM Class Library