Btree; *[0.5ex] typedef struct {
* Btrees_lt;
* Datas_data;
* Btrees_rt;
* } Struct_btree;
*[1.5ex]
Beispiel: Syntaxdefinition von Programmiersprachen
Rekursive Typdefinition
Verwaltung von variablen Datenmengen
Die verschiedenen Rekursionskonzepte wurden mit Hilfe von VDM-Domain-Gleichungen illustriert und können natürlich mit VDM realisiert werden. Der große Vorteil ist die Vermeidung des Umgangs mit Pointern auf Objekte, um den Sie in C nicht herumkommen und der sehr fehlerträchtig ist. Sie können mit Hilfe von VDM allgemeine Datenorganisationsformen wie z.B. Binärbäume oder auch B-Bäume ohne übermäßigen Testaufwand realisieren und bei Bedarf wiederverwenden, da VDM von Implementations-Details abstrahiert. Da solche Organisationsformen in sehr vielen Anwendungen benötigt werden, sinkt die Erstellungszeit für solche Anwendungen bei Verwendung von VDM deutlich.
Für die an rekursiven Strukturen beteiligten Datentypen können Sie nicht jede Implementation verwenden; weil Verweise auf Nachfolgeknoten benötigt werden, müssen die Implementationen auf Pointern basieren. Ein Beispiel: Bei Auswahl der struct-Implementation für den oben angegebenen Binärbaum erzeugt der VDM-Compiler folgende Typdefinition, aus der der C-Compiler keinen Code erzeugen kann, weil die Rekursion nicht auflösbar ist:
typedef struct {
*
Btrees_lt;
*
Datas_data;
*
Btrees_rt;
*
} Btree;
*[1.5ex]
Wählen Sie stattdessen die ptstruct-Implementation, die auf Pointern basiert, kann ein korrekter C-Quelltext generiert werden:
typedef Struct_btree Btree;
*[0.5ex]
typedef struct {
*
Btrees_lt;
*
Datas_data;
*
Btrees_rt;
*
} Struct_btree;
*[1.5ex]
Meist benötigen Sie zwei ,,über Kreuz`` rekursive Strukturen oder sogar mehrere Strukturen, die einen Zyklus von Verweisen enthalten, ohne daß eine der Einzelstrukturen rekursiv ist, weil die DSL-Syntax verlangt, daß alle verschachtelten Datentypen in einzelne Definitionen zerlegt werden. In diesem Fall muß mindestens einer der beteiligten Datentypen mit Hilfe von Pointern implementiert werden. Ein Beispiel dafür sind die beiden Datentypen Btree und Node für Binärbäume.
Der VDM-Compiler kann feststellen, ob die Rekursion auflösbar ist oder nicht, indem er die gewählten Implementationen analysiert und die Typdefinitionen in einer auflösbaren Reihenfolge anordnet, wenn er eine Pointer-Implementation findet. Gelingt ihm das nicht, bricht er mit folgender Fehlermeldung ab: dependency cycle detected
Beispiel: Syntaxdefinition von Programmiersprachen
Rekursive Typdefinition
Verwaltung von variablen Datenmengen