Vor- und Nachteile von Vienna Development Method Das VDM-System unter UNIX

Programmentwicklung mit VDM

 

Nachdem Sie den Aufbau des VDM-Systems, wie es in der FH Wedel installiert ist, kennengelernt haben, interessiert Sie sicherlich eine zusammenhängende Darstellung der Programmentwicklung  mit diesem VDM-System. In diesem Abschnitt werden die einzelnen Phasen schematisch dargestellt und erläutert. Ein Hinweis: Die Dateinamen, die zur Illustration des Ablaufs benutzt werden, sind natürlich nur Beispielsnamen.

Bildelemente Zuvor eine Erläuterung der Bildelemente in den folgenden Schemata:

• Gestrichelte Vierecke: Phasen der Programmentwicklung
• Dünn umrahmte Vierecke: Dokumente, die innerhalb von Phasen entstehen (und nur dort benötigt werden)
• Dick umrahmte Vierecke: Dokumente, die als Ergebnis von Phasen entstehen (jede Phase bearbeitet Ergebnisse früherer Phasen)
• Quer-Ovale: Arbeitsabläufe innerhalb von Phasen (Teilphasen)
• Rauten: Programme, die Phasenergebnisse verarbeiten
• Pfeile: Sie symbolisieren den Weg der Dokumente
• Hoch-Ovale: Modul-Bibliotheken

Design-Phase - Detailentwurf

Abb. 3.1 stellt die Design-Phase  dar, in der der Detailentwurf der Applikation erfolgt. Als Eingabe dient das Ergebnis der vorherigen Phase, der Festlegung des Systementwurfs. Der erste Schritt ist die Erstellung der entsprechenden VDM-Spezifikation in META-IV . Durch die Konkretisierung mit Hilfe der schrittweisen Verfeinerung  entsteht eine implementierbare Spezifikation (die Korrektheit jedes Verfeinerungsschrittes kann -- wie schon erwähnt -- bewiesen werden). Als Ergebnis entstehen die Domain-Gleichungen für die benötigten ADT und die Spezifikation der semantischen Funktionen  mit deren Struktur, d.h. dem Kontrollfluß der Applikation.

 
Abbildung 3.1: VDM in der Design-Phase 

Anmerkung: Nicht immer ist es möglich oder sinnvoll, die gesamte Applikation mit Hilfe von VDM zu spezifizieren -- Trivialfunktionen sollten Sie wie gewohnt ,,direkt`` in C entwerfen und implementieren. Stellen Sie aber sicher, daß die Schnittstellen zwischen den verschiedenen Teilen des Programms konsistent sind.

Übersetzung der Domain-Gleichungen

 

Die ,,Papier-Notation`` der Domain-Gleichungen  ist leider nicht maschinenlesbar. Mit geringem Aufwand können Sie sie aber konvertieren -- so entsteht der erste Teil der DSL-Spezifikation mit dem Namen My_ADT.vdm .

Regeln zur Konvertierung

• Komponenten von zusammengesetzten ADT dürfen nicht ebenfalls zusammengesetzt sein -- Verschachtelungen müssen Sie jetzt in einzelne ADT zerlegen.
• Jeder ADT-Name hat mindestens zwei Zeichen; das erste ist ein durch eine Anzahl von C-Funktionen realisiert, die der Anzahl an Datenelementen entspricht. Die Erweiterung des generischen Namens der Selektions-Operation nur um den Typ des Datenelementes reicht daher nicht aus, weil zwei Datenelemente den gleichen Typ haben könnten.
  Beispiel: Atree :: s_e1 : E1s_e2 : E2s_e3 : E1 ...
• Die Selektoren von Trees müssen mits_anfangen; sie tragen damit den gleichen Namen wie die zugehörigen Selektions-Operationen. Die weiteren Zeichen dürfen Kleinbuchstaben, Ziffern und Unterstriche sein.
• Alle Selektoren in allen Trees einer abstrakten Syntax müssen einzigartig sein, weil ihr Name jeweils ohne weitere Änderung zu einem C-Funktionsnamen wird.
• Auch die Unions können Sie mit expliziten Selektoren definieren. Da eine Union mit zwei identischen Elementtypen allerdings nicht sinnvoll ist (da sie ja immer nur ein Objekt enthält), dürfen Sie die Selektoren auch weglassen; in diesem Fall generiert der VDM-Compiler aus den Namen der Elementtypen die Namen der Selektions-Operationen (durch Voranstellen von ,,s_``).
• Als Ersatzsymbol für das Map-Zuordnungszeichen verwenden Sie -m->
• Tuples definieren Sie wahlweise mit Atuple oder Atuple +

Die Codier-Phase

Abb. 3.2 beschreibt die Codier-Phase , die auf die Design-Phase folgt. Die entstandene Struktur- und Funktions-Spezifikation wird in der Zielsprache -- in diesem Fall C -- implementiert. Die Programmiererin legt nach einer Analyse der Programmanforderungen für jeden ADT die geeignetste Implementation aus dem zur Verfügung stehenden Vorrat fest und trägt ihren Namen zusammen mit den generischen Namen der Operationen, die sie für die Implementation der semantischen Funktionen benutzt, in den zweiten Teil der DSL-Spezifikation ein, die Implementations-Beschreibungen. Die Codierung der Applikation ist noch unvollständig, denn sie ruft die ADT-Operationen auf, ohne daß sie bereits implementiert sind -- ein Mangel, der aber im nächsten Schritt vom VDM-Compiler beseitigt wird!

 
Abbildung 3.2: VDM in Detailentwurf und Codierung 

Dateien Bei der Codierung der Applikation erstellen Sie in der Regel mehrere C-Module My_Prog1.c , ..., My_Prog_n.c . Außerdem vervollständigen Sie die DSL-Spezifikation My_ADT.vdm .

Übersetzung

VDM-Compiler

Abb. 3.3 zeigt die Arbeitsweise des VDM-Compilers . Die Domain-Gleichungen werden mit den Implementations-Beschreibungen zur DSL-Spezifikation zusammengefügt, mit deren Hilfe der VDM-Compiler die benötigten Operationen aus der VDM-Bibliothek  liest und sie zum ADT-Implementations-Modul  zusammenfügt; als weiteres Ergebnis entsteht eine Header-Datei , die die Operationen in anderen Modulen bekannt macht.

 
Abbildung: VDM: Tätigkeit des VDM-Compilers 

Die DSL-Spezifikation braucht nicht in einer Datei vorzuliegen; Sie können sie auf mehrere Dateien verteilen und sie dann gemeinsam übersetzen, indem Sie dem VDM-Compiler alle Dateien gleichzeitig als Parameter mitgeben (siehe auch Anhang D).

Das Schema vereinfacht den Ablauf etwas: der VDM-Compiler kann nicht in einem Durchlauf beide Dateien erstellen, sondern braucht für jede Datei einen Durchlauf.

Dateien Das ADT-Implementations-Modul erhält den Namen My_ADT.c, die Header-Datei heißt My_ADT.h .

Optionen des VDM-Compilers 
*[1.5ex] Sie müssen dem VDM-Compiler unter anderem mitteilen, welche Datei er erzeugen soll; er kennt daher Optionen, die seine Arbeit steuern.

Option -c Der VDM-Compiler erstellt aus der angegebenen Datei das ADT-Implementations-Modul.

Option -h Der VDM-Compiler erstellt aus der angegebenen Datei die Header-Datei.

Option -e Der VDM-Compiler erstellt aus der angegebenen Datei die Enrichment-Datei . Was ist das ? Die Operationen sind zum Teil nicht in der Lage, allein ihre Aufgabe zu erfüllen, sie benötigen andere Operationen dafür. Damit Sie nicht gezwungen sind, diese Beziehungen beim Schreiben der DSL-Spezifikation zu berücksichtigen, erzeugt der VDM-Compiler temporär eine erweiterte, ,,angereicherte`` Zwischendatei, in der wirklich alle benötigten Operationen stehen (er erfährt diese internen Beziehungen aus der VDM-Bibliothek). Das muß er aber bei jeder Bearbeitung der DSL-Spezifikation tun, also mindestens zweimal -- für Header-Datei und ADT-Implementations-Modul! Dieser zeitaufwendige Vorgang kann verkürzt werden, wenn der VDM-Compiler diese Zwischendatei dauerhaft erzeugt, als sogenannte Enrichment-Datei -- sie erhält die Standard-Endung .enr . Zur Erzeugung der beiden anderen Dateien geben Sie dann die Enrichment-Datei als Eingabedatei des VDM-Compilers an mit der Option -n Option -n; damit sorgen Sie dafür, daß der VDM-Compiler die angegebene Enrichment-Datei nur liest, sie aber nicht neu erzeugt. Diese Option spart Zeit, zeigt aber erst bei größeren DSL-Spezifikationen echte Vorteile. Sie sollten Sie bevorzugt im Rahmen einer Projektverwaltung mit MAKE verwenden -- wie, sehen Sie dann im Abschnitt 3.3.4 3.3.4.

Option -o Der VDM-Compiler gibt der erstellten Datei den Hauptnamen, den Sie mit der Option -o Name festlegen. Die Dateiendung entspricht jeweils dem gewünschten Datei-Typ (Header, ADT-Implementations-Modul oder Enrichment-Datei).

Option -v Der VDM-Compiler zeigt auf dem Bildschirm an, was er gerade tut.

Für alle Optionen finden Sie hier und im Rahmen der Erläuterung von MAKE Beispiele.

Aufruf Sie rufen den VDM-Compiler  vdm mit folgendem Befehl auf:

vdm [Optionen] Spezifikations-Datei(en)
*[0.5ex] Unser Beispiel:
* Header-Datei My_ADT.h :vdm -h My_ADT.vdm -o My_ADT
* Implementations-Datei My_ADT.c :vdm -c My_ADT.vdm -o My_ADT
Mit einer Enrichment-Datei:
*[0.5ex] 1. vdm -e My_ADT.vdm -o My_ADT
* 2. vdm -c -n My_ADT.enr -o My_ADT
* 3. vdm -h -n My_ADT.enr -o My_ADT
*[2ex]

Sie müssen in jedes Modul der Applikation, in dem eine Operation aufgerufen wird (also wahrscheinlich in alle), die Header-Datei einbinden, um die Operationen und die Namen der von Ihnen definierten ADT im Modul bekannt zu machen. Dazu ist folgender Befehl nötig:

#include "My_ADT.h"
*[2ex]

C-Compiler

Abb. 3.4 schließlich zeigt, wie der unter UNIX verfügbare C-Compiler  namens cc aus den entstandenen Modulen und seiner Standard-Laufzeit-Bibliothek die fertige, lauffähige Applikation erstellt. Aus Vereinfachungsgründen ist im Schema nur ein Quellmodul für die Applikation dargestellt.

 
Abbildung: VDM: Tätigkeit des C-Compilers 

Dateien Der C-Compiler bearbeitet also folgende Dateien: My_Prog1.c , ... , My_Prog_n.c , My_ADT.c und My_ADT.h sowie eventuelle applikationsspezifische Header-Dateien.

cc übersetzt die gewünschten Quellmodule  einzeln in Objekt-Module , die ausführbaren Code enthalten und den gleichen Hauptnamen wie die Quellmodule haben, aber die Endung .o . Sie sind allein allerdings nicht ausführbar -- in einem zweiten Schritt bindet der C-Compiler sie zu einem ausführbaren Programm zusammen, das im Normalfall den Namen a.out erhält.

Aufruf des C-Compilers Aufruf des C-Compilers:  

cc [Optionen] Datei-1 Datei-2 ...
*[1ex] Für unser Beispiel:
*[1ex] cc My_Prog1.c My_Prog2.c ... My_Prog_n.c My_ADT.c -o My_Prog
*[1.5ex]

Option -o Mit der Option -o Programmname gibt der C-Compiler dem Programm einen von Ihnen angegebenen Namen statt des normalen a.out, die Option hat hier also einen ähnlichen Zweck wie beim VDM-Compiler.

Nur Binden? Der C-Compiler kann noch mehr: er kann auch fertige Objekt-Module zusammenbinden (ohne vorher zu übersetzen). Dazu geben Sie einfach nur die Namen der Objekt-Module statt der Quellmodule an.

Beispiel: Sie haben Ihr Quellmodul My_Prog1.c geändert und wollen das Programm neu erstellen. Nur dieses Quellmodul muß neu übersetzt werden, die anderen sind unverändert geblieben, also brauchen nur deren Objekt-Module eingebunden zu werden; dazu geben Sie die Namen der Objekt-Module ein.

cc My_Prog1.c My_Prog2.o ... My_Prog_n.o My_ADT.o -o My_Prog
*[1.5ex]

Option -c Eine zweite nützliche Option ist -c, die den C-Compiler veranlaßt, die übersetzten Module nicht zu binden. Das ist hilfreich, wenn Sie eine Änderung in einem Quellmodul Ihres Programms vorgenommen haben und es nur ins Objektmodul übersetzen wollen, ohne Binden. Wenn Sie das Programm MAKE zur Projektverwaltung verwenden wollen (und das ist zu empfehlen), werden Sie diese Option benötigen.

Die übrigen Optionen des C-Compilers können Sie ebenfalls verwenden, sie sind allerdings im Rahmen der Programmierung mit VDM nicht notwendig. Für weitere Informationen sei daher auf das Handbuch zum C-Compiler verwiesen.

Projektverwaltung mit make

 

Sie wissen jetzt, wie man die einzelnen Module erzeugt und übersetzt. Auch kleinere Änderungen in einem Quellmodul  machen Ihnen keine Sorgen. Aber was ist, wenn eine Änderung z.B. in der DSL-Spezifikation nötig wird ?

,,Kein Problem, ich rufe einfach nochmal den VDM-Compiler auf (natürlich mehrmals) und übersetze alle Module, die My_ADT.h verwenden, nochmal ¡`

Sehr gut, aber auch sehr aufwendig -- stellen Sie sich vor, Sie machen die dritte kleine Änderung an der DSL-Spezifikation und übersetzen alles per Hand zum dritten Mal neu...

,,Das könnte man ja durch ein Shell-Script automatisieren ¡`

Auch richtig -- und in diesem Falle auch sinnvoll, da ja tatsächlich alles neu übersetzt werden muß. Wenn Sie aber in einem Quellmodul eine kleine neue Funktion definieren, die in anderen Quellmodulen benutzt werden soll, dann ändern sich zwar einige Quellmodule und eine anwendungsspezifische Header-Datei, die diese neue Funktion nach ,,außen`` bekannt macht -- vielleicht müssen aber nicht einmal alle Quellmodule neu übersetzt werden, und die DSL-Spezifikation bleibt davon auch unberührt. Natürlich wollen Sie nur die Quellmodule neu übersetzen, die auch wirklich von der Änderung betroffen sind; dazu müssen Sie sich in Ihren Modulen sehr gut auskennen (und Lust haben, die entsprechenden Aufrufe der Compiler jedesmal einzugeben), oder Sie benutzen ein Programm, dem Sie einmal mitteilen, wie die einzelnen Module verknüpft sind und das dann automatisch mit geringstem Aufwand eine neue Version Ihrer Applikation erstellt.

Dieses Programm heißt make . Die Verknüpfungen der Module beschreiben Sie in einer Datei, der Make-Datei , und make kann erkennen, welche Module neu übersetzt werden müssen, um die neue Version zu erzeugen.

Make-Datei Eine Make-Datei besteht aus sogenannten Produktionen , die für jede beteiligte Datei angeben, von welchen anderen Dateien sie unmittelbar abhängt und wie sie aus diesen Dateien erzeugt wird -- zunächst also das Hauptprogramm, dann die Module, von denen das Hauptprogramm direkt abhängt, dann die von diesen Modulen wiederum direkt abhängigen Module usw.

Format einer Produktion Das allgemeine Format einer Produktion sieht so aus:

Zieldatei:Datei Datei ... Datei ;Kommando
*[1ex]

Die Zieldatei hängt direkt von Datei , Datei usw. ab; das Kommando erzeugt die Zieldatei aus diesen Dateien (und eventuell anderen) neu. Die Produktion braucht nicht in einer Zeile zu stehen, wenn am Ende jeder Zeile (außer der letzten) das Fortsetzungszeichen ,,\`` steht (der Backslash).

Das klingt kompliziert, ist es aber nicht. Die Beispiele in Abb. 3.5 und Abb. 3.6 sollen es Ihnen verdeutlichen; im zweiten wird mit Hilfe einer Enrichment-Datei gearbeitet.

 
Abbildung: Make-Datei für VDM 

Beispiel 1 Das eigentliche Programm besteht aus zwei Quellmodulen (z.B. Implementation der semantischen Funktionen und Steuerprogramm) und einer Header-Datei (z.B. zur Deklaration der semantischen Funktionen). Das Hauptprogramm My_Prog hängt direkt nur von den einzelnen Objekt-Modulen ab; um es zu erzeugen, wird der C-Compiler zum Binden der Objekt-Module aufgerufen.

Die Objekt-Module  My_Prog1.o und My_Prog2.o hängen jeweils von ihrem Quellmodul, der programmspezifischen Header-Datei My_Prog.h und der aus der DSL-Spezifikation entstandenen Header-Datei My_ADT.h ab; sie werden mit dem C-Compiler nur neu übersetzt (ohne Binden, daher die Option -c).

Das Objektmodul My_ADT.o hängt vom ADT-Implementations-Modul und von der zugehörigen Header-Datei My_ADT.h ab, die beide aus der DSL-Spezifikation erzeugt werden. Es wird ebenfalls mit dem C-Compiler neu übersetzt.

Das ADT-Implementations-Modul und die zugehörige Header-Datei hängen ausschließlich von der DSL-Spezifikation My_ADT.vdm ab. Sie werden jeweils durch einen Lauf des VDM-Compilers erzeugt.

 
Abbildung 3.6: Make-Datei mit Erzeugung einer Enrichment-Datei 

make, Aufruf Nachdem Sie diese Make-Datei geschrieben haben, können Sie sicher sein, daß Sie nach jeder Änderung in einer zur Applikation gehörenden Datei durch den Aufruf 

make -f Make-Datei
*[1.5ex]

die aktuellste Version der Applikation erzeugen. Eine Erleichterung: wenn Sie der Make-Datei den Dateinamen makefile geben, genügt der Aufruf von make ohne Parameter!

Vor- und Nachteile von Vienna Development Method Das VDM-System unter UNIX