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.