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

Die Gesamtstruktur

Die DSL-Spezifikation wird in einer separaten Datei gespeichert und hat folgendes Format:

DOMAINS
*[1ex] Domain-Gleichungen
*[1.5ex] IMPLEMENTATIONS
*[1ex] Implementations-Beschreibungen
*[2ex]

Nomenklatur Da diese Datei die Eingabedatei des VDM-Compilers  ist, sollte ihr Name die Standard-Erweiterung.vdmhaben. Der Hauptname der Datei ist natürlich beliebig; wenn Sie aber einen einzelnen, universell zu verwendenden ADT losgelöst von einer Anwendung definieren, sollte der Hauptname der Datei dem Namen dieses ADT entsprechen!

Beispiel: Für die DSL-Spezifikation des universellen Datentyps Btree sollte folgender Name gewählt werden:

Btree.vdm
*[4ex]

Sie können die Spezifikation auch auf mehrere Dateien verteilen, z.B. um einen von Ihnen geschaffenen, universellen Typgenerator separat von seinen verschiedenen Elementtypen zu vereinbaren; Sie brauchen dann für eine neue Anwendung nicht die ,,alte`` DSL-Spezifikation zu ändern, sondern erstellen nur eine neue Spezifikation für den Elementtyp und übersetzen beide gemeinsam. Näheres dazu finden Sie auch im Anhang D.