Programmentwicklung mit VDM Vienna Development Method Struktur einer Modellspezifikation

Das VDM-System unter UNIX

 

In diesem Abschnitt werden zunächst nur die Elemente und die Struktur des VDM-Systems an der FH Wedel behandelt und die zum Verständnis des Systems nötigen technischen Grundlagen. Wie Sie praktisch damit arbeiten und Programme entwickeln, ist das Thema des Abschnitts 3.3.

Die Basistypen in der VDM-Bibliothek

 

Die VDM-Basistypen  -- also die abstrakten Datentypen Set , Tuple , Map , Tree , Union  und Optional  -- wurden mit Hilfe dynamischer Datenstrukturen  in C programmiert, ebenso die zu diesen ADT vorhandenen Operationen . Dadurch wird die Größe eines Objekts nur durch den verfügbaren Hauptspeicher (in einer Umgebung mit virtueller Speicherverwaltung  sogar nur durch den Festplattenspeicher) beschränkt.

Mehrere Implementationen Der Clou: Zu jedem VDM-Basistyp gibt es mehrere Implementationen , die sich im Hinblick auf die benutzte Speicherallokationsstrategie  und die zugrundeliegenden Datenstrukturen unterscheiden, woraus sich unterschiedliche Anforderungen an Laufzeit und Speicherplatz ergeben. Das grundsätzliche Verhalten einer Implementation können Sie meist noch durch bestimmte Parameter im Detail steuern. Eine Anpassung an die besonderen Anforderungen der Applikation ist damit möglich. Ein Beispiel: wenn Sie bereits wissen, mit wievielen Objekten eines ADT Ihr Programm maximal arbeitet, kann die Verwaltung des ADT daran angepaßt werden.

Der für einen VDM-Basistyp definierte Satz an Operationen ist grundsätzlich in allen Implementationen vorhanden, Sie können eine Implementation also jederzeit leicht austauschen, ohne in Ihrem Programm Änderungen vornehmen zu müssen; das ist sehr nützlich, um die beste Kombination aus Performance  und geringem Speicherbedarf zu ermitteln. Eine Übersicht über die aktuellen Implementationen finden Sie im Anhang CAnhang C.

Operationen Die Implementation der Operationen muß berücksichtigen, daß jeder VDM-Basistyp ein Typgenerator ist, also nicht immer die gleichen Elementtypen hat -- es muß also eine Möglichkeit vorgesehen sein, die Parametertypen der Operationen erst bei der Einbindung in die Applikation festzulegen !

Ein weiteres Problem: Sie dürfen jeden VDM-Basistyp mehrfach für die Konstruktion eigener ADT verwenden, z.B. den Set für je eine Menge Intset von Zahlen und eine Menge Boolset von Wahrheitswerten. Jede Mengen-Operation (z.B. mk_empty, die Erzeugung der leeren Menge) muß dann zweimal vorhanden sein, jeweils mit unterschiedlichen Parametern und Resultaten -- mit der Konsequenz, daß der Name mk_empty allein nicht ausreicht, um die richtige Operation auszuwählen.

Die zunächst vielleicht naheliegende Lösung einer bereits compilierten Modulbibliothek scheidet aus diesen Gründen leider aus, da C keine Mittel zur Umgehung dieser Probleme bei compilierten Modulen anbietet; stattdessen muß der Quellcode der Funktionen entsprechend geändert werden.

Aus diesem Grunde wurde die VDM-Bibliothek  als Quellcode-Bibliothek  konzipiert. In ihr ist der Quellcode aller Operationen, die für den verschiedenen VDM-Basistypen definiert sind, in einer effizienten Struktur abgelegt, die das schnelle Auffinden unterstützt. Sie wählen die benötigten Operationen aus - das VDM-System generiert daraus ein passendes Quellmodul , das Sie zusammen mit der Applikation compilieren.

Die Lösung der beiden Probleme ist jetzt einfach:

1. Die Datentypen der Parameter und des Resultats werden aus der Spezifikation des ADT ermittelt und an der entsprechenden Stelle im Quellcode eingetragen.
2. Für jeden von Ihnen spezifizierten ADT wird auf diese Weise ein eigener Satz Operationen generiert, die natürlich auch für jeden ADT einen Operationen werden daher erweitert, und zwar um den Namen des ADT -- das ist eindeutig, da alle ADT unterschiedliche Namen haben (Ausnahme: ein ADT, der aus Trees oder Unions besteht, braucht für den Zugriff auf die Komponenten mehrere Selektions-Funktionen, deren generischer Name s ist. VDM fordert, daß jede Komponente einen einzigartigen, mit s_ beginnenden Namen haben muß, der dann identisch mit dem erweiterten Namen der Selektions-Funktion ist).

  Erweiterung der Operationsnamen Die Namenserweiterung muß noch etwas genauer beschrieben werden: dem generischen Namen wird zunächst ein Unterstrich nachgestellt, dann folgt in der Regel der ADT-Name, wobei der Großbuchstabe am Anfang in eine Kleinbuchstaben konvertiert wird. Beispiele: Für die oben erwähnten Mengen Intset und Boolset heißen die Konstruktoren einer leeren Menge mk_empty_intset und mk_empty_boolset. Da ein Tree mehrere Komponenten enthält und ein Union-Objekt seinen Datentyp ändern kann, werden die komponentenbezogenen Operationen von Tree und Union mit dem jeweiligen Komponentennamen erweitert, eventuell auch zusätzlich mit dem Namen des ADT. Die beiden führenden Zeichen ,,s_`` eines Komponentennamens werden dabei weggelassen! Beispiel:

Uni = Intg | Str
* Die Konstruktoren heißen mk_intg_uni und mk_str_uni
*[0.5ex] Tree :: s_first : Intgs_last : Str
* Die Selektoren heißen s_first und s_last
*

Die Domain Specification Language

Ihre Modellspezifikation  ist fertig, aber nicht ,,maschinenlesbar``. Sie wissen, welche VDM-Basistypen Sie benötigen, Sie haben Ihre semantischen Funktionen  konstruktiv spezifiziert und wissen auch, welche grundlegenden Operationen der VDM-Basistypen Sie benötigen. Wie geht es weiter ?

Sie ,,übersetzen`` Ihre Spezifikation in eine für das VDM-System verständliche Sprache, die Domain Specification Language (abgekürzt DSL ). Keine Panik, das ist einfach: der erste Teil einer DSL-Spezifikation enthält die Domain-Gleichungen Domain-Gleichungen , die Sie bereits erstellt haben und die Sie nur geringfügig zu verändern brauchen. Der zweite Teil enthält für jeden angegebenen ADT die gewünschte Implementation Implementation (Sie wissen ja, es gibt zu jedem VDM-Basistyp mehrere Möglichkeiten) und die von Ihren semantischen Funktionen benutzten Operationen -- natürlich nur ihre generischen Namen, die auch Enrichments  genannt werden, also ,,Anreicherungen`` des ADT.

Dateiname Der Dateiname dieser DSL-Spezifikation sollte die Endung .vdm haben.

Die Regeln, nach der Sie die Domain-Gleichungen ,,übersetzen``, finden Sie im Abschnitt 3.3.13.3.1.

Der VDM-Compiler

Bei den ersten beiden Punkten haben Sie sich vielleicht die folgenden Fragen gestellt:

• ,,Wer oder was generiert denn das Quellmodul, das meiner Anwendung die benötigten Operationen mit den entsprechend angepaßten Namen, Parameterlisten und Resultattypen bereitstellt ¿`
• ,,Wer oder was kann denn etwas mit der DSL-Spezifikation anfangen ¿`

Die Antwort auf beide Fragen lautet: der VDM-Compiler. Er liest Ihre DSL-Spezifikation (und moniert eventuelle Fehler), holt aus der VDM-Bibliothek die gewünschten Module heraus und ändert das, was geändert werden muß. Daraus entsteht eine C-Deklarationsdatei (eine sogenannte Header-Datei) und ein ADT-Implementations-Modul  in C.

Die Header-Datei  enthält die Deklarationen der Funktionen, die die Operationen realisieren, und die Definitionen der Typnamen, die Sie in der DSL-Spezifikation vergeben haben und mit deren Hilfe Sie in Ihrer Applikation Objekte der ADT erzeugen können.

Das ADT-Implementations-Modul enthält den Quellcode von Operationen und Funktionen für die dynamische Speicherverwaltung  der Objekte, die von den Operationen benötigt werden, über die aber keine Informationen in der Header-Datei stehen (weil sie in anderen Modulen nicht bekannt zu sein brauchen). Kenntnisse über den Inhalt des ADT-Implementations-Moduls benötigen Sie für die Programmierung Ihrer Applikation nicht !

Informationen mit vdminfo

 

Eine weitere Frage drängt sich Ihnen vielleicht noch auf:

,,Wenn die VDM-Bibliothek so viele Implementationen der einzelnen Basistypen enthält und so viele Operationen -- wie kann ich mir denn da Auskünfte holen, z.B. über neu hinzugekommene Implementationen oder über die Syntax der Operationen ¿`

Dokumentation Auch daran wurde gedacht. Die Dokumentation der VDM-Bibliothek ist ob ihrer Größe natürlich sehr wichtig; also wurde die Möglichkeit vorgesehen, die Dokumentation in der Bibliothek abzuspeichern. Bei Änderungen (durch befugtes Personal) muß die Dokumentation aktualisiert werden, so daß sie lückenlos den kompletten Inhalt beschreibt. Gleichzeitig wurde ein Programm namens vdminfo  erstellt, um diese Dokumentation auch nutzen zu können.

Das Kapitel 8 8 befaßt sich ausführlich mit diesem Programm. Dort ist auch die Struktur der VDM-Bibliothek erläutert (für die Programmierung mit VDM benötigen Sie keinerlei Wissen über die interne Struktur -- nur der VDM-Compiler greift auf die Bibliothek zu).

Programmentwicklung mit VDM Vienna Development Method Struktur einer Modellspezifikation