Datenbankmanager
Analyse der VDM Klassenbibliotek
Preprozessor
Es ist insbesondere in der Softwarentwicklung nicht sinnvoll, das Rad neu zu erfinden. Der Entwickler greift zur Vermeidung von Ressourcenverschwendung in der Regel auf Bibliotheken (librarys) zurück. Ebensolche Ressourcen, die auch in der VDM Klassenbibliothek enthalten sind. Der Zugriff auf diese erfolgt durch den Domaincompiler mit dem Namen vdm. Der Domaincompiler wird in der Regel durch ein Shell-Skript mit dem Namen VDM aufgerufen, das die Parametrisierung vereinfacht.
Die Arbeitsweise des Domaincompilers ist durch das VDM-Handbuch von Jan Peter Mohr [JM95] hervorragen beschrieben. Es soll daher nur ein Abriß über den Domaincompiler wiedergegeben und auf diese Fundstelle verwiesen werden, um eine schlichte Wiederholung zu vermeiden.
Der Domaincompiler liest eine Datei ein, die DSL-Spezifikation enthält[JM95, S.143,]. Der mit lex und yacc erzeugte Scanner und Parser des Domaincompilers verarbeitet die Syntax, und extrahiert aus der Klassenbibliothek die benötigen Fragmente. Da der Objektcode des VDM Preprozessors im Domaincompiler enthalten ist, kann eine direkte Verarbeitung der Elemente noch durch den Compiler selbst erfolgen, der die vormals abstrakten Datentypen wie sets, tuples, maps, functions, trees oder bags konkretisiert und diese für die gewählte Zielsprache in Quellcode umsetzt.
Der Quellcode wird durch einen Compiler, der die Zielsprache verarbeitet, gemeinsam mit dem Quellcode der Applikation, welche die Bibliothek verwendet, übersetzt und gebunden.