TREE (tree)
Die Operationen der ADT
OPTIONAL (opti)
TREE (tree)
Die Operationen der ADT
OPTIONAL (opti)
func1binary(func2)
#typedef Domain func1(Domain,Domain)
#typedef Domain func2(Domain,Element)
Funktional
Der Name der Argument-Funktion wird mit dem Implementationsparameter FOLDFCT festgelegt; dient zur Realisierung von Funktionen mit zwei Sets als Argumenten, die wieder einen Set liefern, mit Hilfe von Funktionen mit einem Set und einem Element als Argumenten.
Beispiel: union = binary(FOLDFCT=,,union1``))
Nat0card(Domain x1)
Kardinalität (Anzahl der Elemente) des Set x1
Domaindiff(Domain x1,Domain x2)
Set-Differenz: aus dem Set x1 werden alle Elemente, die auch in x2 enthalten ist, entfernt
x1 wird zerstört
Domaindiffd(Domain x1,Domain x2)
Set-Differenz: aus dem Set x1 werden alle Elemente, die auch in x2 enthalten ist, entfernt und dabei mit del gelöscht
x1 wird zerstört
funcfold(func1,func2,func3)
#typedef Result func(Domain,x1,...,xn)
#typedef Result func1(Element,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: Distributive Vereinigung der Elemente eines Set von Sets
DOMAINS
*
Set1 = E1 -set
*
Set2 = Set1 -set
*
IMPLEMENTATIONS
*
Set2 = ...+ fold.dunion(NULLFCT=,,mk_empty``, FOLDFCT=,,union``)
*
voidforall(Domain x1,proc x2)
#typedef void proc(Element)
Für alle Elemente im Set x1 wird die Prozedur x2 ausgeführt
voidforsome(Domain x1,predicate x2,proc x3)
#typedef Bool predicate(Element)
#typedef void proc(Element)
Für alle Elemente a im Set x1, für die das Prädikat x2(a) erfüllt ist, wird die Prozedur x3 ausgeführt
Domaininters(Domain x1,Domain x2)
Der Durchschnitt der beiden Sets x1 und x2 wird geliefert
x1 und x2 werden zerstört
Domainintersd(Domain x1,Domain x2)
Der Durchschnitt der beiden Sets x1 und x2 wird geliefert
Die nicht im Resultat enthaltenen Elemente werden mit del gelöscht
x1 und x2 werden zerstört
Boolis_empty(Domain x1)
Test auf leeren Set
Boolis_in(Element x1,Domain x2)
Test, ob das Element x1 im Set x2 enthalten ist
Boolis_subset(Domain x1,Domain x2)
Test, ob der Set x1 im Set x2 enthalten ist
Domainmk_empty(void)
Der leere Set wird geliefert
Domainmk_one(Element x1)
Der einelementige Set { x1 } wird geliefert
Elementsel(Domain x1)
Irgendein Element des Set x1 wird geliefert
Domainsub1(Domain x1,Element x2)
Das Element x2 wird aus dem Set x1 entfernt
x1 wird zerstört
Domainsub1d(Domain x1,Element x2)
Das Element x2 wird aus dem Set x1 entfernt; war es tatsächlich vorhanden, wird es mit del gelöscht
x1 wird zerstört
Domainunion(Domain x1,Domain x2)
Vereinigung zweier Sets
x1 und x2 werden zerstört
Domainunion1(Domain x1,Element x2)
Das Element x2 wird in den Set x1 eingetragen
x1 wird zerstört
Domainunion1d(Domain x1,Element x2,Element2 x3)
Das Element x2 wird in den Set x1 eingetragen; ist x2 bereits in x1 enthalten, wird es mit del gelöscht
x1 wird zerstört
Domainuniond(Domain x1,Domain x2)
Vereinigung zweier Sets; ist ein Element in beiden Maps enthalten, wird eines davon mit del gelöscht
x1 und x2 werden zerstört
VDM Class Library