Prof. Dr. Uwe Schmidt

Die VDM Class Library

Was ist die VDM Class Library ?

Die VDM Class Library ist eine Toolbox zur Erstellung von C und C++ Programmen aus VDM Spezifikationen. Sie unterstützt die systematische Umsetzung von Spezifikationen in C oder C++ Programme. Sie enthält für die in der Spezifikationssprache verwendeten abstrakten Datentypen (ADTs) eine Vielzahl von Implementierungen. Mit dem Einsatz dieser Toolbox werden in den erstellten Programmen genau die gleichen Datentypen mit den gleichen Methoden verwendet wie in der Spezifikation.

Wie arbeitet das System ?

Diese Toolbox ist keine statische Klassenbibliothek, sondern die in einer Software verwendeten Klassen werden aus einem VDM Datenmodell generiert. Bei der Generierung können die Klassen an die Anforderungen der Anwendung angepaßt werden.

Ausgangspunkt für die Erzeugung ist eine Datei, die ein VDM Datenmodell enthält, in dem mit den abstrakten Datentypen Set, Map, Tuple, Bag, Record und Union ein hierarchisches Datenmodell aufgestellt wird.

Zusätzlich zu dem Datenmodell wird eine Beschreibung benötigt, mit welcher Strategie die einzelnen ADTs zu implementieren sind, verkettete Listen, binäre Bäume, ..., und welche Methoden benötigt werden, nicht alle in der library enthaltenen Methoden werden in jeder Anwendung benötigt. Aus dieser Beschreibung wird in einem Generierungsprozeß C oder C++ Quelldateien erzeugt. Arbeitet man auf C Ebene, so wird eine Header-Datei für die C Datentypdefinitionen und die Prototypen erzeugt, diese ist in das Anwendungsprogramm einzubinden. Die Implementierungsteile sind in einer C-Quellcodedatei enthalten.

Bei der Arbeit mit C++ werden ebenfalls die C-Module erzeugt, diese werden für C++ wiederverwendet, außerdem wird eine C++ Header-Datei generiert, die die C++ Klassen und Methoden definiert.

Für C++ gibt es eine sehr hilfreiche Erweiterung: die C++ Klassen können so erzeugt werden, daß die Speicherverwaltung, deren Implementierung in C++ immer sehr arbeitsintensiv und fehlerträchtig ist, vollständig in den erzeugten Klassen abläuft und vor dem Anwender vollständig verborgen bleibt.

Auf welchen Plattformen läuft die VDM Class Library ?

Das Entwicklungssystem ist im Moment Linux, lauffähig ist das System auf allen gängigen UNIX Derivaten, Sun Solaris, HP, IBM RS6000, SCO, ... Eine Portierung nach Windows NT auf dessen Posix-Interface sollte keine große Hürde sein. Die generierten C- und C++-Dateien sind (fast) systemunabhängig, können also auch auf Microsoft Plattformen eingesetzt werden.

Wo gibt es die VDM Class Library ?

Die Quellen für die Portierung auf ein neues System stehen den Studierenden der FH Wedel zur freien Verfügung. Die Verteilung von fertig generierten Binärdateien hat sich nicht bewährt, das es immer Probleme mit dynamic link libraries und deren Versionen gibt.

Welche Systemvoraussetzungen müssen erfüllt sein ?

Voraussetzung ist ein UNIX-System mit dem GNU C und C++ Compiler, empfohlen wird die Version 2.7.2 oder neuer. Für das Hilfe- und Infosystem wird das Tcl/Tk System benötigt, mindestens in der Version Tcl7.3 und Tk3.6, empfohlen wird Tcl7.5 und Tk4.1. Es gibt eine Anbindung des Hilfe- und Infosystems an das WWW, hierfür arbeitet die Toolbox in einer Client/Server Architektur, diese Erweiterung setzt zwingend Tcl7.5 und Tk4.1 voraus und natürlich einen http server, z.B. den Apache server, der bei S.u.S.E. Linux dabei ist.

Wie läuft die Installation ?

Der README file gibt Hinweise für die Installation des Systems.

Wo gibt es genauere Dokumentation und ausführlichere Information ?

• Im Hilfe- und Infosystem, entweder im Tk-basierten vdmhelp oder über den WWW Client gibt es Information über die aktuell verfügbaren ADTs und deren Eigenschaften.

• In der Test-directory des Systems gibt es Beispiele für die Benutzung und für Spezialanwendungen, z.B. Kopplung von C++ mit yacc, Einbinden von externen C Schittstellen und anderes mehr.

• Marko Temme hat in seiner Diplomarbeit den Anschluß der VDM Class Library an das WWW und die Client/Server Architektur implementiert, diese Arbeit ist sowohl in HTML als auch in PostScript verfügbar.

• In einer Diplomarbeit von Jan Peter Mohr, einem VDM Class Library Tutorium gibt es eine Einführung in den Gebrauch der VDM Class Library und eine Beschreibung der Konzepte. Dieses Dokument beschreibt den Gebrauch auf reiner C Ebene, die C++ Erweiterungen sind erst anschließend dazugekommen. Einige Absätze sind von dem LaTeX-to-HTML Filter nicht gut umgesetzt worden, für diese Details bitte im PostScript Dokument nachsehen.

• In einer weiteren, ebenfalls sehr guten Diplomarbeit von Torsten Tews über die automatische Speicherverwaltung für C++ wird die Implementierung der Speicherverwaltung mit Hilfe von Referenzzählern beschrieben.

• Jens Wulf hat in seiner Diplomarbeit die VDM Class Library um einen ADT bag für Multimengen erweitert und zwei allgemeine Implementierungen für diesen ADT bereitgestellt.

Anregungen, Tips und Kommentare bitte an

zurück zur aktuellen Information