Die VDM-Basistypen Domain Specification Language (DSL) Die Domain-Gleichungen

Die Implementationsbeschreibungen

Für jeden definierten ADT müssen Sie eine Beschreibung geben, wie dieser realisiert werden soll und welche Operationen  sie benötigen -- dazu dienen die Implementationsbeschreibungen.

Struktur Eine Implementationsbeschreibung hat die folgende Struktur:

Domain = Implementation + Enrichment + ...
*[2ex]

Die erste Angabe Implementation ist der Name der gewünschten Implementation  des zugrundeliegenden ADT, möglicherweise gefolgt von einer Liste mit Parametern, die bestimmte Aspekte der Repräsentation noch ,,adjustieren`` können. Für jeden ADT gibt es einen individuellen Satz von Implementationen. Zur Information über die vorhandenen Implementationen können Sie auch das Online-Hilfesystem   vdminfo (siehe dazu Kapitel 8Kapitel 8) heranziehen.

Mit der Angabe der Implementation definieren Sie nur die grundlegenden Datenstrukturen mit den nötigen Datenelementen zu ihrer Verwaltung sowie interne Kontrollfunktionen, die von den Operationen benötigt werden, nicht aber die Operationen selbst; aus Gründen der Speicherplatzersparnis sollten Sie nämlich nur diejenigen Operationen in Ihr Programm einbinden, die Sie auch wirklich benutzen!

Daher folgt nun die Angabe der benötigten Enrichments Operationen , den sogenannten Enrichments , also ,,Anreicherungen`` des ADT. Sie brauchen nur den generischen Namen  angeben, also den Grundnamen ohne Spezialisierung für den spezifischen, von Ihnen definierten Domain-Namen (Sie wissen doch: der Quelltext der Operation wird vom VDM-Compiler auf den von Ihnen definierten Domain zugeschnitten, was die Parameter und den Funktionswert betrifft; dabei wird der generische Name der Operation durch Erweiterung mit dem Domain-Namen spezialisiert -- siehe dazu Abschnitt 3.2.13.2.1). Auch Enrichments sind zum Teil mit Parametern noch spezifisch steuerbar.

Zusätzliche Enrichments Sie können übrigens für einen ADT mehrere Implementationsbeschreibungen angeben -- eine häufige Anwendung dafür ist die Erweiterung eines allgemein verwendbaren ADT um einige Enrichments, die Sie nur in einer Applikation benötigen; die Änderung der allgemeinen Beschreibung des ADT ist nicht nötig, Sie ,,erweitern`` sie einfach um eine weitere Beschreibung. Da sie die Implementation nicht ändern dürfen (sonst beklagt sich der VDM-Compiler über eine mehrdeutige Implementationsbeschreibung), können Sie sie auch weglassen; Ihre Beschreibung beginnt dann mit einem Plus-Zeichen. Beispiel: Sie möchten den Datentyp Str um die Operationen puts und fwrite erweitern. Sie schreiben dann

Str=+ puts + fwrite
*[1.5ex]

Parameter Parameter  müssen Sie innerhalb von runden Klammern angeben. Die meisten Parameter sind optional und haben Default-Werte; daher brauchen Sie sie für eine ,,Standard-Konfiguration`` nicht anzugeben. Welche Parameter angegeben werden müssen, hängt natürlich von der gewählten Implementation ab und ist daher im Anhang C Anhang C angegeben. Zur Definition von Parametern gibt es fünf Möglichkeiten:

  1. PARAMETER = " String "
    *[0.5ex] Dieser String kann beliebige Zeichen außer Anführungsstrichen (") und Zeilenwechseln enthalten. Welche Strings sinnvoll sind, hängt natürlich davon ab, um welchen Parameter es sich handelt.
  2. PARAMETER = 0
    *[0.5ex] Damit wird der Parameter ,,undefiniert``, der VDM-Compiler ignoriert ihn; so können Default-Werte ungültig gemacht oder globale Definitionen per Kommandozeilen-Option des VDM-Compilers für eine spezielle Implementation ignoriert werden.
  3. PARAMETER = Zahl
    *[0.5ex] Diese Zahl ist eine nicht-negative, ganze Zahl. Beachten Sie: Wollen Sie den Wert Null zuweisen, geben Sie bitte <<00>> ein, eine einfache <<0>> sorgt ja dafür, daß der Parameter undefiniert ist!
  4. PARAMETER
    *[0.5ex] Das ist eine Kurzform für die Zuweisung PARAMETER = 1.
  5. PARAMETER = Name
    *[0.5ex] Ein String, der nur aus Buchstaben und Ziffern besteht, heißt auch ,,Name``. Solche Strings können auch ohne Anführungsstriche zugewiesen werden.

Der VDM-Compiler prüft, ob ein angegebener Parameter zugelassen ist; wenn nicht, erhalten Sie eine Fehlermeldung.

Beispiel: Zum Abschluß noch ein Beispiel für eine komplette DSL-Spezifikation. Wenn Sie mit den ADT noch nicht vertraut sind, werden Sie es vielleicht nicht verstehen; es soll auch nur dazu dienen, einen Eindruck vom Aussehen einer solchen Spezifikation zu bekommen.

  figure1190
Abbildung: Beispiel für eine DSL-Spezifikation

Die VDM-Basistypen Domain Specification Language (DSL) Die Domain-Gleichungen

VDM Class Library