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