Softwaredesign: Semantik von Entwürfen mit UML/OMT

Semantik	Klassendiagramme besitzen, im Gegensatz zu Programmiersprachen, keine formale Semantik

	nur die Signaturen tauchen (zum Teil) in Klassendiagrammen auf

	Eigenschaften und Verhalten bleiben offen

	keine Vor- und Nachbedingungen keine Invarianten (wie z.B. in Eiffel)

	zusätzliche Notation notwendig häufig Pseudocode oder OO-Programmiersprache

	Fehlererkennung und Behandlung bleibt offen

	Test-Methoden werden nicht unterstützt

Semantik	präzise definiert

	Eigenschaften des Systems werden eindeutig festgelegt

	Vor- und Nachbedingungen Invarianten für Konsistensbedingungen Fehlersituationen

	ein Programm kann gegen die Spezifikation getestet werden

ADTs	die Gesetze einer ADT-Definition bilden Basis für einen systematischen black-box Text

Datenmodellierung	fester Satz von ADTs Verbund, Listen, Mengen, Tabellen, Relationen, Graphen, ...
	jeder ADT besitzt formale Semantik

Z!	entwickelt von C.A.R. Hoare
	alle ADTs werden auf Mengen zurückgeführt

VDM	entwickelt von Bjørner und Jones
	ADTs für Verbund, Vereinigung, Liste, Menge und Tabelle vorgegeben andere ADTs werden aus diesen zusammengesetzt

Haskell	1-1-Umsetzung der abstrakten Syntax aus VDM in eine ausführbare Notation möglich
	ausführbare Spezifikationen
	rapid prototyping

Datenmodell	aus Basis-Datentypen und Kombination der ADTs
	abstrakte Syntax

Invarianten	Konsistenzbedingungen an das Datenmodell
	Basis-Operationen im Datenmodell durch ADTs festgelegt

Funktionen	problemspezifische Operationen

Definition
	durch Eigenschaften: Vor- und Nachbedingungen z.B. in Z! (Hoare)
	funktional: Zustandslose Beschreibung leichter manipulierbar als mit imperativen Modellen
	Zustandsorientiert

elementare Wertebereiche
Zahlen	natürliche ganze reelle Zahlen
	aus der Mathematik übernommen
Char	aus Programmiersprachen übernommen

Aufzählungsbereiche	data Enum = V₁ \| V₂ \| ... \| V_n

strukturierte Wertebereiche	für
	Verbund (Paare, Triple, n-Tupel) Vereinigung Option (Maybe) Summe (Either) Liste ([...]) Menge (Set) Tabelle (Map)

Liste	type L = [E]
Operationen	null, head, tail, length, ++, ==, ...

	OMT:

Menge	type S = Set E
Operationen	union, intersection, include, in, =, ...

	OMT:

Tabelle map dictionary assoziatives array	type Map = Map K A
Operationen	Mengenoperationen einfügen, überschreiben, suchen, selektieren

	OMT:

Verbund record kartesisches Produkt	type Tuple = (Comp₁, ... , Comp_n)
Operationen	Konstruktion, Selektion, Vergleich

	OMT:

Vereinigung	date Sum = Constr₁ ... \| ... \| Constr_n ...
Operationen	Test auf Gleichheit, Bereichstest, ...

	OMT:

Semantik von Entwürfen mit UML/OMT