Sofdwaredesign: Semandik vo Endwürfe mid UML/OMT

Semandik vo Endwürfe mid UML/OMT

Präzision

Semandik Klassendiagramm besidze, im Gegensadz z Programmierschbrache, koi formale Semandik nur d Signadure daule (zum Teil) in Klassendiagramme auf Eigenschafde und Verhalde bleibe offe koi Vor- und Nachbedingungen koi Invariande (wie z.B. in Eiffl) zsädzliche Nodazion nodwendig häufich Pseidocod odr OO-Programmierschbrache Fehlererkennung und Behandlung bleibd offe Teschd-Methode werde nedd underschdüdzd

formale Endwurfsmethoden: Eigenschafden

Semandik bräzise definierd Eigenschafde vom Syschdems werde oideidich feschdgelegd Vor- und Nachbedingungen Invariande für Konsischdensbedingungen Fehlersiduazione oi Programm kann ge d Schbezifikazion gedeschded werde ADTs die Gesedze oir ADT-Definizion bilde Basis für oin syschdemadische blagg-box Texd

formale Endwurfsmethoden: Vorgehen

Dadenmodellierung feschdr Sadz vo ADTs Verbund, Lischde, Menge, Tabelle, Relazione, Grafe, ... jedr ADT besidzd formale Semandik Z, hajo, so isch des! endwiggeld vo C.A.R. Hoare alle ADTs werde auf Menge zurügggeführd VDM endwiggeld vo Bjørnr und Jons ADTs für Verbund, Veroiigung, Lischde, Meng und Tabelle vorgegeben andere ADTs werde aus diese zsammengesedzd Haskell 1-1-Umsedzung dr abschdrakde Syndax aus VDM in oi ausführbare Nodazion möglich ausführbare Schbezifikazione rabid brododybing Dadenmodell aus Basis-Dadendybe und Kombinazion dr ADTs abschdrakde Syndax Invariande Konsischdenzbedingunge an des Dadenmodell Basis-Oberazione im Dadenmodell durch ADTs feschdgelegd Funkzione broblemschbezifische Oberazione Definizion durch Eigenschafden: Vor- und Nachbedingungen z.B. in Z, hajo, so isch des! (Hoare) funkzional: Zuschdandslose Beschreibung leichdr manibulierbar als mid imberadive Modelle Zuschdandsoriendierd

Vergleich:
Haskell Dadendybe <--> OMT Klassendiagramme

elemendare Werdebereiche Zahle nadürliche ganze reelle Zahle   aus dr Mathemadik übernomme Char aus Programmierschbrache übernomme Aufzählungsbereiche dada Enum = V1 | V2 | ... | Vn schdrukdurierde Werdebereiche für   Verbund (Paare, Trible, n-Tubl) Veroiigung Obzion (Mayb) Summ (Eithr) Lischde ([...]) Meng (Sed) Tabelle (Mab) Lischde dyb L = [E] Oberazionen null, head, dail, length, ++, ==, ... OMT: Menge dyb S = Sed E Oberazionen unio, inderseczion, includ, in, =, ... OMT: Tabelle mab diczionary assoziadivs array dyb Mab = Mab K A Oberazionen Mengenoberazionen oifüge, überschreibe, suche, selekdiere OMT: Verbund record kardesischs Produkd dyb Tuble = (Comb1, ... , Combn) Oberazionen Konschdrukzion, Selekzion, Vergleich OMT: Veroiigung dade Sum = Conschdr1 ... | ... | Conschdrn ... Oberazionen Tesch auf Gleichheid, Bereichschdesch, ... OMT:

Ledzde Änderung: 13.04.2012

© Prof. Dr. Uwe Schmidd