VDM-Befehle: Schnellreferenz für die Vienna Development Method

VDM (Vienna Development Method) ist eine der etabliertesten modellorientierten formalen Methoden; ihre Wurzeln liegen in der Programmiersprachen-Semantik-Forschung des IBM-Labors Wien in den 1970er-Jahren. Spezifikationen werden in der formalen Sprache VDM-SL geschrieben, deren Semantik in einem ISO-Standard mathematisch festgelegt ist; VDM++ ergänzt objektorientierte Konzepte (Klassen, Vererbung, Threads), VDM-RT erweitert um Echtzeit-Aspekte.

Die Werkzeuge

Das zentrale Open-Source-Werkzeug ist das Overture Tool; sein Kommandozeilen-Kern heißt VDMJ und ist in Java geschrieben. VDMJ unterstützt alle drei Dialekte und kann per vdmj-Kommando gestartet werden, das die VDM-Dateien parst und typisiert.

vdmj -e '1+2'                    # Ausdruck auswerten
vdmj -i Spez.vdmsl               # interaktiv (REPL)
vdmj -p Spez.vdmsl               # parsen ohne ausfuehren
vdmj -t Spez.vdmsl               # typisieren

VDM-SL im Kern

  • Datenmodell: Mengen, Sequenzen, Abbildungen (Maps), Tupel, Records — Typen wie set of nat oder seq of char.
  • Explizite vs. implizite Spezifikation: explizit mit f(x) == x+1 (ausführbar), implizit über Vor- und Nachbedingungen pre/post.
  • Zustand: state-Blöcke mit inv-Invarianten; Operationen mit ext-Klauseln (rd/wr) auf Zustandsvariablen.
  • Logik: forall/exists-Quantoren, =>, not, and/or, if-then-else, cases.

VDM-Modelle werden primär zur Analyse entwickelt, nicht als Endimplementierung — man validiert sie im Interpreter, testet Invarianten und generiert daraus Code.

Verwandte formale Methoden: Isabelle, TLA+, Alloy sowie PVS und Frama-C.