DSL-Syntax Online-Hilfe mit vdminfo Die Struktur der VDM-Bibliothek

Der Aufruf von vdminfo

Format: vdminfo hat folgendes Befehlsformat:

vdminfo [Optionen] [ ADT [ Implementation [ Operation ] ] ]
*[3ex]

Die VDM-Basistypen haben innerhalb der Bibliothek abgekürzte Bezeichnungen mit maximal vier Zeichen. Es stehen momentan die in Abb. 8.2 angegebenen Basistypen zur Verfügung; die jeweiligen Implementationen sind ebenfalls angeführt.

 
Abbildung 8.2: ADT in der VDM-Bibliothek: Namen, Implementationen 

Optionen Die Optionen von vdminfo haben folgende Bedeutung:

-e  :  Ausgabe der vordefinierten Basistypen

-d  :  detaillierte Dokumentation

-c  :  C-Funktionsprototypen der Operation

Option -e Das VDM-System kennt einige vordefinierte Datentypen, die Sie auch schon kennengelernt haben: Nat0, Nat1, Intg, Bool, Char, Str. Eine DSL-Spezifikation dieser vordefinierten Typen erhalten Sie mit der Option -e.

Option -d Die Option -d, allein mit einem VDM-Basistyp angegeben, liefert Ihnen die verfügbaren Implementationen mit deren Parametern. Bei zusätzlicher Angabe einer Implementation erhalten Sie eine Liste aller Operationen, die damit verfügbar sind, inklusive den Funktionsspezifikationen.

Beispiel: Sie möchten die verfügbaren Implementationen des ADT ,,Tree`` wissen:

vdminfo -d tree
*[1ex] liefert
*[2ex] implementations for constructor ,,tree``
*[2ex] implementation ,,ptstruct``:
*[2ex] implementation ,,struct``:
*[1ex] Implementation of trees as records (Pascal) or structures (C)
* No dynamic data allocation on a heap is required, but
* assignments require copying of the whole structure.
*[3ex]

Option -c Bei detaillierter Ausgabe der Operationen einer Implementation (mit Option -d) ist die VDM-übliche Notation angegeben. Die Option -c bei Angabe einer speziellen Operation liefert den entsprechenden Prototyp der C-Funktion, mit der diese Operation realisiert ist.

Beispiel: vdminfo -d set linklist
*[1ex] liefert für die Operation is_eq:
*[1ex] is_eq (x1,x2) = ( x1 = x2 )
*[1ex] TYPE: DomainDomain-->Bool
*[2ex] vdminfo -c set linklist is_eq
*[1ex] liefert:
*[1ex] Bool is_eq ( Domain x1, Domain x2 )
*[2ex]

Domain Der Name ,,Domain`` steht für den Namen des selbstdefinierten abstrakten Datentyps; seine Domain-Gleichung würde also im Falle eines ,,Set of Element`` lauten:

Domain = Element -set.

DSL-Syntax Online-Hilfe mit vdminfo Die Struktur der VDM-Bibliothek