OPTIONAL (opti)

ELEMENTARY (elem)

MAP (map)

Die Implementation ,,heap`` enthält nur sehr wenige Operationen; diese sind explizit gekennzeichnet.

func1binary(func2)

#typedef Domain func1(Domain,Domain)

#typedef Domain func2(Domain,Element1)

Funktional

Der Name der Argument-Funktion wird mit dem Implementationsparameter FOLDFCT festgelegt; dient zur Realisierung von Funktionen mit zwei Maps als Argumenten, die wieder eine Map liefern, mit Hilfe von Funktionen mit einer Map und einem Argumentwert als Argumenten.

Beispiel: ovwrt = binary(FOLDFCT=,,ovwrt1``))

Nat0card(Domain x1)

Kardinalität (Anzahl der Paare) der Map x1

Element1ext(Domain x1,Element2 x2)

Die Map x1 wird um ein Paar ( random x2 ) erweitert; der (zufällig) ermittelte Argumentwert wird zurückgeliefert, die Map ist Referenz-Parameter

x1 wird verändert

NUR in den Implementationen ``heapmap`` und ,,heap`` vorhanden

funcfold(func1,func2,func3)

#typedef Result func(Domain,x1,...,xn)

#typedef Result func1(Element1,Element2,x1,...,xk)

#typedef Result func2(void)

#typedef Result func3(Result,Result,x1,...,xn)

Funktional

Die Namen der drei Argument-Funktionen werden mit den Implementationsparametern CVFCT, NULLFCT und FOLDFCT festgelegt, der Resultattyp mit dem Parameter RESULT. Die x1,...,xn stellen zusätzliche optionale Parameter dar, die an func1 bzw. func3 übergeben werden; ihre Datentypen können mit den Implementationsparametern X, XX und XXX für func1 sowie Y, YY, YYY, Z, ZZ und ZZZ für func3 definiert werden. Die genaue Spezifikation können Sie mit vdminfo ermitteln.

Beispiel: Invertieren einer Map mit inverse, wenn sie bijektiv ist.

 Hilfsfunktion: 
 *
swap_e1_e2(x1,x2) = [ ( x2    x1 ) ] 
 *
TYPE: Elem1Elem2    Map2 
 *[0.5ex]
DOMAINS 
 *
Map1 = E1 -m-> E2 
 *
Map2 = E2 -m-> E1 
 [0.5ex]
IMPLEMENTATIONS
 *
Map1 = ...
 *
+ fold.inverse(RESULT=127Map2127, 
 *
		CVFCT=,,swap``, 
 *
		NULLFCT=,,mk_empty``, 
 *
		FOLDFCT=,,union``) 
 *

voidforall(Domain x1,proc x2)

#typedef void proc(Element1,Element2)

Für alle Paare in der Map x1 wird die Prozedur x2 ausgeführt

Ist die Map geordnet, werden die Objekte in dieser Reihenfolge verarbeitet.

voidforrange(Domain x1,proc x2,Element1 x3,Element1 x4)

PRECONDITION: Für den ADT Element1 muß eine Relation existieren!

#typedef void proc(Element1,Element2)

Für alle Paare ( a b ) in der Map x1 mit wird die Prozedur x2 ausgeführt

voidforsome(Domain x1,predicate x2,proc x3)

#typedef Bool predicate(Element1)

#typedef void proc(Element1,Element2)

Für alle Paare ( a b ) in der Map x1, für die das Prädikat x2(a) erfüllt ist, wird die Prozedur x3 ausgeführt

Domainfread(Str x1)

PRECONDITION: (Arg-Dom = Str) (Co-Dom hat Operation fread )

Eine Map wird aus dem Verzeichnis x1 des Datei-Systems gelesen -- jede Datei repräsentiert ein Paar ( Dateiname Tuple ), jedes Unterverzeichnis ein Paar ( Verzeichnisname Map )

Bei einem Fehler wird die leere Map zurückgeliefert!

Boolfwrite(Domain x1,Str x2)

PRECONDITION: Arg-Dom = Str Co-Dom kennt Operation fread

Eine Map x1 wird in das Verzeichnis x2 des Datei-Systems geschrieben -- jede Datei repräsentiert ein Paar ( Dateiname Tuple ), jedes Unterverzeichnis ein Paar ( Verzeichnisname Map )

Bei einem Fehler wird FALSE zurückgeliefert, sonst TRUE

Domaininters(Domain x1,Domain x2)

Der Durchschnitt der beiden Maps x1 und x2 wird geliefert

x1 und x2 werden zerstört, Sub-Strukturen allerdings nicht!

Domainintersd(Domain x1,Domain x2)

Der Durchschnitt der beiden Maps x1 und x2 wird geliefert Sämtliche Sub-Strukturen, die nicht im Resultat enthalten sind, werden mit del gelöscht.

x1 und x2 werden zerstört

Boolis_empty(Domain x1)

Test auf leere Map

Boolis_in(Element1 x1,Domain x2)

Test, ob das Element x1 in der Argumentmenge der Map x2 enthalten ist

Boolis_in_dom(Element1 x1,Domain x2,Element2 x3)

Test, ob das Element x1 in der Argumentmenge der Map x2 enthalten ist; wenn ja, wird der zugehörige Map-Wert im Referenzparameter x3 zurückgegeben

x3 wird verändert

Boolis_in_max(Element1 x1,Domain x2,Element2 x3)

Test, ob es ein Paar ( a b ) mit gibt; wenn ja, wird das b mit dem maximalen a im Referenzparameter x3 gespeichert

x3 wird verändert

Boolis_in_min(Element1 x1,Domain x2,Element2 x3)

Test, ob es ein Paar ( a b ) mit gibt; wenn ja, wird das b mit dem minimalen a im Referenzparameter x3 gespeichert

x3 wird verändert

Boolis_in_rng(Element2 x1,Domain x2,Element1 x3)

Test, ob x1 im Co-Domain der Map x2 existiert; wenn ja, wird der zugehörige Argumentwert im Referenzparameter x3 gespeichert

x3 wird verändert

Boolis_submap(Domain x1,Domain x2)

Test, ob die Map x1 in der Map x2 enthalten ist

Domainmk_empty(void)

Die leere Map wird geliefert

In der Implementation ,,heap`` vorhanden

Domainmk_one(Element1 x1,Element2 x2)

Die einelementige Map [ ( x1 x2 ) ] wird geliefert

Domainovwrt(Domain x1,Domain x2)

Die Map x2 wird mit der Map x1 vereinigt; bei Argumentwerten, die in beiden Maps existieren, wird das Paar aus x2 genommen

x1 und x2 werden zerstört

Domainovwrt1(Domain x1,Element1 x2,Element2 x3)

Das Paar [ x2 x3 ] wird in die Map x1 eingetragen -- war is_in(x1,x2) erfüllt, wird das alte Paar überschrieben

x1 wird zerstört

In der Implementation ,,heap`` vorhanden

Domainovwrt1d(Domain x1,Element1 x2,Element2 x3)

Das Paar [ x2 x3 ] wird in die Map x1 eingetragen -- ist x2 bereits in der Argumentmenge der Map enthalten, wird das alte Paar mit del gelöscht

x1 wird zerstört

Domainovwrtd(Domain x1,Domain x2)

Die Map x2 wird mit der Map x1 vereinigt; bei Argumentwerten, die in beiden Maps existieren, wird das Paar aus x2 genommen und das entsprechende Paar aus x1 mit del gelöscht

x1 und x2 werden zerstört

Element2sel(Domain x1,Element1 x2)

PRECONDITION: is_in(x1,x2) = TRUE

Der x2 zugeordnete Map-Wert wird geliefert

In der Implementation ,,heap`` vorhanden

Element1sel_dom(Domain x1)

PRECONDITION: x1 []

Irgendein Argumentwert der Map x1 wird geliefert

Domainsub(Domain x1,Domain x2)

Subtraktion zweier Maps: aus der Map x1 werden alle Paare, deren Argumentwert auch in x2 enthalten ist, entfernt

x1 wird zerstört

Domainsub1(Domain x1,Element1 x2)

Das Paar ( x2 sel(x1,x2) ) wird aus der Map entfernt

x1 wird zerstört

In der Implementation ,,heap`` vorhanden

Domainsub1d(Domain x1,Element1 x2)

Das Paar [ x2 sel(x1,x2) ] wird aus der Map entfernt und, wenn es tatsächlich enthalten war, mit del gelöscht

x1 wird zerstört

Domainsubd(Domain x1,Domain x2)

Subtraktion zweier Maps: aus der Map x1 werden alle Paare, deren Argumentwert auch in x2 enthalten ist, entfernt

Alle nicht weiter verwendeten Sub-Strukturen von x1 werden mit del gelöscht

x1 wird zerstört

Domainunion(Domain x1,Domain x2)

PRECONDITION: ( i dom x1 dom x2)(x1(i) = x2(i))

Vereinigung zweier Maps

x1 und x2 werden zerstört

Domainunion1(Domain x1,Element1 x2,Element2 x3)

PRECONDITION: is_in(x1,x2) sel(x1,x2) = x3

Das Paar ( x2 x3 ) wird in die Map x1 eingetragen

x1 wird zerstört

In der Implementation ,,heap`` vorhanden

Domainunion1d(Domain x1,Element1 x2,Element2 x3)

PRECONDITION: is_in(x1,x2) sel(x1,x2) = x3

Das Paar ( x2 x3 ) wird in die Map x1 eingetragen; ist das gleiche Paar bereits in der Map enthalten, wird ein Paar gelöscht

x1 wird zerstört

Domainuniond(Domain x1,Domain x2)

PRECONDITION: ( i dom x1 dom x2)(x1(i) = x2(i))

Vereinigung zweier Maps; wenn ein Paar in beiden Maps enthalten ist, wird eines davon mit del gelöscht

x1 und x2 werden zerstört

OPTIONAL (opti) Die Operationen der ADT ELEMENTARY (elem)

VDM Class Library