Tuples Die VDM-Basistypen Elementare Datentypen

Sets

 

Was ist ein Set ?

Definition Ein Set  ist eine endliche, ungeordnete Sammlung von unterschiedlichen, aber dennoch gleichartigen Objekten. Etwas ausführlicher:

Mit diesen Eigenschaften ähnelt ein Set einer mathematischen Menge; diese jedoch kann auch unendlich groß sein (wie z.B. die Zahlenmengen). Die Beschränkung auf endliche Sets ist jedoch im Rahmen der Anwendung in der Programmierung vernünftig. Mathematische Mengen sind grundsätzlich ebenfalls ungeordnet, auch wenn die Zahlenmengen ein Ordnungprinzip aufzuweisen scheinen; dies ist jedoch den Objekten (Zahlen) immanent -- Punktmengen sind zum Beispiel ungeordnet.

DSL Um in der DSL-Spezifikation einen Set Aset von Objekten eines Domains  tex2html_wrap_inline6370 zu definieren, schreiben Sie

displaymath1613

Anwendung Sie können Sets also einsetzen, wenn Sie Sammlungen von Objekten modellieren möchten, die ungeordnet sind und deren Elemente alle verschieden sind; außerdem sollte die Manipulation eines Sets auf dem Hinzufügen, Entfernen und (zufälligem) Auswählen von Objekten basieren.

Beispiel: Ein kleines Beispiel soll den Einsatz von Sets verdeutlichen: eine Schule besteht aus mehreren verschiedenen Klassen und in jeder Klasse sind verschiedene Schüler. Eine Klasse bildet demzufolge einen Set von Schülern, eine Schule ist ein Set von Klassen. Mehr noch: natürlich bildet auch die Schule einen Set von Schülern, der die gleiche Größe und die gleichen Elemente hat wie die Vereinigung aller Klassen. Die Anzahl der Schüler ist immer endlich und sie unterliegen keinem immanenten Ordnungssystem, also ist die Repräsentation durch Sets gerechtfertigt. Sie können also folgendes modellieren:

 School=Class -set 
 *
Class		=Student -set

Die Tatsache, daß auch Schulen Sets von Schülern sind, wird hiermit noch nicht wiedergegeben. Dazu könnten Sie einen weiteren Set Schoolofstudents einführen: um eine Schule als Set von Schülern zu betrachten, benötigen Sie dann eine Funktion, die ein Objekt School in ein äquivalentes Objekt des Typs Schoolofstudents überführt.

Während der Erläuterung der Operationen werden Sie diesen Domains immer wieder begegnen.

Set-Implementation

Zur Zeit gibt es für Sets nur die Implementation linklist . Sie wird auch für andere VDM-Basistypen verwendet; ihre Charakteristika finden Sie dort oder im Anhang C.

Set-Operationen

Zur Veranschaulichung der Operationen dienen folgende Variablen:

 Schools1, s2; 
 *
Class		c1, c2; 
 *
Student		st1, st2;

Set-Konstruktoren

VDM bietet Ihnen vier Operationen zur Erzeugung von Set-Objekten:

mk_empty Mitmk_emptyerzeugen Sie einen neuen, leeren Set.
* Beispiel -- Gründung einer Schule:

s1 = mk_empty_school();
*[1.5ex]

mk_oneMitmk_oneerzeugen Sie einen neuen, ein-elementigen Set.
* Beispiel -- Eröffnung einer Klasse mit folgender Gründung einer Schule, die diese eine Klasse umfaßt:

c1 = mk_empty_class();
* s2 = mk_one_school(c1);
*[1.5ex]

copy / copy1 copy und copy1 haben Sie ja bereits kennengelernt -- diese Operationen stehen für alle strukturierten Typen zur Verfügung.

Set-Kombinatoren

union Die Vereinigung zweier Sets ( s1 tex2html_wrap_inline7100 s2 ) heißtunionund enthält alle Elemente, die in einem der beiden Sets enthalten sind. Es gibt häufig den Wunsch, dem Set genau ein Objekt hinzuzufügen, also einen ein-elementigen Set. Um nun nicht den Umweg über die Erzeugung eines solchen Set gehen zu müssen, gibt es dafür die union1 Operation union1.
* Beispiel -- das Hinzufügen einer Klasse zu einer Schule läßt sich auf zwei Weisen darstellen:

union1_school(s1,c1) tex2html_wrap_inline6455 union_school(s1,mk_one_school(c1))
*[1ex]

Zusätzlich gibt es die Versionen uniond und union1d mit implizitem Löschen.

inters Der Durchschnitt zweier Sets ( s1 tex2html_wrap_inline7104 s2 ) heißtintersund enthält die Elemente, die in beiden Sets enthalten sind. intersdlöscht implizit.
* Beispiel -- der Durchschnitt zweier Schulen ist natürlich leer, da keine Klasse zu zwei Schulen gehören kann:

is_empty_school(inters_school(s1,s2)) == TRUE
*[1.5ex]

diff Die Set-Subtraktion ( s1 \ s2 ) heißtdiffund enthält alle Elemente, die im ersten, aber nicht im zweiten Set enthalten sind. Auch hier gibt es eine Vereinfachung, wenn Sie nur ein Element aus einem Set entfernen möchten: sub1 sub1. Hinzu kommen diffd und sub1d, die implizit löschen.
Beispiel -- eine Klasse in einer Schule wird geschlossen:

s1 = sub1_school(s1,c1);oder
* s1 = diff_school(s1,mk_one_school(c1));
*[1.5ex]

Set-Prädikate

is_eq Mitis_eqtesten Sie die Gleichheit zweier Sets, d.h. ob sie die gleiche Kardinalität (Element-Anzahl) haben und die gleichen Elemente enthalten.
Beispiel -- zwei Schulen haben nie die gleichen Klassen:

is_eq_school(s1,s2) == FALSE
*[1.5ex]

is_empty Mitis_emptytesten Sie, ob ein Set gerade keine Elemente enthält.
Beispiel -- eine neugegründete Schule hat zunächst keine Klassen:

is_empty_school(mk_empty_school()) == TRUE
*[1.5ex]

is_in Mitis_in können Sie testen, ob ein bestimmtes Element in einem Set enthalten ist ( c1 tex2html_wrap_inline6465 s1 ).
Beispiel -- ist ein bestimmter Schüler in einer bestimmten Klasse ?

if (is_in_class(st1,c1)) ...
*[1.5ex]

is_subset Mit is_subset können Sie testen, ob alle Elemente eines Set auch in einem anderen Set des gleichen Typs enthalten sind (Teilmengen-Beziehung, c1 tex2html_wrap_inline6471 c2 ).
Beispiel -- die Schüler einer Klasse sind nie vollständig auch in einer anderen Klasse:

is_subset_class(c1,c2) == FALSE
*[1ex]

Der leere Set ist in jedem anderen Set enthalten:

is_subset_xxx(mk_empty_xxx(),xxx) == TRUE
*

Set-Attribute

card Die Kardinalität eines Set, d.h. die aktuelle Anzahl von Elementen, liefert Ihnencard. Der leere Set hat die Kardinalität 0.
Beispiel -- Ermittlung der Schülerzahl in einer Klasse:

printf("%d",card_class(c1));
*[1ex]

Selektion in einem Set

sel Mitselwählen Sie zufällig ein Element eines nicht-leeren Set aus.
* Beispiel -- Auslosung des Klassensprechers in einer Schulklasse:

st1 = sel_class(c1);
*[1.5ex]

Set-Funktionale

 

Zur Erzeugung neuer, komplexer Funktionen mit Hilfe der vorhandenen gibt es zwei Funktionale , das sind Funktionen, die wieder Funktionen zurückliefern. In der DSL-Spezifikation geben Sie dazu den Namen des Funktionals, gefolgt von einem Punkt und dem Namen der zu erzeugenden Funktion an. Wie üblich folgen dann in Klammern die Parameter des Funktionals.

binary Mitbinarykönnen binäre Funktionen, die aus einem Set und einem Element einen neuen Set erzeugen, verallgemeinert werden zu Funktionen, die aus zwei Sets einen neuen Set erzeugen und dabei ihre Argumente zerstören. Eine mit binary erzeugte Funktion arbeitet wie folgt:

Aset newfct_aset (Aset s1, Aset s2)
* {
* Elem e;
*[0.5ex] if (is_empty_aset(s2))
* return s1;
* else {
* e = sel_aset(s2);
* return newfct_aset(foldfct_aset(s1,e), sub1_aset(s2,e)) ;
* }
* }
*[1.5ex]

foldfct ist die Funktion, die binary als Parameter übergeben wurde. Sie hat zwei Argumente, einen Set und ein Element, und liefert wieder einen Set; Sie legen sie in der DSL-Spezifikation mit dem Parameter Parameter ,,FOLDFCT`` fest. Für die Funktion newfct_aset sieht das so aus:

IMPLEMENTATIONS
* ...+ binary.newfct(FOLDFCT="foldfct")
*[1.5ex]

Nomenklatur Beachten Sie, daß sowohl der Name der erzeugten Funktion (newfct) als auch der Name der Parameterfunktion (foldfct) als generische Namen aufgefaßt werden; sie werden mit dem zugehörigen Set-Namen erweitert. Falls Sie also eine selbstdefinierte Funktion als Parameterfunktion einsetzen möchten, geben Sie ihr den richtigen Namen! Im ADT-Implementations-Modul wird dann eine Funktion ähnlich der obenstehenden erzeugt; damit es auch compiliert werden kann, wird in der Header-Datei für die Parameterfunktion eine Deklaration eingetragen.

Beispiel -- die Operation union kann mit Hilfe von binary und union1 definiert werden:

IMPLEMENTATIONS
* ...+ binary.union(FOLDFCT="union1")
*[4ex]

fold Das Funktionalfoldist wesentlich komplexer: es hat drei Parameter-Funktionen und erzeugt eine Funktion, die einen Set auf einen durch die Parameter-Funktionen festgelegten Resultattyp abbildet. Damit lassen sich sehr gut komplexe Manipulationen aller Elemente einer Menge realisieren. Die Parameter-Funktionen haben folgende Bedeutung:

  1. Parameter Die Konvertierungsfunktion (CVFCT) bildet ein Element des Set auf den Resultattyp ab (ist das Resultat vom Elementtyp, kann diese Funktion wegfallen).
  2. Die Nullfunktion (NULLFCT) hat kein Argument und liefert konstant den Resultat-Wert für den leeren Set.
  3. Die Fold-Funktion (FOLDFCT) bildet zwei Werte des Resultattyps auf den Resultattyp ab.

In Klammern ist der jeweilige Parametername für die DSL-Spezifikation angegeben; hinzu kommt noch der optionale Parameter RESULT,,RESULT``, der den Resultattyp angibt für den Fall, daß es nicht der Elementtyp ist.

Die erzeugte Funktion sieht von der Struktur her wie folgt aus:

 Result newfct_aset (Aset s) 
 *
{ 
 *
Elem e; 
 *[0.5ex]
if (is_empty_aset(s)) 
 *
return nullfct_result(); 
 *
else { 
 *
e = sel_aset(s); 
 *
return foldfct_result(cvfct_elem(e), 
 *
		newfct_aset(sub1_aset(s,e))); 
 *
} 
 *
}

Die Verarbeitung ähnelt also strukturell dem Funktional binary, nur die Resultate werden auf komplexere Weise erzeugt.

Nomenklatur Die Namen der drei Parameterfunktionen und der erzeugten Funktion werden erweitert, wie Sie in der obigen Funktion sehen können:

Beispiel 1 Eine häufige Anwendung von fold ist die distributive Vereinigung aller Sets in einem Set von Sets, also z.B. die Zusammenlegung aller Klassen einer Schule zu einer neuen Klasse:

IMPLEMENTATIONS
* ...+ fold.d_union(NULLFCT="mk_empty", FOLDFCT="union")
* erzeugt
* Class d_union_school (School s)
*[1ex]

Da der Resultattyp hier identisch mit dem Elementtyp des Set school ist, braucht keine Konvertierungsfunktion angegeben zu werden, ebensowenig wie der Parameter ,,RESULT``.

Beispiel 2 Gelegentlich möchten Sie testen, ob entweder für alle Elemente eines Set ein bestimmtes Prädikat erfüllt ist oder ob es mindestens ein solches Element gibt. Dafür haben sich die folgenden Schreibweisen eingebürgert:

tex2html_wrap_inline7136
* tex2html_wrap_inline7138
*[1.5ex]

Mit fold können Sie beide Tests generieren; Sie benötigen dazu Operationen für den Datentyp Bool. ,,forall`` ist für den leeren Set erfüllt, ansonsten wird das Prädikat für jedes Element geprüft und die Resultate AND-verknüpft. ,,exists`` ist für den leeren Set nicht erfüllt, ansonsten werden die Resultate des Prädikats OR-verknüpft.

 fold.forall(RESULT="Bool", 
 *
		 CVFCT="Predicate", 
 *
		 NULLFCT="true", 
 *
		 FOLDFCT="and") 
 [1ex]
fold.exists		(RESULT="Bool", 
 *
		 CVFCT="Predicate", 
 *
		 NULLFCT="false", 
 *
		 FOLDFCT="or")

Der VDM-Compiler erkennt übrigens nicht, welche Standard-Operationen für irgendwelche mit binary oder fold definierte Funktionen notwendigerweise eingebunden werden müssen! Sie müssen sie also in Ihrer DSL-Spezifikation explizit anfordern, sonst erhalten Sie einen Fehler beim Binden, z.B.
* ,,undefined function mk_empty_class``.

Zusätzliche Parameter Manchmal benötigen die Parameterfunktionen ihrerseits noch weitere Argumente; vielleicht ist die Konvertierung eines Elements nur möglich, wenn Zusatzinformationen vorliegen. Die Erzeugung der Deklaration in der Header-Datei ist natürlich nur möglich, wenn der Typ dieser zusätzlichen Argumente bekannt ist; Sie geben dazu dem Funktional fold weitere Parameter: 

Beim Aufruf der erzeugten Funktion geben Sie die zusätzlichen Argumente in der entsprechenden Reihenfolge an, zuerst die mit den X..., danach die mit Y... und am Ende die mit Z... vereinbarten Argumente. Die Funktionsdeklaration sieht dann wie folgt aus:

 Result newfct_aset (Āset as,
 *
		X x1,
 *
		XX x2, ...,
 *
		Y y1, ..., 
 *
		ZZZ z3) 
 *

Eine Anwendung dafür finden Sie im Abschnitt 5.6 5.6 über Maps.

Set: Diverse Operationen

forall Mitforallwird für alle Elemente eines Set eine angegebene Prozedur ausgeführt, die das aktuelle Element als Argument erhält.
* Beispiel -- die klassenweise Ausgabe aller Schüler einer Schule mit der Ausgabe-Operation pr:

forall_school(s1,pr_class);
*[1.5ex]

forsome Mitforsomewird mit allen Elementen eines Set, die ein angegebenes Prädikat erfüllen (in Form einer Funktion mit bool-Resultat), eine Prozedur ausgeführt.
Beispiel -- die klassenweise Ausgabe aller Schüler einer Schule, wobei leere Klasssen automatisch unterdrückt werden:

forsome_school(s1,not_empty_class,pr_class);
*[0.5ex] Definition von not_empty_class:
*[0.5ex] Bool not_empty_class (class c)
* { return !is_empty_class(c) }
*[1.5ex]

Beispiel: ,,Coarsest Partitioning``

   

Wir haben beliebige, nicht-leere Sets gegeben, die nicht überschneidungsfrei sind. Daraus soll nun die ,,coarsest partitioning`` erzeugt werden -- die ,,gröbste Zerlegung`` dieser Sets, die aus nicht-leeren, aber überschneidungsfreien Sets besteht, bei minimaler Anzahl an Element-Sets. Sie sehen: die ,,coarsest partitioning`` ist kein selbständig definierter Begriff, sondern nur relativ zu einem Ausgangszustand definiert. Graphisch veranschaulicht diesen Vorgang Abb. 5.2.

  figure1777
Abbildung: Beispiel für Sets: das ,,coarsest partitioning``-Problem  

DSL Wir können bereits die DSL-Spezifikation für dieses Problem festlegen: ein Domain Aset mit beliebigen Elementen (in unserem Beispiel natürliche Zahlen), ein Domain Sset mit Elementen vom Typ Aset, also ein Set von Sets. In der Abbildung sind die Sets ss und cp vom Typ Sset, alle übrigen vom Typ Aset.

 DOMAINS 
 *[0.5ex]
Aset=Nat0 -set 
 *
Sset		=		Aset -set 
 *[0.5ex]
IMPLEMENTATIONS 
 *
Aset		=		linklist + ...
 *
Sset		=		linklist + ...
 *

Der Ablauf einer Zerlegung sieht folgendermaßen aus: solange noch Sets im Gesamt-Set vorhanden sind, deren Durchschnitt nicht-leer ist, wählen wir ein Paar solcher Sets (x,y) aus, entfernen sie aus dem Gesamt-Set (s\{ x,y }) und fügen diesem dann drei neue, nicht-leere Sets hinzu: (x \ y), (y \ x) und (x  tex2html_wrap_inline7104  y) -- falls einer dieser Sets leer ist, wird er ignoriert. Mit diesem neukonstruierten Gesamt-Set verfahren wir ebenso, bis er schließlich kein Paar sich überschneidender Sets mehr enthält. Der dabei entstehende Gesamt-Set ist die ,,coarsest partitioning`` des Ausgangszustands.

Spezifikation mit VDM Hier sehen Sie die VDM-Funktions-Spezifikation für eine semantische Funktion decompose zur Ermittlung der ,,coarsest partitioning`` unter Verwendung der VDM-Notation.

TYPE decompose (Ss):Sset tex2html_wrap_inline6488 Sset
* decompose =
* if ( tex2html_wrap_inline6479 x,y tex2html_wrap_inline6465 Ss) ((x tex2html_wrap_inline6483 y) tex2html_wrap_inline6445 (x tex2html_wrap_inline7104 y) tex2html_wrap_inline6483 {}))
* then (let {x,y} tex2html_wrap_inline6471 Ss be s.t. ((x tex2html_wrap_inline6483 y) tex2html_wrap_inline6445 (x tex2html_wrap_inline7104 y) tex2html_wrap_inline6483 {})) in
* decompose(({x\y , y\x , x tex2html_wrap_inline7104 y} tex2html_wrap_inline7100 Ss \ {x,y}) \ {})
* else Ss
*[1.5ex]

Sie lesen die VDM-Spezifikation folgendermaßen: ,,Für den Fall, daß es noch irgend zwei verschiedene Sets im Gesamt-Set gibt, die sich überschneiden, so wähle x und y so, daß sie zwei sich überschneidende Sets im Gesamt-Set darstellen und führe damit den Aufruf von decompose aus; sonst liefere den Gesamt-Set zurück``. Das Argument des rekursiven decompose-Aufrufs wird wie oben angegeben ermittelt -- beachten Sie: eine der beiden Set-Differenzen könnte leer sein, daher wird vom neukonstruierten Set Ss sicherheitshalber der leere Set subtrahiert.

Die semantische Funktion decompose_sset, die ein wohlgeformtes Objekt vom Typ Sset (das nicht-leer ist und nur nicht-leere Element-Sets enthält) in ihre ,,coarsest partitioning`` umwandelt, codieren wir nun in C:

  #define TRUE 1
* #define FALSE 0
* Sset decompose_sset (Sset ss)
* {
* Aset a1,a2,sav1,sav2;
* Sset ss1,ss2;
* Bool found = FALSE;
ss1 = copy1_sset(ss);
* while (!found && !is_empty_sset(ss1)) {
* a1 = sel_sset(ss1);
* ss1 = sub1_sset(ss1,a1);
* ss2 = copy1_sset(ss1);
* a2 = find_partner(ss2,a1);
* found = !is_empty_aset(a2);
* }
del1_sset(ss1);
* if (!found)
* return(ss);
else {
* ss = sub1_sset(ss,a1);
* ss = sub1_sset(ss,a2);
* sav1 = copy1_aset(a1);
* sav2 = copy1_aset(a2);
* ss = union1_sset(ss,inters_aset(sav1,sav2));
* sav1 = copy1_aset(a1);
* a1 = diff_aset(a1,a2);
* a2 = diff_aset(a2,sav1);
* del1_aset(sav1);
*[0.5ex] if (!is_empty_aset(a1))
* ss = union1_sset(ss,a1);
* if (!is_empty_aset(a2))
* ss = union1_sset(ss,a2);
* return(decompose_sset(ss));
* }
* }
*[1.5ex]

decompose_sset Zunächst müssen zwei Sets gesucht werden, die sich überschneiden. Dazu wird zunächst eine Kopie des Gesamt-Set angelegt (copy1_sset), danach solange ein Set dem Gesamt-Set entnommen (sel_sset und sub1_sset), bis mit Hilfe der Funktion find_partner (die ihr Argument zerstört, daher die Kopie in ss2), ein solches Paar gefunden wurde (found = TRUE) oder der Gesamt-Set leer ist (is_empty_sset). Im letzteren Fall ist man fertig.

Nachdem die while-Schleife verlassen wurde, ist ss2 zerstört, ss1 aber nicht. Der Aufruf von del1_sset sorgt dafür, daß kein Speicherplatz vergeudet wird. Wie Sie sehen, reicht die Kopie der Haupt-Struktur (mit copy1) aus, da die Sub-Strukturen nicht verändert werden.

Für den Fall, daß ein Paar sich überschneidender Sets existiert, ist es in den Variablen a1 und a2 gespeichert. Nun werden diese beiden Sets -- entsprechend dem oben geschilderten Ablauf -- aus dem Gesamt-Set entfernt (mit sub1_sset). Danach wird der garantiert nicht-leere Durchschnitt der beiden Sets, der mit inters_aset ermittelt wurde, eingefügt (mit union1_sset). Die beiden Differenz-Sets werden mit Hilfe von diff_aset erzeugt und in denselben Variablen abgelegt. Weil dabei der leere Set entstehen kann, wird mit is_empty_aset überprüft, ob eine Aufnahme in den Gesamt-Set erforderlich ist. Schließlich wird decompose_sset mit diesem veränderten Gesamt-Set rekursiv aufgerufen.

find_partner Die Hilfsfunktion find_partner erledigt die Suche nach einem Set, der mit dem Argument einen nicht-leeren Durchschnitt hat. Sie liefert bei Mißerfolg den leeren Set zurück; das ist sinnvoll, weil die Element-Sets per Definition nicht-leer sind!

Aset find_partner (Sset ss,Aset as)
* {
* Aset sav1,sav2;
* Aset ret;
*[0.5ex] if (is_empty_sset(ss))
* return(mk_empty_aset());
* else {
* ret = sel_sset(ss);
* ss = sub1_sset(ss,ret);
* sav1 = copy1_aset(as);
* sav2 = copy1_aset(ret);
*[0.5ex] if (!is_empty_aset(inters_aset(sav1,sav2))) {
* del1_sset(ss);
* return(ret);
* }
* else
* return(find_partner(ss,as));
* }
* }
*[1.5ex]

Auch find_partner ist eine rekursive Funktion: mit jedem Aufruf wird die Anzahl der Element-Sets im Gesamt-Set um eins kleiner -- ist kein Set mehr übrig, war die Suche erfolglos.

Bei jedem Aufruf wird dem Gesamt-Set ein Element-Set entnommen (mit sel_sset und sub1_sset) und überprüft, ob der Durchschnitt mit dem Argument-Set leer ist (mit is_empty_aset und inters_aset) -- wenn nicht, ist ein Paar gefunden und der Gesamt-Set muß ,,per Hand`` zerstört werden (explizit mit del1); wenn doch, wird find_partner rekursiv aufgerufen.

Tuples Die VDM-Basistypen Elementare Datentypen

VDM Class Library