auf Objekte vom Typ 
abbildet, schreiben Sie
Optionals
Die VDM-Basistypen
Tuples
Definition Eine Map ist eine partielle Funktion, die Objekten aus einer Argumentmenge andere Objekte aus einer Zielmenge zuordnet. Die Argumentmenge ist endlich; ihre Elemente sind ungeordnet, so daß die Paare nicht in einer Reihenfolge stehen.
Nomenklatur Die Argumentmenge heißt auch Argument-Domain . Die Zielmenge wird auch Co-Domain genannt. Die Elemente der Argumentmenge heißen Argumentwerte , die ihnen zugeordneten Werte aus der Zielmenge heißen Map-Werte.
Häufig kann keine allgemeine Regel zur Erzeugung der Map-Werte angegeben werden. Das entscheidende bei einer Map ist allerdings folgendes: die Paare sind durch die Argumentwerte eindeutig definiert, denn kein Argumentwert kann mehr als einen Map-Wert haben! Also dient der Argumentwert als ,,Schlüssel`` zum Map-Wert; um auf ein Paar zuzugreifen, benötigt man nur Kenntnisse über den Argumentwert.
Maps und Sets Aus diesen Angaben kann man ersehen, daß die Argumentmenge ein Set im Sinne des Abschnitts 5.4 ist, auf den die Set-Operationen angewendet werden können. Für Maps gibt es dementsprechend viele ähnliche Operationen.
DSL Um in einer DSL-Spezifikation eine Map zu
definieren, die Objekte vom Typ auf Objekte vom Typ
abbildet, schreiben Sie
Dies ist die ,,maschinenlesbare`` Schreibweise von 
Anwendung Die Map ist der vielseitigste VDM-Basistyp. Ihr Einsatz ist immer dann angezeigt, wenn Sie eine ungeordnete Sammlung verschiedener, zusammengesetzter Objekte modellieren sollen, die möglichst schon durch einen ihrer Teile genau bestimmt sind und auf die Operationen wie Suche nach Objekten, oder Hinzufügen, Löschen und Ersetzen von Objekten angewendet werden sollen. Die letztgenannten Operationen geben Ihnen vielleicht einen Hinweis: die Manipulation von indizierten Datensätzen ist mit Hilfe von Maps gut durchzuführen -- der Index (Primärschlüssel) kann als Argumentwert dienen.
Beispiele Sie können auch ein Tuple mit einer Map darstellen, wenn Sie auf die Reihenfolge der Indizes verzichten; der Typ der Argumentwerte ist dann der Zahlentyp Nat1 . Sie können aber, wenn Sie auch negative Indizes benötigen, ebensogut den Typ Intg verwenden -- Sie sind also flexibler, was den Typ der Indizes angeht. Die Implementation ,,scaldom`` unterstützt übrigens genau diese Anwendung von Maps. Häufig spricht aber die Ordnung der Elemente und -- vor allem -- der schnellere Zugriff auf die Elemente für die Wahl des Tuple statt der Map.
DOMAINS
*
Elem=...
*
Amap=Nat0 
Elem
*
Atup=Elem 
*[1.5ex]
Eine weitere Anwendung ist die Zuordnung von Dateinamen des Datei-Systems zu ihren Inhalten. Wenn es sich um sequentielle Dateien mit Daten des gleichen, elementaren Typs handelt, kommt als Zielmenge idealerweise ein Tuple in Betracht. Auch diese Anwendung wird durch eine Implementation besonders unterstützt, nämlich durch ,,dir``.
DOMAINS
*
Elem=...
*
Atup=Elem
*
Amap=Str Atup
*[1.5ex]
Wenn Sie in C mit dynamischen Objekten umgehen, vereinbaren Sie für den Zugriff einige statische Pointer. Sie benötigen in der Regel keine Operationen für die Bearbeitung der Gesamtheit dieser Pointer, sondern nur den Zugriff auf das Heap-Objekt sowie Erzeugen und Löschen solcher Objekte. Die Adresse eines Objekts auf dem Heap ist dabei ein Charakteristikum dieses Objekts; Sie können also auch Pointer und Objekte zu einer Map zusammenfassen und die Objekte mit Hilfe der Map-Operationen manipulieren. Wenn Probleme und Fehler beim Umgang mit diesen Objekten auftauchen, können Sie die Implementation der Map einfach austauschen -- Sie haben dann zwar mehr Verwaltungsaufwand, aber auch eine ,,sichere`` Basis für die Manipulation der Heap-Objekte. Im Abschnitt 5.6.5 wird diese Anwendung ausführlicher beschrieben.
Nach diesen sehr speziellen Anwendungen nun noch eine ,,gewöhnliche``, die im weiteren auch zur Erläuterung der Operationen eingesetzt wird.
Ein Datei-System enthält Verzeichnisse, die Dateien enthalten. Jede Datei ist durch ihren Namen eindeutig gekennzeichnet. Ein Verzeichnis kann also als Map von Dateinamen auf Dateien modelliert werden, während ein Datei-System eine Map von Verzeichnisnamen auf Verzeichnisse ist. Die Dateien sind einfach Tuples von irgendwelchen, nicht näher definierten Datensätzen.
DOMAINS
*
Filesys=Str
Dir
*
Dir = Str File
*
File = Rec
*
Maps können durch fünf Implementationen repräsentiert werden:
Vorbemerkung Die Operationen für Sets und Tuples sind entweder Prozeduren oder ,,echte`` Funktionen, die genau ein Resultat haben. Für Maps hat es sich als praktikabel erwiesen, Operationen mit mehreren Resultaten bereitzustellen; dazu erhalten diese Funktionen Referenzparameter, die (wie in C üblich) in Form ihrer Adresse übergeben werden.
,,heap`` Die Implementation ,,heap`` stellt einen Sonderfall einer Map dar, daher sind nur sehr wenige Operationen verfügbar, auf die im folgenden jeweils explizit hingewiesen wird. Fehlt dieser Hinweis also, gibt es die Operation unter ,,heap`` nicht.
Zur Erläuterung der Operationen dienen folgende Variablen:
Filesysfs;
*
Dir d1, d2, d3, d4;
*
File f1, f2;
*
Str fname, dname;
mk_empty Mitmk_empty
erzeugen Sie eine leere Map. mk_empty ist in der Implementation
,,heap`` verfügbar.
*
Beispiel -- Einrichtung eines Datei-Systems auf einem neuen Rechner:
fs = mk_empty_filesys();
*[1.5ex]
mk_one Mimk_oneerzeugen Sie
eine ein-elementige Map. Natürlich müssen Sie hier zwei Argumente
angeben, die die beiden Teile des ersten Paares in der Map angeben.
*
Beispiel -- Erzeugung eines Verzeichnisses mit einer Datei:
d1 = mk_one_dir(fname, f1);
*[1.5ex]
copy / copy1 Natürlich gibt es auch für Maps die beiden Kopier-Operationen copy und copy1.
Die Kombinatoren sind zum größten Teil von den Sets her geläufig, denn sie beziehen sich auf den Argument-Domain einer Map; die Map-Werte werden dabei meist nur als ,,Zubehör`` der Argumentwerte betrachtet.
Die einzige Ausnahme ext ist daher auch nur in den Implementationen ,,heap`` und ,,heapmap`` verfügbar, die ja, was ihre Argumentwerte angeht, einen Sonderstatus einnehmen: es sind die Pointer auf Daten auf dem Heap.
ext Mitexttragen Sie einen neuen Map-Wert in die Map ein, die hier Referenzparameter ist. Der Argumentwert, dem der neue Map-Wert zugeordnet wird, also ein Pointer auf den Map-Wert, wird als Resultat geliefert. Beispiel:
DOMAINS
*
Token = ELEMENTARY
*
Map = Token-m->Str
*
IMPLEMENTATIONS
*
Token = ptr + ...
*
Map = heap + mk_empty + ext + ...
Token t;
*
Map m;
*
Str s;
*
*
m = mk_empty_map();
*
t = ext_map(&m,s);
*[1ex]
Der String wird an freier Position auf dem Heap abgespeichert, seine Adresse wird im Token abgelegt. Die Operation entspricht also einer normalen Speicherallokation.
Die übrigen Kombinatoren sind für alle Implementationen verfügbar:
union Mitunionfügen Sie zwei
Maps zusammen, vereinigen also ihre Argumentmengen. Eine Vorbedingung muß
allerdings erfüllt sein: den Argumentwerten, die in beiden Maps auftreten,
muß jeweils der gleiche Map-Wert zugeordnet sein! Hinzu kommt die Version
uniond mit implizitem Löschen.
*
Beispiel -- Sie fügen zwei Verzeichnisse zu einem zusammen; enthalten sie
gleiche Dateien (Name und Inhalt), wird eine der beiden gelöscht:
d1 = uniond_dir(d1,d2);
*[1.5ex]
union1 Mitunion1tragen Sie
in eine Map ein neues Paar ein, das also noch nicht enthalten ist.
Erlaubt ist allerdings auch, daß die Map das Paar bereits enthält; in diesem
Falle können Sie eines der beiden identischen Paare mit union1d implizit
löschen. Ein Fehler ist aber das Hinzufügen eines Paares, dessen
Argumentwert mit einem anderen Map-Wert in der Map enthalten ist!
union1 ist in der Implementation ,,heap`` verfügbar.
*
Beispiel -- ein neues Verzeichnis wird ins Datei-System eingetragen:
fs = union1_filesys(fs,dname,d1);
*[1.5ex]
ovwrt Mitovwrtfügen Sie
ebenfalls zwei Maps zu einer zusammen, allerdings braucht die Vorbedingung von
union hier nicht erfüllt zu sein: ein Argumentwert darf in beiden Maps
vorkommen und jeweils einen unterschiedlichen Map-Wert haben! Die zweite
angegebene Map ist dabei dominant. Die Version mit implizitem Löschen heißt
ovwrtd.
Beispiel -- beim Zusammenfügen zweier Verzeichnisse sollen die Dateien des
zweiten Vorrang genießen:
d1 = ovwrtd_dir(d1,d2);
*[1.5ex]
ovwrt1 Mitovwrt1überschreiben
Sie ein Paar in einer Map durch ein neues (ist es noch nicht vorhanden, wird
es ganz normal eingefügt). ovwrt1d ist die Version mit implizitem
Löschen. ovwrt1 ist in der Implementation ,,heap`` verfügbar.
Beispiel -- Sie wollen eine Datei nach einer Änderung wieder zurück ins
Verzeichnis schreiben; die alte Version der Datei soll dabei gelöscht werden:
d1 = ovwrt1d_dir(d1,fname,f1);
*[1.5ex]
sub Mitsubentfernen Sie alle
Paare, deren Argumente in einer Map vorhanden sind, aus einer anderen Map
(unabhängig vom Map-Wert). subd löscht dabei implizit.
Beispiel -- Sie haben zwei Verzeichnisse, die zum Teil identische Dateien
enthalten. In einem dieser Verzeichnisse wollen Sie die doppelten Dateien
löschen:
d1 = subd_dir(d1,d2);
*[1.5ex]
sub1 Mitsub1entfernen Sie das
Paar, dessen Argumentwert Sie angeben, aus einer Map (wenn es enthalten ist).
sub1d löscht dabei das Argument und den Map-Wert implizit. sub1
ist in der Implementation ,,heap`` verfügbar.
*
Beispiel -- Sie wollen ein ganzes Verzeichnis aus Ihrem Datei-System löschen:
fs = sub1d_filesys(fs,dname);
*[1.5ex]
inters Mitintersbilden Sie
den Durchschnitt zweier Maps, also genau die Paare, die in beiden Maps
enthalten sind -- die Gleichheit betrifft sowohl den Argumentwert als auch
den Map-Wert! intersd löscht implizit die Paare, die nicht im Ergebnis
vorkommen.
*
Beispiel -- Sie möchten die vollkommen identischen Dateien zweier
Verzeichnisse herausfinden, nicht aber die Datei-Paare, die den gleichen Namen
haben, aber unterschiedlichen Inhalt; die gemeinsamen Dateien sollen in ein
neues Verzeichnis eingetragen werden, die alten Verzeichnisse sollen
unverändert bleiben:
d3 = copy_dir(d1);
*
d4 = copy_dir(d2);
*
d3 = intersd_dir(d3, d4);
*[0.5ex]
d4 dient nur als temporärer Speicher und wird von intersd
vollständig wieder gelöscht.
is_eq Mitis_eqermitteln
Sie, ob zwei Maps vollkommen identisch sind, also die gleiche Anzahl
Argumentwerte haben, die jeweils in beiden Maps identisch sind und denen
jeweils identische Map-Werte zugeordnet sind.
*
Beispiel -- Test, ob zwei Verzeichnisse identisch sind; wenn ja, kann das
eine komplett gelöscht werden:
if (is_eq_dir(d1,d2))
*
del_dir(d2);
*[0.5ex]
Es wird angenommen, daß die Dateien jeweils doppelt existieren, daß die
Verzeichnisse also nicht nur Verweise auf Dateien enthalten; sonst wäre das
Löschen aller Sub-Strukturen fatal!
is_empty Mitis_empty
ermitteln Sie, ob eine Map keine Paare enthält.
*
Beispiel -- Test, ob ein einem Verzeichnis Dateien enthalten sind; wenn
nicht, kann das Verzeichnis gelöscht werden:
if (is_empty_dir(d1))
*
del1_dir(d1);
*[0.5ex]
Das Löschen mit del1 genügt hier, da es keine Sub-Strukturen gibt, die
ebenfalls gelöscht werden können.
is_in Mitis_inermitteln
Sie, ob ein Argumentwert in einer Map enthalten ist.
*
Beispiel -- Sie prüfen, ob ein Dateiname in einem bestimmten Verzeichnis
enthalten ist; wenn nicht, tragen Sie eine Datei mit diesem Namen ein:
if (!is_in_dir(d1,fname))
*
d1 = union1_dir(d1,fname,f1);
*[1.5ex]
is_submap Mitis_submap
prüfen Sie, ob eine Map vollständig in einer anderen Map enthalten ist, das
heißt, ob alle ihre Paare ein identisches Pendant in der anderen Map haben.
*
Beispiel -- wenn alle Dateien eines Verzeichnisses identisch in einem anderen
Verzeichnis vorkommen, kann das Verzeichnis gelöscht werden:
if (is_submap_dir(d1,d2))
*
del_dir(d1);
*[0.5ex]
Es gibt noch vier weitere Prädikate, die aber gleichzeitig ein Objekt selektieren, wenn das Prädikat erfüllt ist. Aus diesem Grund sind sie unter den Selektions-Operationen aufgeführt. Es handelt sich um is_in_dom, is_in_rng, is_in_min und is_in_max.
card cardliefert die Anzahl an
Paaren in einer Map.
*
Beispiel -- Anzahl der Dateien in einem Verzeichnis:
printf("%d", card_dir(d1));
*[2ex]
sel Mitselermitteln Sie den
Map-Wert, der dem angegebenen Argumentwert zugeordnet ist; eine übliche
Schreibweise dieser ,,Anwendung der Map`` (map apply) ist auch
val = map(arg). sel ist in der Implementation ,,heap`` verfügbar.
*
Beispiel -- Sie wollen die Datei mit dem Namen rec.dat verarbeiten:
fname enthält "rec.dat"
*
f1 = sel_dir(d1, fname);
*[1.5ex]
sel_dom Mitsel_domerhalten
Sie irgendeinen zufälligen Argumentwert der Map (die Wirkung entspricht also
der sel-Operation für Sets).
*
Beispiel (nicht sehr sinnvoll) -- Sie benötigen irgendeinen Dateinamen, der
in einem Verzeichnis vorkommt:
fname = sel_dom_dir(d1);
*[1.5ex]
Selektion mit Prädikaten Die folgenden Operationen sind Kombinationen von Prädikaten und Selektions-Operationen, denn sie liefern ein Objekt (immer als Referenzparameter), wenn das Prädikat erfüllt ist; ist es nicht erfüllt, ist der Referenzparameter undefiniert. Das Resultat ist jeweils ein Wahrheitswert.
is_in_dom is_in_domprüft (wie
is_in), ob ein bestimmter Argumentwert in einer Map enthalten ist;
wenn ja, wird auch der zugeordnete Map-Wert geliefert.
*
Beispiel -- wenn die Datei rec.dat in einem Verzeichnis existiert, soll
sie verarbeitet werden:
fname enthält "rec.dat"
*
if (is_in_dom_dir(fname, d1, &f1))
*
process_file(f1);
*
else
*
perror("rec.dat nicht vorhanden");
*[1.5ex]
is_in_rng Mitis_in_rng
ermitteln Sie, ob ein Map-Wert in einer Map enthalten ist; wenn ja, erhalten
Sie den zugehörigen Argumentwert. Ist der Map-Wert mehrfach vorhanden, wird
der Argumentwert zufällig ausgewählt.
*
Beispiel -- Sie möchten wissen, ob und wenn ja unter welchem Dateinamen eine
bestimmte Datei in einem Verzeichnis enthalten ist:
if (is_in_rng_dir(f1,d1,&fname))
*
puts_str(fname);
*[1.5ex]
is_in_min Mitis_in_min
ermitteln Sie den kleinsten Argumentwert in einer Map, der größer oder
gleich dem angegebenen ist (wenn es überhaupt einen solchen gibt).
*
Diese Operation kann z.B. angewendet werden, wenn Sie eine indizierte Datei
mit einer Map von Key auf Datensatz modelliert haben und einen Teilschlüssel
suchen:
DOMAINS
*
File=Str Record
*
*
keyist ein Teilschlüssel und enthält,,Schmi``
*
if (is_in_min_file(key, f, &fullkey))
*
process_rec(sel_file(f, fullkey);
*[0.5ex]
Der erste Schlüssel, der größer oder gleich ,,Schmi`` ist (also z.B.
,,Schmid``), wird gesucht und der zugehörige Datensatz verarbeitet.
is_in_max is_in_maxsucht den
größten Argumentwert in einer Map, der kleiner oder gleich dem angegebenen ist
(wenn es einen solchen gibt).
*
is_in_max ist also der Partner von is_in_min, der z.B. für die
Teilschlüsselsuche in einer absteigend sortierten indizierten Datei oder vom
Dateiende her verwendet werden kann.
Es gibt für Maps (wie auch für Tuples) Operationen zum Zugriff auf das Datei-System, allerdings nur Spezialfälle, die dementsprechend deutlichen Einschränkungen unterworfen sind:
Die Implementationen ,,heap``, ,,heapmap`` und ,,scaldom`` scheiden also bereits aus, da ihre Argumente keine VDM-Strings sein können.
Anwendung Zur Verwaltung einfacher Tuples reicht die ,,Standardversion`` aus:
DOMAINS
*
Dir=Str File
*
File=Rec
*[1.5ex]
Eleganter ist die rekursive Definition des Co-Domain, entweder als Datei oder als weiteres Verzeichnis; damit kann ein hierarchisches Datei-System wie unter UNIX oder MS-DOS verwaltet werden. Damit ist eine einfache indizierte Dateiverwaltung möglich, die für jeden Datensatz eine Datei anlegt: sie arbeitet mit Schlüsseln, die in Verzeichnis- und Dateinamen zerlegt werden. Eine beliebig tiefe Strukturierung der Schlüssel ist möglich -- der einzige Nachteil ist, daß jeder Datensatz eine Datei bildet und sehr viel Festplattenplatz vergeudet (Verwaltungsinformation für die Verzeichnisse und Datei-Speicherplatz, der in der Regel blockweise vergeben wird). Die Definition benutzt Unions , die im Abschnitt 5.9 genauer behandelt werden:
DOMAINS
*
Direc=Str
Direntry
*
Direntry = Datfile | Direc
,,dir`` Die Implementation ,,dir`` kann diese beiden Map-Strukturen direkt auf der Festplatte verwalten. Nur bei Bedarf wird ein Teil des Datei-Systems in den Hauptspeicher geladen, wo die ,,linklist``-Implementation verwendet wird (momentan die einzige Möglichkeit...). Wenn Sie also sehr viele Objekte in Ihrer Applikation verwalten, sollten Sie überlegen, die Implementation ,,dir`` zu verwenden, um Hauptspeicherplatz zu sparen.
Haben Sie eine solche Map vereinbart, stehen die folgenden beiden Operationen zur Verfügung; beide haben einen VDM-String als Argument, der den Verzeichnisnamen festlegt.
fread Mitfreadwird ein durch einen VDM-String bezeichnetes Verzeichnis des Datei-Systems in eine Map eingelesen. Unterverzeichnisse (wenn sie vorhanden sind) bilden untergeordnete Maps, Dateien werden in Tuples gelesen. Tritt bei einer Datei-Operation ein Fehler auf, wird die leere Map zurückgeliefert.
dirvar = fread_direc(dname);
*
if (is_empty_direc(dirvar))
*
file_error();
*[1.5ex]
fwrite Mitfwritewird umgekehrt eine Map in entsprechende Verzeichnisse bzw. Dateien des Datei-Systems geschrieben. Tritt bei einer Datei-Operation ein Fehler auf, wird FALSE zurückgeliefert, sonst TRUE.
if (!fwrite_direc(dirvar, dname))
*
file_error();
*[2.5ex]
Zur Erzeugung neuer, komplexer Funktionen mit Hilfe der vorhandenen gibt es zwei Funktionale, die Sie mittlerweile von den Sets und Tuples her kennen. Wie schon gesagt: wenn Sie mit der folgenden Beschreibung Schwierigkeiten haben, sollten Sie die entsprechenden Passagen ab lesen.
binary Mitbinarykönnen binäre Funktionen die eine Map und eine Paar -- Argumentwert und Map-Wert -- in eine Map überführen, verallgemeinert werden zu Funktionen, die aus zwei Maps eine neue Map erzeugen. Eine mit binary erzeugte Funktion arbeitet wie folgt:
Amap newfct_amap (Amap m1,Amap m2)
*
{
*
Argdom a;
*
Codom c;
*[0.5ex]
if (is_empty_amap(m2))
*
return m1;
*
else {
*
a = sel_dom_amap(m2);
*
c = sel_amap(m2, a);
*
return newfct_amap(foldfct_amap(m1, a, c),
*
sub1_amap(m2,a));
*
}
*
}
foldfct hat bei Maps drei Argumente, eine Map, einen Argumentwert und einen Map-Wert, und liefert wieder eine Map. Sie wird mit dem Implementationsparameter ,,FOLDFCT`` definiert.
fold Das Funktionalfoldhat drei Parameter-Funktionen und erzeugt eine Funktion, die eine Map auf einen durch die Parameter-Funktionen festgelegten Resultattyp abbildet. Damit lassen sich sehr gut komplexe Manipulationen aller Paare einer Map realisieren. Die Bedeutung der Parameter-Funktionen ist Ihnen ja bereits bekannt (Konvertierungsfunktion, Null-Funktion und Fold-Funktion).
CVFCT Bei Maps ist die Konvertierungsfunktion allerdings nicht optional, da sie ein Paar der Map in einen Wert vom Resultattyp umwandelt. Ihr Name wird sowohl mit dem Namen des Argument-Domains als auch mit dem Namen des Co-Domains erweitert.
Die erzeugte Funktion sieht von der Struktur her wie folgt aus:
Result newfct_amap (Amap m)
*
{
*
Argdom a;
*
Codom c;
[0.5ex]
if (is_empty_amap(m))
*
return nullfct_result();
*
else {
*
a = sel_dom_amap(m);
*
c = sel_amap(m, a);
*
return foldfct_result(cvfct_argdom_codom(a, c),
*
newfct_amap(sub1_amap(m, a)));
*
}
*
}
*
Beispiel: Zwei Standard-Operationen für Maps werden von VDM a priori nicht unterstützt, da der Ergebnistyp nicht in jeder Applikation spezifiziert ist. Mit Hilfe von fold können Sie sie aber leicht generieren, wenn Sie die entsprechenden Datentypen definiert haben. Es handelt sich um den Set aller Argumente (der mit der Standard-Operation dom ermittelt wird) und den Set aller Map-Werte (Ergebnis der Standard-Operation rng). Folgende Domain-Gleichungen sind notwendig:
DOMAINS
*
Amap=Ārg
Rng
*
Argset =Arg -set
*
Rngset =Rng -set
dom Die Operation dom ist die Vereinigung (union) aller einelementigen Sets, die aus der Argumentmenge der Map gebildet werden können. Die Nullfunktion erzeugt also den leeren Argset, die Konvertierungsfunktion wandelt ein Paar in einen ein-elementigen Argset um. Diese letzte Funktion müssen Sie selbst schreiben; das ist aber ganz leicht -- nur die Ermittlung des Funktionsnamens erfordert kurzes Nachdenken:
IMPLEMENTATIONS
*
Amap= ¯...
*
+ fold.dom(RESULT=
Argset toargset_arg_rng (Arg a, Rng r) "Argset",
*
CVFCT="toargset",
*
NULLFCT="mk_empty",
*
FOLDFCT="union")
*
{ return mk_one_argset(a); }
*[1.5ex]
rng Die Operation rng wird nach demselben Muster definiert, nur der Resultattyp und die Konvertierungsfunktion sind zu ändern:
IMPLEMENTATIONS
*
Amap= ¯...
*
+ fold.rng(RESULT=
Rngset torngset_arg_rng (Arg a, Rng r) "Rngset",
*
CVFCT="torngset",
*
NULLFCT="mk_empty",
*
FOLDFCT="union")
*
{ return mk_one_rngset(r); }
*[1.5ex]
Beachten Sie: Hier werden natürlich andere Versionen von mk_empty und union ausgewählt als bei der Funktion dom .
Zusätzliche Parameter Eine einfache Anwendung für zusätzliche Parameter für eine der Parameterfunktionen finden Sie im abschließenden Beispiel über eine Stücklistenverwaltung mit Maps beim Verständnis des zusätzlichen Implementations-Parameters haben, schauen
forall Mitforallführen Sie
mit allen Paaren in einer Map eine Prozedur aus, die zwei Elemente hat: eines
aus dem Argument-Domain und eines aus dem Co-Domain der Map.
*
Beispiel -- Ausgabe eines Hexdumps für alle Dateien in einem Verzeichnis:
void hexdump(Str name, File f)
*
{ puts_str(name);dump_file(f); }
*[1ex]
forall_dir(d1, hexdump);
*[1.5ex]
forrange Mitforrangeführen
Sie mit allen Paaren einer Map, deren Argumentwert in einem angegebenen
Bereich liegt, eine Prozedur aus, die zwei Elemente hat: eines aus dem
Argument-Domain und eines aus dem Co-Domain der Map. Voraussetzung ist, daß
für den Argument-Domain die Operation is_ge definiert ist; dies ist
z.B. bei Sets nicht gegeben.
*
Beispiel -- Hexdump aller mit ,,F`` beginnenden Dateien in einem Verzeichnis:
Str f1, f2;
*[1ex]
f1 = mk_one_str('F');
*
f2 = mk2_str('F','~');
*
forrange_dir(d1, hexdump, f1, f2);
*
Hinweis: alle mit ,,F`` beginnenden Dateinamen sind kleiner als ,,F~``.
forsome Mitforsomeführen
Sie mit allen Paaren einer Map, die ein angegebenes Prädikat erfüllen (
beide Teile des Paares werden dem Prädikat übergeben), eine Prozedur aus,
die zwei Elemente hat: eines aus dem Argument-Domain und eines aus dem
Co-Domain der Map.
*
Beispiel -- Hexdump aller mit ,,F`` beginnenden Dateien, die weniger als
100 Datensätze haben:
Bool test_file (Str name, File f)
*
{ return hd_str(name) == 'F' && len_file(f) < 100
}
*[1ex]
forsome_dir(d1, test_file, hexdump);
*[3ex]
Stückliste Eine Stückliste enthält alle Teile, die für die Konstruktion eines Werkstücks benötigt werden. Für diejenigen Teile, die zusammengesetzt sind, also untergeordnete Bestandteile haben, ist zudem diese Zusammensetzung angegeben; diese Liste von Elementen ist für die nicht weiter zerlegbaren Teile (die ,,Rohstoffe``) natürlich leer.
Es ist zwar sinnvoll, die Anzahl der benötigten Teile zur Zusammensetzung einer größeren Einheit ebenfalls in die Stückliste einzutragen. Für unser Beispiel wollen wir uns aber auf eine qualitative Stückliste beschränken, die für jedes zusammengesetzte Teil nur die benötigten Elemente enthält, unabhängig von ihrer Stückzahl.
Wir nehmen weiter an, daß ein Teil durch seine Teilnummer (part number) eindeutig gekennzeichnet ist.
Modell Einem zusammengesetzten Teil wollen wir die (ungeordnete) Menge der Teilnummern seiner Bestandteile zuordnen. Ist das Teil nicht zerlegbar, soll diese Menge leer sein. Aus dieser Beschreibung leiten wir das abstrakte Modell ab: ein Eintrag in der Stückliste ist eine funktionale Zuordnung zwischen einer Teilnummer und dem (möglicherweise leeren) Set der Bestandteile dieses Teils; die Stückliste ist also eine Map von Teilnummern auf Sets von Teilnummern! Die DSL Domain-Gleichungen zur Modellierung einer Stückliste Plist sieht so aus:
DOMAINS
*
Plist= Pn
Pnset
*
Pnset = Pn -set
*
Pn = ELEMENTARY
*
Invariante Wann ist eine Stückliste wohlgeformt ?
Die VDM-Spezifikation der Datentyp-Invarianten für die Stückliste sieht dann so aus:
inv-Plist(plist) =
*
*
*[1.5ex]
Die beiden obigen Bedingungen sind jeweils in einer Zeile der Invariante formalisiert:
Die Invariante wollen wir hier nicht überprüfen. Sie finden eine Anwendung in sehr ähnlicher Form, nämlich für eine quantitative Stückliste, im Kapitel 7, wo ein komplettes Beispiel für die Anwendung von VDM dargestellt wird.
parts_pn Die semantische Funktion parts_pn müssen wir selbst definieren; sie liefert den Set aller Bestandteile eines Teils. Dies ist auf jeden Fall eine nützliche Funktion für unsere Stückliste. Wir spezifizieren sie implizit:
TYPE parts_pn(pn, plist)(ps):PnPlist
Pnset
*
pre: pn 
dom plist
*
post: ps =
*
*[1.5ex]
postcondition Die postcondition verlangt
natürlich nach einer Erklärung, zumal sie eine Rekursion enthält. ps ist
der Set aller Teile p, für die gilt: p ist in der Stückliste beschrieben
(also in der Argumentmenge enthalten) UND es ist entweder ein direktes
Bestandteil des Teils pn (also in dessen Map-Wert enthalten) ODER es gibt
ein Teil 
in dem hier gerade zu konstruierenden Set ps, dessen
direktes Bestandteil p ist (sodaß also p im Map-Wert von
enthalten ist).
Wegen der Rekursion bezüglich ps sollte man diese Funktion auch rekursiv realisieren. Ein Problem haben wir aber: der Typ des gewünschten Resultats ist nicht identisch mit dem Parametertyp! Wir behelfen uns, indem wir eine Hilfsfunktion parts_pnset schaffen, die als Argument einen Set ps von Teilen hat und einen Set aller Bestandteile der Teile in ps liefert. Diese Hilfsfunktion brauchen wir nur noch mit dem Set der direkten Bestandteile von pn aufzurufen und erhalten das gewünschte Ergebnis. Damit können wir die semantische Funktion parts_pn bereits implementieren (wir benutzen eine Kopie dieses Set, weil er von parts_pnset zerstört wird):
Pnset parts_pn (Plist plist, Pn pn)
*
{ return parts_pnset(plist, copy1_pnset(sel_plist(plist, pn))); }
*[1.5ex]
parts_pnset Nun geht es darum, die Funktion parts_pnset zu spezifizieren. In jedem Rekursionsschritt wird zu dem Set ps, der als Argument übergeben wird, der Set ps_sub der direkten Bestandteile aller Elemente von ps ermittelt. Enthält dieser Set ps_sub ein Teil, das nicht in ps enthalten ist, wird die Funktion (mit der Vereinigung von ps und ps_sub als Argument) erneut aufgerufen; ist ps_sub aber vollständig in ps enthalten, sind wir fertig und ps enthält das Ergebnis. Die konstruktive VDM-Spezifikation von parts_pnset sieht demzufolge so aus:
TYPE parts_pnset(ps, plist):PnsetPlist
Pnset
*
pre: 
*
parts_pnset =
*
if subparts_pnset 
*
then ps
*
else parts_pnset(subparts_pnset 
*[1.5ex]
Das können wir gleich in C implementieren:
Pnset parts_pnset (Plist plist, Pnset ps)
*
{
*
Pnset ps_sub = copy1_pnset(ps);
ps_sub = subparts_pnset(ps_sub, plist);
*
if (is_subset_pnset(ps_sub, ps)) {
*
del1_pnset(ps_sub);
*
return ps;
*
}
else {
*
ps = union_pnset(ps, ps_sub);
*
return parts_pnset(plist, ps);
*
}
*
}
*[1.5ex]
Zunächst wird die Variable 
erzeugt, indem das Argument, ps,
kopiert wird (copy1_pnset), weil wir ihn später noch brauchen. Nun
wird der Set aller direkten Bestandteile aller in ps_sub
befindlichen Teile ermittelt (subparts_pnset) und wieder in
gespeichert. Ist eine Teilmenge des Arguments ps
(sind also keine neuen Teile hinzugekommen, ermittelt mit
is_subset_pnset), braucht nur noch ps_sub wieder gelöscht zu werden
(del1_pnset) und die Funktion ist beendet. Wenn nicht, wird das
Argument ps mit vereinigt (union_pnset) und
parts_pnset erneut aufgerufen.
subparts_pnset Noch sind wir nicht fertig: die neu eingeführte Hilfsfunktion subparts_pnset muß noch realisiert werden. Sie ermittelt die Vereinigung der Bestandteil-Sets aller Teile im ihr übergebenen Set. Für solche Operationen, die man mit dem Begriff ,,Für alle`` charakterisieren kann, ist häufig das Funktional fold geeignet; so auch hier. Die Nullfunktion muß einen leeren Pnset-Set liefern, dafür ist mk_empty_pnset geeignet; die Fold-Funktion vereinigt zwei Sets, dafür taugt union_pnset; die Konvertierungsfunktion wandelt ein Element des Set in den Resultattyp um, ermittelt also zu einem Teil die direkten Bestandteile mit Hilfe der Stückliste. Siehe da: die Konvertierungsfunktion benötigt Zugriff auf die Stückliste! Wir benötigen also für die mit fold erzeugte Funktion subparts_pnset ein zusätzliches Argument, die Stückliste, die der Konvertierungsfunktion übergeben wird. Der Typ dieses Arguments muß in der Implementations-Beschreibung von Pnset in der Parameterliste von fold auftauchen, und zwar mit dem Parameter X als erstem zusätzlichen Argument der Konvertierungsfunktion.
IMPLEMENTATIONS
*
Pnset= ¯...
*
+ fold.subparts(RESULT=
"Pset",
*
CVFCT="getparts",
*
NULLFCT="mk_empty",
*
FOLDFCT="union",
*
X="Plist")
*
getparts Die als Konvertierungsfunktion angegebene Funktion getparts müssen wir natürlich auch noch definieren; außerdem brauchen wir ihren ,,richtigen`` Namen, nach der Erweiterung. Er lautet getparts_pn:
Pnset getparts_pn (Pn pn, Plist plist)
*
{ return copy1_pnset(sel_plist(plist, pn)); }
*[1.5ex]
Sie liefert eine Kopie des Set der Bestandteile des Teils pn, weil die Fold-Funktion der Funktion subparts_pnset ihre Argumente zerstört und wir die Stückliste plist später noch brauchen.
Zum Abschluß sehen Sie die fertige, mit fold generierte Funktion subparts_pnset, die Sie nicht selbst zu schreiben brauchen (sie wird ja vom VDM-Compiler generiert):
Pnset subparts_pnset (Pnset ps, Plist plist)
*
{
*
Pn pn;
*[0.5ex]
if (is_empty_pnset(ps))
*
return mk_empty_pnset();
*
else {
*
pn = sel_pnset(ps);
*
return union_pnset(getparts_pn(pn, plist),
*
subparts_pnset(sub1_pnset(ps, pn)));
*
}
*
}
*
In diesem Abschnitt wird eine konventionelle Heap-Verwaltung in C einer Heap-Verwaltung mit Hilfe einer Map von Pointern (Token) auf Objekte gegenübergestellt. Wir wollen hier der Einfachheit halber nur Zahlen auf dem Heap manipulieren; das Prinzip läßt sich aber auch auf komplexe Datentypen anwenden. Zunächst die DSL-Spezifikation:
DOMAINS
*
Heap=Token
Nat0
*
Token = ELEMENTARY
*
IMPLEMENTATIONS
*
Heap = heap
*
+ mk_empty + union1 + sub1 + sel + ovwrt1 + ext
*
Token = ptr(ELEM=Nat0) + del + ...
*[1ex]
In C:
*
#typedef Nat0 Adr;
Token ist also der Typ der ,,Pointer auf Nat0``; Heap ordnet diesen Pointern Werte des Typs Nat0 zu. In C wird der Typ Adr als Pointer auf Nat0 vereinbart.
Die Map hat einen Nachteil: die Operationen haben die bei Maps übliche Syntax (benötigen also eine Map als Argument), obwohl das eigentlich unnötig ist: die Paare der Map sind ja nicht irgendwie zusammengefaßt unter einem Namen ansprechbar. Der Grund dafür ist allerdings einleuchtend: wenn Ihnen die Arbeit mit Heap-Objekten und die notwendige Speicherverwaltung einmal zu gefährlich, zu schwierig oder zu unübersichtlich wird, können Sie problemlos eine andere Map-Implementation auswählen, denn Ihr Programm enthält bereits alle Operationsaufrufe mit der korrekten Syntax, Sie haben bereits ein Map-Objekt eingerichtet usw. Die Initialisierung der Map sieht also so aus:
Heap h = mk_empty_heap();
*[0.5ex]
Beachten Sie, daß dieses Objekt ,,virtuell`` ist, denn es belegt keinen Speicher, stört Sie im Programm also nicht weiter.
Die üblichen Heap-Operationen werden nun einander gegenübergestellt.
Objekt erzeugen In C erzeugen Sie ein Objekt auf dem Heap, indem Sie Speicher anfordern; dazu rufen Sie die Standard-Funktion malloc mit der Größe des Objekttyps als Parameter auf und wandeln den Ergebnispointer in den Typ Token um. Danach initialisieren Sie das Objekt mit Hilfe einer Dereferenzierung. Bei der Map rufen Sie die Operation ext auf, die genau das gleiche durchführt, was Sie in C ,,per Hand`` machen. In einer anderen Implementation würden Sie die Operation union1 verwenden, da der Argumentwert dann ja von Ihnen bestimmt wird und nicht dynamisch von malloc ermittelt wird.
Adr c1;
*
Token m1;
*
c1 = (Token) malloc(sizeof(Nat0)); c1 = 14;
*[0.5ex]
m1 = ext_heap(&h, 14);
*[1.5ex]
Objekt löschen In C löschen Sie ein Objekt auf dem Heap, indem Sie den Speicher wieder freigeben (mit free) und danach den Pointer sicherheitshalber löschen. Bei der Map entfernen Sie das Objekt mit sub1, nachdem Sie es mit del gelöscht haben. sub1 ist nur nötig, wenn Sie den Austausch der Implementation erwägen.
free((void ) c1);c1 = NULL;
*
del_token(m1);h = sub1_heap(h,m1);
*[1.5ex]
Auslesen Zum Auslesen des Heap-Objekts in C dereferenzieren Sie den Pointer; bei der Map verwenden Sie die Operation sel.
printf("\n%d %d", c1, sel_heap(h, m1));
*[1.5ex]
Überschreiben In C weisen Sie dem dereferenzierten Pointer (der dadurch mit dem Objekt identisch wird) einen neuen Wert zu. Bei der Map verwenden Sie die Operation ovwrt1 mit einem bereits initialisierten Token und dem neuen Inhalt.
c1 = 9;h = ovwrt1_heap(h,m1,9);
*[1.5ex]
Sie sehen: der Unterschied ist nicht sehr groß und der kleine Mehraufwand sollte für den Fall, daß die Performance nicht die größte Rolle spielt, in Kauf genommen werden. Die Implementation ``heapmap`` z.B. ist der Implementation ,,heap`` sehr ähnlich -- allerdings werden die Argumentwerte in einem Set gehalten, so daß alle Map-Operationen zur Verfügung stehen, ohne daß die Performance der obigen Heap-Operationen wesentlich schlechter wird.
VDM Class Library