entwurf zuverl assiger software - universität potsdam · lehrziele und geplanter aufbau der...
Post on 18-Sep-2018
213 Views
Preview:
TRANSCRIPT
Entwurf zuverlassiger Software
Sommersemester 1996
Christoph KreitzFG Intellektik, TH Darmstadt, Telephon (06151) 16-2863
kreitz@intellektik.informatik.th-darmstadt.de
1. Einfuhrung: Notwendigkeit zuverlassiger Entwurfsmethoden. . . bei der Entwicklung von Softwaresystemen. . . bei der Entwicklung von Algorithmen
2. Wissensbasiertes Software-Engineering
– Chancen und Grenzen
3. Lehrziele und geplanter Aufbau der Vorlesung
4. Organisatorisches
Entwurf zuverlassiger Software 1 Einfuhrung
Kommerzielle Softwareproduktion
COMPUTER
exakte
KUNDE
Sumpf der Unklarheit
Beschreibung
Wildnis derLoesungswege
Anforderung Programm
Spezifikation
• “von Hand”, direkt in Programmiersprache, schnell
• Software-Krise – ungelost seit 25 Jahren
– Hohe Kosten fur Erstellung und Wartung
– Modifikationen und Erweiterungen schwierig
– Mangelnde Zuverlassigkeit mit fatalen Folgen
Entwurf zuverlassiger Software 2 Einfuhrung
Softwareentwicklung ist ..
logischer Schlußfolgerungsprozeß
+ Kreativitat
+ Verarbeitung von Wissen (Erfahrung)
+ fehlerfreie Codierung (Disziplin)
⇒ Kooperation zwischen Mensch und Maschine sinnvoll
– Programmierer: Steuerung des Entwicklungsprozesses
– Computer: Korrektheitsgarantie fur erzeugte Software
Entwurf zuverlassiger Software 3 Einfuhrung
Systementwurf: Typische Problemstellung
Flugverkehrverwaltung uber Europa
Gegeben sei eine Menge von Stadten, Flughafen, Flugzeugtypen, (ge-
planten) Flugen und Ereignissen, die innerhalb eines Zeitintervalls
von 24 Stunden vorkommen. Entwerfen und implementieren Sie ein
Programmsystem, das alle Veranderungen der Flug- und Flughafen-
zustande entsprechend der folgenden Problembeschreibung berech-
net und protokolliert.
Entwurf zuverlassiger Software 4 Einfuhrung
Flugverkehrverwaltung: zu verarbeitende Konzepte
Stadte haben einen Namen und eine Anzahl zugehoriger Flughafen.
Flughafen haben einen Namen, eine Stadt in deren Nahe sie liegen und eine Anzahl von abfliegenden
und ankommenden Flugen. Der Zustand eines Flughafens kann clear , fog , snow , traffic oder heavy
traffic sein. Die Kapazitat eines Flughafens besagt, wieviele Fluge abgewickelt werden konnen, ohne
daß es zu Verspatungen kommt. Es gibt eine Menge von Ausweichflughafen samt ihrer Entfernung. Es
ist bekannt, ob Landungen bzw. Starts bei Nebel moglich sind. Schließlich ist jedem Flughafen eine
Folge von bisherigen Ereignissen zugeordnet.
Fluge haben eine Fluggesellschaft, Flugnummer, Flugzeugtyp, Start- und Zielflughafen, Abflug- und
Ankunftszeit und einen Status (regular , delayed , late , diverted , cancelled oder forced landing).
Flugzeugtypen haben eine Bezeichnung, eine Passagierkapazitat, eine maximale Reichweite (in
Flugstunden) und eine Liste von Flugen, die von Flugzeugen dieses Typs durchgefuhrt werden. Es ist
bekannt ob Flugzeuge dieses Typs uber eine Nebellandevorrichtung verfugen.
Ereignisse sind wetterbedingte Veranderungen des Zustands eines Flughafens. Sie werden durch die
Vorkommenszeit, den betroffen Flughafen und den erzeugten Zustand (clear , fog , oder snow)
beschrieben. Ereignisse haben direkte und indirekte Auswirkungen auf Flughafen und Flugplane:
Entwurf zuverlassiger Software 5 Einfuhrung
Flugverkehrverwaltung: mogliche Ereignisse I
snow: Fluge, die in einem Flughafen landen sollen, der zum Zeitpunkt der Ankunft verschneit ist,
werden zum nachsten Ausweichflughafen umgeleitet, der clear ist und fur den Flugzeugtyp
erreichbar ist. Die Ankunftszeit dieser Fluge wird entsprechend der Entfernung zu diesem
Ausweichflughafen verspatet und der Flug gilt als diverted . Erfullt keiner der Ausweichflughafen
die o.g. Bedingungen, dann werden die betroffenen Fluge zu dem Flughafen zuruckgeschickt, von
dem aus sie gestartet sind und die Ankunftszeit entsprechend der bisherigen Flugzeit berechnet.
Fluge, die innerhalb von 5 Stunden nach dem Einsetzens des Schnees hatten starten sollen,
erhalten den Status cancelled .
fog: Fluge, die in einem Flughafen landen sollen, auf dem zur Ankunftzeit Nebel herrscht, werden
um 30 Minuten verspatet, wenn keine Landung bei Nebel moglich ist. Sie erhalten den Status
delayed , wenn der bisherige Status regular ist bzw. late , wenn der bisherige Status delayed ist.
Lost sich der Nebel vor der aufgeschobenen Ankunftszeit dieser Fluge nicht auf, so werden sie
zum nachsten Ausweichflughafen umgeleitet, wobei die gleichen Regeln wie beim Auftreten von
Schnee gelten.
Der Abflug von Flugen, die in einem nebligen Flughafen ohne Nebellandevorrichtung starten
sollen, wird 30 Minuten verzogert. Ihre Ankunft wird um 30 Minuten verspatet, wenn die
ursprungliche Flugzeit weniger als 4 Stunden betragt, und ihr Status entsprechend verandert.
Lost sich der Nebel innerhalb dieser 30 Minuten nicht auf, so wird der Abflug um weitere 30
Minuten verzogert.
Entwurf zuverlassiger Software 6 Einfuhrung
Flugverkehrverwaltung: mogliche Ereignisse II
traffic: Wird die regulare Kapazitat eines Flughafens um bis zu 50% uberschritten und ist der
Status der Flughafens clear , so erhalt der Flughafen den Status traffic. Ankommende Fluge
werden um 30 Minuten verspatet und ihr Status entsprechend verandert. Ebenso werden
startende Fluge um 30 Minuten verzogert, wobei die gleichen Regeln wie bei nebelbedingten
Abflugverzogerungen gelten.
heavy traffic: Wird die regulare Kapazitat eines Flughafens um mehr als 50% uberschritten und
ist sein Status clear oder traffic so erhalt der Flughafens den Status heavy traffic. Fluge, die
innerhalb von einer Stunde nach Beginn dieses Zustands landen sollen, werden um 1 Stunde
verspatet. Sie erhalten den Status late , wenn der bisherige Status regular oder delayed ist.
Fluge, die spater als 1 Stunde nach Beginn des heavy traffic-Status landen sollen und nicht
bereits diverted sind, werden zum nachsten geeigneten Ausweichflughafen umgeleitet. Sie
erhalten den Status diverted und ihre Verspatung wird entsprechend bestimmt. Fluge, die von
einem Flughafen starten sollen, der sich im heavy traffic-Status befindet, erhalten den Status
late . Ihr Abflug wird um eine Stunde verspatet. Ihre Ankunft wird um 30 Minuten verspatet,
wenn die Flugzeit mehr als 4 Stunden betragt, andernfalls um 1 Stunde.
Fluge, deren Flugzeit aufgrund einer Verspatung oder Umleitung die maximale Flugzeit ihres
Flugzeugtyps uberschreitet, landen im Flughafen, in dem die Verspatung oder Umleitung
ausgelost wurde, und erhalten den Status forced landing . Ihre Abflug- und Ankunftszeiten
bleiben unverandert.
Entwurf zuverlassiger Software 7 Einfuhrung
Entwurf von Softwaresystemen
• Komplexe Aufgabenstellung, meist nur grob umrissen– Ad hoc Losung oft unmoglich– Modellierung der realen Welt erwunscht– Algorithmische Probleme einfach⇒ Systemstrukturierung wichtiger als Codierung
• Rechnerunterstutzung eingeschrankt moglich– Veranschaulichung– Projektplanung und -uberwachung– Einhaltung einer bestimmte Methodik bei Systementwicklungaber– kein “deduktives” Problem: Ausgangspunkt informal – Zielpunkt formal– Korrektheitsbegriff unklar⇒ beschrankte Automatisierbarkeit
• CASE, Objektorientierung, “formale Methoden”– Hilfe bei Strukturierung, Spezifikation, Wiederverwendbarkeit– Korrektheitsgarantie kaum moglich
Entwurf zuverlassiger Software 8 Einfuhrung
Algorithmenentwurf: Typische Problemstellung
Problem der Maximalen Segmentsumme
• Gegeben eine Folge a1, a2, . . . , an ganzer Zahlen
Bestimme die Summe Σqi=pai eines Segmentes, die maximal im Bezug auf
alle moglichen Summen von Segmenten ist
Mn ≡ max(Σqi=pai | 1≤p≤q≤n)
• Direkte Losung leicht zu finden, aber ineffizient
• Induktive Betrachtung liefert
M1 = a1, Mn+1 = max(Mn,Ln+1)
wobei Ln ≡ max(Σni=pai | 1≤p≤n)
L1 = a1, Ln+1 = max(Ln+an+1,an+1) )
→ eleganterer, effizienterer und korrekter Algorithmus
Entwurf zuverlassiger Software 9 Einfuhrung
Maximale Segmentsumme – direkte Losung
maxseg:INTEGER islocal p, q, i, sum :INTEGERdo
from p := lower -- variiere untere Grenze pResult := item(lower); -- Initialwert zum Vergleich
until p >= upperloop
from q := p -- variiere obere Grenze quntil q > upperloop
from i := p ; -- Berechne∑q
i=p ai
sum := item(i) -- Initialwert der Summeuntil i = qloop
i := i+1; sum := sum+item(i)end -- sum =
∑qi=p ai
if sum > Result then Result := sum endq := q+1
end;p := p+1
endend
Entwurf zuverlassiger Software 10 Einfuhrung
Maximale Segmentsumme: systematische Losung
maxseg:INTEGERislocal n, L n :INTEGERdo
from n := lower;Result := item(n);L n := item(n)
until n >= upperinvariant -- Result = Mn ∧ L n = Lnvariant upper - nloop
if L n > 0then L n := L n + item(n)else L n := item(n)
end; -- L n = Ln+1if L n > Result
then Result := L nend; -- Result = Mn+1n := n+1
endend
Entwurf zuverlassiger Software 11 Einfuhrung
Entwurf von Algorithmen
• Uberschaubare, eindeutig spezifizierte Aufgabenstellung– Algorithmische Probleme schwierig– Ad hoc Losung moglich, aber fehleranfallig⇒ systematischer Entwurf zur Korrektheitssicherung erforderlich
• Formalisierbares Vorgehen– Ausgangspunkt (Spezifikation) und Zielpunkt (Programm) formal– Korrektheitsbegriff klar definierbar– “deduktives” Problem: Computerbeweise moglich
• Rechnerunterstutzung durch nachtragliche Verifikation– Korrektheitsbeweis durch Rekonstruktion der Programmidee– Unterstutzung bei Entwurf und Implementierung fehlt
• Rechnerunterstutzung durch Programmsynthese– semi-automatische Erzeugung von Programmen aus formalen Spezifikationen– Programmierung durch logische Schlußfolgerungsprozesse
7→ Implementierung schnell + garantiert korrekt+ automatische Dokumentation des Entwicklungsprozesses
7→ Wartung / Modifikation leicht
Entwurf zuverlassiger Software 12 Einfuhrung
Wissensbasierte Softwareentwicklung
= Erzeugung formaler Spezifikationen aus Anforderungen
+ Synthese von Programmen aus formalen Spezifikationen
• Formalisierung von Wissen (Kalkule)– Formale Sprache
– Grundgesetze und Inferenzregeln, welche logisches Schließen simulieren
– Verfahren zum Erwerb von formalem “Synthesewissen”
• Methoden zum Entwurf formaler Spezifikation– Analyse und Modellierung der Realitat in formaler Sprache
• Strategien zur automatischen Programmsynthese– Beweisfuhrung: Automatisierung des Schließens mit Kalkulen
– Programmerzeugung + korrektheitserhaltende algorithmische Optimierung
– Implementierung abstrakter Datentypen
– (sprachabhangige Compilierung & Optimierung)
Entwurf zuverlassiger Software 13 Einfuhrung
Verfahren der Programmsynthese
• Beweisbasierte Syntheseverfahren
– Steuerung von Regeln eines ausdrucksstarken mathematischen Kalkuls
7→ Korrektheitsgarantie fur erzeugter Software
– niedriges Abstraktionsniveau (elementare formale Logik)
7→ fur Programmierer schwer verstandlich (Kooperation unmoglich)
7→ nur “Spielbeispiele” praktisch losbar
• Praktisch orientierte Syntheseverfahren
– theoretische Untersuchungen + ad hoc Codierung
7→ Prototypen erfolgreich: schnellere Entwicklung + schnellere Software
KIDS: US-Army Transport Scheduling Algorithmus um Faktor 2000 (!!) schneller
– Fehler bei Codierung des Verfahrens moglich
7→ keine echte Korrektheitsgarantie
Integration der Starken beider Ansatze in Erforschung
Entwurf zuverlassiger Software 14 Einfuhrung
Lehrziele
• Softwaresysteme mit formalen Methoden entwerfen
– Verstandnis objektorientierter Konzepte
– Objektorientierte Modellierung
• Programmsynthesesysteme verwenden konnen
– Methodik verstehen
– Syntheseprozesse vorplanen und von Hand durchspielen
– Arbeit mit praktischen Systemen (?)
• Programmsyntheseverfahren weiterentwickeln
– Starken und Schwachen einschatzen
– Theorembeweiser und ahnliche KI Methoden spezialisieren
– uberzeugende Beispiele entwerfen
Entwurf zuverlassiger Software 15 Ubersicht
Geplanter Aufbau der Vorlesung
1. Qualitatskriterien fur zuverlassige Software (3.4. – 4.4.)
2. Modulare Strukturierung von Softwaresystemen (10.4. – 25.4.)
– Abstrakte Datentypen, Klassen und Objekte
– Kontraktmodell: Importe und Zusicherungen
– Generizitat und Vererbung
3. Kalkulbasierte Programmsynthese (2.5. – 23.5.)
– Grundkonzepte, Formalisierung
– Synthese durch konstruktive Beweisfuhrung
– Synthese durch logische Transformationen
4. Wissensbasierte Programmsynthese (29.5. – 27.6.)
– Synthese durch Algorithmenschemata
– Globalsuche, Divide&Conquer, Lokalsuche, . . .
– Korrektheitserhaltende algorithmische Optimierung
5. Systeme und Anwendungen (3.7. – 4.7.)
Entwurf zuverlassiger Software
Lektion 2
Qualitatskriterien und Entwurfsprinzipien
1. Qualitatskriterien
2. Leitlinien fur System- und Algorithmenentwurf
3. Formale Grundbegriffe
Entwurf zuverlassiger Software 16 Entwurfsprinzipien
Softwarequalitat – externe Merkmale
Korrektheit – Programm erfullt exakt seine Aufgaben
Robustheit – funktioniert auch unter außergewohnlichen Bedingungen
Erweiterbarkeit – anpaßbar an geanderte Anforderungen
Wiederverwendbarkeit – fur neue Anwendungen
Kompatibilitat – verbindbar mit anderen Programmen
Effizienz – okonomische Nutzung von Platz und Zeit
Portabilitat – leicht ubertragbar auf verschiedene Umgebungen
Verifizierbarkeit – Fehler wahrend der Betriebsphase erkennbar
Integritat – gegen unberechtigten Zugriff
Benutzerfreundlichkeit – leichter Umgang fur ungeubte Benutzer
Entwurf zuverlassiger Software 17 Entwurfsprinzipien
Entwicklungsprozeß fur große SoftwaresystemeEvolutionare Entwicklung von Software (Phasenkonzept)
?Problemstellung
Systemanalyse
?Pflichtenheft
Deskriptive Formulierung
?formale Spezifikation
Entwurf
?Grobstruktur des Systems
Implementierung
?Realisierung in Programmiersprache
Tests, Dokumentation
6
Abnahme durch Benutzer
Vorschlage fur
erweiterte,
verbesserte
neue Version
Entwurf zuverlassiger Software 18 Entwurfsprinzipien
Leitlinien fur die Systementwicklung
1. Analyse + Gestaltung– Gesetzmaßigkeiten des Umfelds entdecken
– Modell eines Ausschnitts der Realitat fixieren
2. Grobspezifikation– Welche Leistungen mussen nach außen sichtbar sein?
3. Feinspezifikation / Systementwurf– Zerlegung des Systems in unabhangige interne Komponenten
– Beschreibung einzelner Klassen/Module
– Beziehung der Klassen (Generizitat, Vererbung, Benutzung)
– Beschreibung der Dienstleistungen (Kontrakte)
4. Entwurf und Implementierung von Algorithmen– Realisierung der Dienstleistungen
– Prozeduralisierung (Namen einsetzen, Parameter bestimmen)
– Schrittweise Verfeinerung (Teilschritte, Alternativen, Wiederholungen)
5. Ein- und Ausgabeformate zum Schluß
Entwurf zuverlassiger Software 19 Entwurfsprinzipien
Kriterien fur gute Entwurfsmethoden
Zerlegbarkeit in Module
– kooperierende Einheiten geringer Komplexitat
– Verstandlicheres Gesamtsystem
Zusammensetzbarkeit aus Modulen
– Wiederverwendung vorgegebener Einheiten
Verstandlichkeit der Module
– unabhangig von der konkreten Verwendung
– erleichtert Wartung und Modifikationen
Stetigkeit der Module
– kleine Anderungen haben geringe Folgen
– lokale Modifikationen nach außen i.w. unsichtbar
Modularer Schutz
– Fehler und Ausnahmesituationen werden im Modul behandelt
Entwurf zuverlassiger Software 20 Entwurfsprinzipien
Entwurfsprinzipien fur Softwaresysteme
Module mussen Klassen entsprechen
– fordert Verstandlichkeit und Kombinierbarkeit
Minimale Kommunikation zwischen Moduln
– fordert Stetigkeit
Schmale Schnittstellen
– fordert Stetigkeit und modularen Schutz
Vollstandige Beschreibung der Schnittstellen
– fordert Zerlegbarkeit, Kombinierbarkeit, Verstandlichkeit, Stetigkeit
Geheimnisprinzip
– fordert Stetigkeit und modularen Schutz
Entwurf zuverlassiger Software 21 Entwurfsprinzipien
Systemspezifikation durch abstrakte Datentypen
Vollstandige, genaue und eindeutige Beschreibung
einer Datenstruktur ohne Uberspezifikation
• Welche Typen werden eingefuhrt?
• Welche Funktionen (Dienstleistungen) werden eingefuhrt?
• Was sind die Vorbedingungen fur die Anwendbarkeit der
Funktionen?
• Welche Axiome (Eigenschaften) erfullen die Funktionen?
Systementwurf = strukturierte Sammlung abstrakter Datentypen
Entwurf zuverlassiger Software 22 Entwurfsprinzipien
Systemenentwurf: Formale Grundbegriffe
• Systemspezifikation: Abstrakter Datentyp T = (S, Ω, Ax)
– S: Menge von Sortennamen (Namen fur Datentypen)
– Ω: Familie von Operationsnamen (zusammen mit Typisierung)
– Ax: Menge von Axiomen fur Datentypen und Operationen
• Modul/Klasse M : Struktur fur T :
– Menge von konkreten Datentypen und Operationen, typisiert gemaß Ω
• Korrektheit von M : M Modell fur T– M ist eine Struktur, die alle Axiome aus T erfullt
• Alternative Darstellung bei imperativen
Programmiersprachen
– Vor- und Nachbedingungen von Routinen
– Invarianten von Klassen
Entwurf zuverlassiger Software 23 Entwurfsprinzipien
Abstrakter Datentyp Liste
TYPES: List[X]
FUNCTIONS: empty: List[X] → BOOLEAN
new: → List[X]
cons: X×List[X] → List[X]
head: List[X] 6→ X
tail: List[X] → List[X]
PRECONDITIONS: pre head(L:List[X]) = (not empty(L))
AXIOMS: ∀x:X.∀L:List[X].
empty(new())
not empty(cons(x,L))
head(cons(x,L)) = x
tail(cons(x,L)) = L
tail(new()) = new()
Entwurf zuverlassiger Software 24 Entwurfsprinzipien
Implementierung zuverlassiger Programme
• Systemspezifikation liefert Implementierungs“vertrag”
von Algorithmen
– Implementierung muß nur lokale Axiome der Klasse berucksichtigen
– Aufteilung der Implementierung in unabhangige Komponenten moglich
– Syntheseverfahren fur Algorithmenentwurf einsetzbar
• Korrektheit von Programmen ist nicht testbar
– digitale Verfahren sind unstetig
– Korrektheitsbeweis muß moglich sein
Entwurf zuverlassiger Software 25 Entwurfsprinzipien
Leitlinien fur den Algorithmenentwurf
• Programmentwicklung durch Beweisfuhrung– Beweisidee liefert Implementierungsidee und sichert Korrektheit
• Eigenschaften zu manipulierender Objekte klaren– “Objekttheorie” hilft bei Problemlosung
• Formalismus und gesunder Menschenverstand
• Bewußtes Anwenden von Prinzipien– vermeidet Fehler, die durch oberflachliche Betrachtung entstehen
• Entwicklung am angestrebten Resultat orientieren– Top-Down zugang zum Algorithmenentwurf
• Problemstellung einfach und prazise beschreiben– erleichtert formale Methoden und Rechnerunterstutzung
• Programmiere nicht innerhalb einer Programmiersprachesondern in die Sprache hinein.– trenne Algorithmenentwurf vom Programmcode
Entwurf zuverlassiger Software 26 Entwurfsprinzipien
Algorithmenentwurf: Formale Grundbegriffe
• Spezifikation: Tupel spec = (D,R,I,O)
Notation : FUNCTION f(x:D):R WHERE I(x) RETURNS y SUCH THAT O(x,y)
– D (Domain) und R (Range): Datentypen
– I (Input-Bedingung an zulassige Eingaben): Pradikat uber D
– O (Output-Bedingung an mogliche Ausgaben): Pradikat uber D×R
D,R,I,O in Spezifikationssprache zu beschreiben
• Programm: Tupel p = ( D,R,I,O,body )
FUNCTION f(x:D):R WHERE I(x) RETURNS y SUCH THAT O(x,y) = body(x)
– (D,R,I,O): Spezifikation
– body:D6→R (Programmkorper): berechenbare Funktion
body in Programmiersprache zu beschreiben (f darf vorkommen)
• Programm p korrekt, falls gilt: ∀x:D. I(x) ⇒ O(x,body(x))
• Spezifikation spec erfullbar (synthetisierbar), falls eine Funktion
body:D6→R existiert, so daß p=(spec,body) korrekt ist
Entwurf zuverlassiger Software 27 Entwurfsprinzipien
Phasen eines computergestutzten Entwurfs von Software
?Problemstellung
Systemanalyse
Deskriptive PrazisierungFormalisierung vorkommender Begriffe
Aufstellen mathematischer Gesetze
?“Objekttheorie” + formale Spezifikation
Systementwurf“formale Methoden”/ OMT
?Spezifikation von Modulen und Routinen
Implementierung
Algorithmenentwurf / Programmsynthese
Verifizierte algorithmische Optimierung
Implementierung abstrakter Datentypen
Compilierung/sprachabhangige Optimierung
?Realisierung in Programmiersprache
(Tests), Dokumentation
6
Abnahme durch Benutzer
Verbesserungs-
Vorschlage
Entwurf zuverlassiger Software
Lektion 3
Spezifikation von Modulen
1. Klassen und Objekte
2. Routinen
3. Geheimnisprinzip
4. Generizitat
5. Zusicherungen: Vertrage fur Software-Zuverlassigkeit
6. deferred Classes: abstrakte Spezifikation von Klassen
Entwurf zuverlassiger Software 28 Klassen
Leitbeispiel – Bibliothekenverwaltung
• Bibliotheken:
– z.B. Informatik, Mathematik, E-Technik, LHB, ...
• Bucher:
– Autor, Titel, Kennung, Entleihstatus, Leihfrist ....
• Benutzer:
– Entleiher, Universitatsangestellte, Professoren
– Bibliotheksmitarbeiter
• Transaktionen:
– Ausleihen, Verlangerung, Ruckgabe
– Entnahme, Neubeschaffung, Status andern
• Dienstleistungen:
– Verwaltung, Mahnung, Informationssystem
Entwurf zuverlassiger Software 29 Klassen
Objekte
• extern: Bestandteil der realen Welt
• intern: Laufzeitelemente eines Softwaresystems– strukturierte Reprasentation externer Objekte
– abstrahiert auf verarbeitungsrelevante Komponenten
Beispiel:
‘Bertrand Meyer’
‘Objektorientierte Software-entwicklung’
1990
‘Hanser’
547
‘D4.1 Mey 8267’
4 Zeichenketten, 2 ganze Zahlen — moglicherweise Reprasentation eines Buches
Entwurf zuverlassiger Software 30 Klassen
Komplexe Objekte
‘Objektorientierte Software-entwicklung’1990
‘Hanser’547
‘D4.1 Mey 8267’
‘Eiffel -- the Language’1992
‘Prentice Hall’595
‘D4.1 Mey 8935’‘Meyer’
‘Bertrand’1946????
Frankreich-
XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXz
‘Referenzsemantik’
‘Meyer’‘Bertrand’
1946????
Frankreich
‘Objektorientierte Software-entwicklung’1990
‘Hanser’547
‘D4.1 Mey 8267’
Objekt in anderem Objekt
nicht empfehlenswert
Konsistenzprobleme zu erwarten
Entwurf zuverlassiger Software 31 Klassen
Klassen
Statische Beschreibung einer Menge von Objekten– Attribute: Struktur der Objekte– Routinen: erlaubte Operationen auf Objekten→ Features der Klasse
Einfaches Beispiel (in Eiffel)
class PERSON feature
name, vornamen: STRING;
geburtsjahr, todesjahr: INTEGER;
nationalitat: STRING
end -- class PERSON
– Schlusselworte class, feature, end
– Trennzeichen ‘;’, Kommentaranfang ‘--’
Reprasentation abstrakter Datentypen in Programmiersprache
Entwurf zuverlassiger Software 32 Klassen
Kunden und Lieferanten
• Klasse A heißt Kunde der Klasse B,
wenn A eine Deklaration der Form entity:B enthalt.
B heißt Lieferant von A
• Selbstreferenz ist moglichclass PERSON feature
name, vornamen: STRING;
geburtsjahr, todesjahr: INTEGER;
nationalitat: STRING;
vater, mutter: PERSON
end -- class PERSON
• Zyklische Objektstrukturen sind erlaubt
Entwurf zuverlassiger Software 33 Klassen
Routinen
Wesentliche Dienstleistungen einer Klasse
• Prozeduren: konnen Zustand eines Objektes andern
• Funktionen: berechnen Werte (aus dem Zustand von Objekten)
• Punktnotation fur Aufruf: entity.operation(argumente)
– Komponentenzugriff: p.vornamen (p Objekt von PERSON)
= Komponente von p, die dem Attribut vornamen entspricht
– Funktion: p.anzahl vornamen
= berechnete Anzahl der Vornamen des Objektes p
– Funktion: p.alter(1993)
= berechnetes Alter der mit p bezeichneten Person im Jahre 1993
– Prozedur: p.setze todesjahr(1993)
Veranderung des Zustandes von p: die Komponente, welche dem Attribut
todesjahr entspricht, wird auf 1993 gesetzt
Entwurf zuverlassiger Software 34 Klassen
Definition von Routinen
class PERSON feature
name, vornamen, nationalitat: STRING;
geburtsjahr, todesjahr: INTEGER;
vater, mutter: PERSON;
anzahl vornamen: INTEGER is -- Anzahl der Vornamen bestimmendo Result := Anzahl der Vornamen in vornamenend; -- anzahl vornamen
alter(jahr:INTEGER): INTEGER is -- Alter im jahr bestimmendo Result := jahr - geburtsjahrend; -- alter
setze todesjahr(jahr:INTEGER) is -- Todesjahr auf jahr setzendo todesjahr := jahrend -- setze todesjahr
end -- class PERSON
– Schlusselwortfolge is...do...end oder is...deferred
– Formale Argumente in Klammern: Namen:Typ– Funktionen haben Ergebnistyp – Ergebnis in Result
– Rumpf: do anweisung1; anweisung2; ...;anweisungn end
Entwurf zuverlassiger Software 35 Klassen
Vordefinierte Operationen
!!entity Standard-Erzeugung von Objekten
!!entity.init(argumente) Nicht-Standard-Erzeugung von Objekten
entity := Ausdruck Zuweisung (limitiert)
entity.attribut (Komponenten)Zugriff (limitiert)
entity := void() Auflosen eines Verweises
entity = void() Uberprufung des Verweiszustandes
entity := clone(entity 1) (Flache) Duplizierung von Objekten
entity := deep clone(entity 1) Tiefe Duplizierung von Objekten
entity.copy(entity 1) (Flache) Kopie von Objektinhalten
entity.deep copy(entity 1) Tiefe Kopie von Objektinhalten
entity 1 = entity 2 Vergleich von Objekten
equal(entity 1,entity 2) (Flacher) Vergleich von Objektinhalten
deep equal(entity 1,entity 2) Tiefer Vergleich von Objekten
Current Verweis auf das aktuelle Objekt
Entwurf zuverlassiger Software 36 Klassen
Klassendefinition mit Initialisierungsprozedur
class PERSON
creation
init mit namen
feature...
init mit namen(n,v:STRING) is -- Initialisiere Person
-- mit Vornamen und Namen
do
name := n;
vornamen := v
end; -- init mit namen...
end -- class PERSON
Entwurf zuverlassiger Software 37 Klassen
Geheimnisprinzip
• Interne Darstellung der Daten nach außen unsichtbar
• Direktes Lesen und Schreiben von Daten nicht erlaubt
Veranderung/Auswertung nur uber prozedurale Schnittstellen
⇒ Aufruf von Attributen entspricht Funktionen
⇒ Zuweisungen nur innerhalb der deklarierenden Klasse
⇒ nicht alle Attribute nach außen hin zuganglich
selektiver Export von Features
– Angabe in geschweiften Klammern hinter feature
feature Klasse1,...,Klassen featurelist
Entwurf zuverlassiger Software 38 Klassen
Klassendefinition mit Datenkapselung
class PERSON
creation init mit namen
feature
vornamen liste: STRING;
feature
init mit namen(n,v:STRING) is ... do ... end;
name: STRING;
vornamen: STRING is ... do ... end;
anzahl vornamen: INTEGER is ... do ... end;
geburtsjahr, todesjahr: INTEGER;
alter(jahr:INTEGER): INTEGER is ... do ... end;
setze todesjahr(jahr:INTEGER) is ... do ... end;
vater, mutter: PERSON;
geschwister: ARRAY[PERSON] is ... do ... end;
großeltern: ARRAY[PERSON] is ... do ... end;
nationalitat: STRING
end -- class PERSON
Entwurf zuverlassiger Software 39 Klassen
Selektiver Export von Features
class PERSONcreation init mit namenfeatureinit mit namen(n,v:STRING) is ... do ... end;name: STRING;vornamen: STRING is ... do ... end;anzahl vornamen: INTEGER is ... do ... end;
featureEINWOHNERMELDEAMTgeburtsjahr, todesjahr: INTEGER;alter(jahr:INTEGER): INTEGER is ... do ... end;vater, mutter: PERSON;nationalitat: STRING
featureSTANDESAMTsetze todesjahr(jahr:INTEGER) is ... do ... end;
featureEINWOHNERMELDEAMT, PERSONgeschwister: ARRAY[PERSON] is ... do ... end;
featurePERSONgroßeltern: ARRAY[PERSON] is ... do ... end;
featurevornamen liste: STRING;
end -- class PERSON
Entwurf zuverlassiger Software 40 Klassen
Listenklassen
class INTLIST
creation new
feature
empty: BOOLEAN is -- Liste leer ?
do...end;
new is -- Erzeuge leere Liste
do...end;
cons(n:INTEGER) is -- Hange n an
do...end;
head: INTEGER is -- Erstes Element
do...end;
tail is -- Entferne erstes
do...end
end -- class INTLIST
class REALLIST
creation new
feature
empty: BOOLEAN is -- Liste leer ?
do...end;
new is -- Erzeuge leere Liste
do...end;
cons(r:REAL) is -- Hange n an
do...end;
head: REAL is -- Erstes Element
do...end;
tail is -- Entferne erstes
do...end
end -- class REALLIST
Entwurf zuverlassiger Software 41 Klassen
Generische Klassendefinition
class LIST[X]
creation new
feature
empty: BOOLEAN is -- Ist die Liste leer ?
do...end;
new is -- Erzeuge leere Liste
do...end;
cons(r:X) is -- Hange r vor die Liste
do...end;
head: X is -- Erstes Element
do...end;
tail is -- Entferne erstes Element
do...end
end -- class LIST[X]
• formale generische Parameter in eckigen Klammern
mehrere generische Parameter moglich
• Konkrete Deklaration durch Instantiierung des Typparameters:
il: LIST[INTEGER]
personenlisten: LIST[LIST[PERSON]]
Entwurf zuverlassiger Software 42 Klassen
Generische Klasse Felder (mit infix Deklaration)
class ARRAY[X]
creation make
feature
lower, upper, count: INTEGER;
make(min,max:INTEGER) is -- Erzeuge Feld mit Grenzen min/max
do...end;
item, infix ¨@¨ (i:INTEGER):X is -- Element mit Index i
do...end;
put(val:X,i:INTEGER) is -- Weise dem Element mit Index i
-- den Wert val zu
do...end;...
end -- class ARRAY[X]
Infix-Bezeichner hinter Schlusselwort infix nach Funktionsnamen
– erlaubt p := p array@17 statt p := p array.item(17)
Entwurf zuverlassiger Software 43 Klassen
Vertrage fur Software-Zuverlassigkeit
• Sicherstellung von Korrektheit und Robustheit
– Garantien des Lieferanten fur Benutzer einer Klasse
– Festlegung von Bedurfnissen und Verantwortlichkeiten
• Spezifikationselemente in der Implementierung
– Gegenstuck zu Axiomen in abstrakten Datentypen
⇒ Zusicherungen (assertions)
– Ausdruck uber Zweck von Klassen, Routinen, Anweisungen
– wahrend der Laufzeit uberwachbar
– Dokumentation, Strukturierungs- und Verifikationshilfe
Entwurf zuverlassiger Software 44 Klassen
Bestandteile der Zusicherungssprache
• erreichbare Funktionen & Attribute, formale Argumente, Result
(keine Prozeduren, keine lokalen Variablen)
• Boolesche Ausdrucke (einschließlich Arithmetik)Eiffel logischer Operator
and Konjunktion ∧
or Disjunktion ∨
and then Sequentielle Konjunktion ∧
or else Sequentielle Disjunktion ∨
not Negation ¬
xor Exklusive Disjunktion ∨
implies Implikation ⇒
• Kommentare als Ersatz fur volle Pradikatenlogik
• Semikolon zur Trennung nicht zusammengehoriger Bestandteilen>0 ; not x=void()
• Namen fur zusammengehorige BestandteilePositiv: n>0 ; Nichtleer: not x=void()
• old: Wert bei Eintritt in eine Routine (nur in Nachbedingungen)
Entwurf zuverlassiger Software 45 Klassen
Vor- und Nachbedingungen
Beschreibung semantischer Eigenschaften von Routinen
• Vorbedingung: was muß beim Aufruf der Routine gelten?
– muß bei jedem Aufruf erfullt sein
– Schlusselwort require vor der Anweisungsfolge
• Nachbedingung: was gilt nach Beendigung der Routine?
– Garantie im Falle eines korrekten Aufrufs
– Schlusselwort ensure direkt vor dem end
Entwurf zuverlassiger Software 46 Klassen
Nachbedingung mit old
Ist a ein Attribut, dann bezeichnet in Nachbedingungen old a den Wert der ents-
prechenden Objektkomponente beim Aufruf und jedes andere Vorkommen von a den
Wert bei Beendigung der Routine
resize(min,max:INTEGER) is
-- Erweitere Feld auf Grenzen min und max
do...
ensure
upper >= old upper;
lower <= old lower
end; -- resize
Erforderlich, da Sprache imperativ
Entwurf zuverlassiger Software 47 Klassen
Vor- und Nachbedingungen als Vertrag
require und ensure beschreiben Rechte und Pflichten
• Vorbedingung bindet den Kunden:
– die Routine wird nur in erlaubten Fallen benutzt
– andernfalls ist der Lieferant zu nichts verpflichtet
• Nachbedingung bindet Lieferantenklasse
– Kunde kann sich auf versprochene Leistung verlassen
(falls die Vorbedingung eingehalten wurde)
– macht Verifikation von Routinen notwendig
• Vertrag erspart uberflussige Kontrollen
– Genauigkeit abhangig von Vertrauen
und Vielfalt der Anwendungsgebiete
Entwurf zuverlassiger Software 48 Klassen
Klasseninvarianten
Beschreibung globaler Eigenschaften von Objekten
Invariante: unveranderliche Eigenschaft der Klasse
– muß in jedem ‘stabilen’ Zustand erfullt sein
– Schlusselwort invariant am Ende der Klassendeklaration
Zusicherung I ist genau dann eine korrekte Klasseninvariante einer Klasse C, wenn
eine der beiden folgenden Bedinungen erfullt ist• I gilt nach jedem Aufruf einer Erzeugungsprozedur von C mit Argumenten,
welche die Vorbedingungen erfullen.
• I gilt nach jedem Aufruf einer exportierten Routine mit Argumenten, welche die
Vorbedingungen erfullen, die auf Objekte angewandt wurde, welche I erfullen.
Entwurf zuverlassiger Software 49 Klassen
Klassendefinition mit Klasseninvariantenclass ARRAY[X]creation makefeature
lower, upper, count: INTEGER;make(min,max:INTEGER) is -- Erzeuge Feld mit Grenzen min und max
do...ensure max<min implies count = 0;
max >= min implies lower = min and upper = maxend; -- make
item, infix ¨@¨ (i:INTEGER):X is -- Element mit Index irequire lower <=i; i <= upperdo...end; -- item
put(val:X,i:INTEGER) is -- Weise val dem Element mit Index i zurequire lower <=i; i <= upperdo...ensure item(i)=valueend; -- put
resize(min,max:INTEGER) is -- Erweitere Feld auf min und maxdo...ensure upper >= old upper; lower <= old lowerend; -- resize...
invariant
nonnegative size: count >= 0;consistent size: count = upper - lower + 1
end -- class ARRAY[X]
Entwurf zuverlassiger Software 50 Klassen
Aufgeschobene (deferred) Klassen
• Klassen mit nichtausfuhrbaren Routinen
– Routinendeklaration enthalt Schlusselwort deferred
anstelle des Anweisungsteils
– Klasse muß als deferred class deklariert werden
• Gegenstuck zum abstrakten Datentyp
– Leistungen werden spezifiziert, aber nicht implementiert
– Spezielle Implementierung in Erbenklassen
• Anwendungen:
– Abstrakter Entwurf und Verfeinerung in Eiffel
– partielle Implementierungen
– Oberklasse fur Klassen mit konzeptionellen Gemeinsamkeiten
polymorphe Anwendung gleichartiger Routinen
– auch als Ersatz fur Prozedurparameter in Routinen
Entwurf zuverlassiger Software 51 Klassen
Aufgeschobene Klasse von Listen
deferred class LIST[X]featurelength: INTEGER;empty: BOOLEAN is -- Ist die Liste leer ?
do length=0 end;new is -- Erzeuge leere Liste
deferredensure emptyend; -- new
cons(r:X) is -- Hange r vor die Listedeferredensure not empty; head = r -- tail wurde old liefernend; -- cons
head: X is -- Erstes Elementrequire not emptydeferred end; -- head
tail is -- Entferne erstes Elementdeferredensure old empty implies emptyend -- tail
invariant nonnegative size: size >= 0end -- class LIST[X]
Entwurf zuverlassiger Software
Lektion 4
Vererbung
1. Grundkonzepte
2. Polymorphie
3. Feature-Export, Redefinition und Umbenennung
4. Veranderung von Kontrakten
5. Implementierung aufgeschobener Klassen
Entwurf zuverlassiger Software 52 Vererbung
VERERBUNG
• Konzeptionelle Beziehung zwischen Klassen: –
Spezialisierung eines Konzepts (Erben)
– Generalisierung eines Konzepts (Vorfahren)
– Kombination von Konzepten (Mehrfachvererbung)
• Nachkommen erben Rechte und Pflichten der Eltern –
Unqualifizierter Aufruf geerbter features
– Modifikation geerbter features moglich
– Kontrakte der Vorfahren sind einzuhalten
• Vererbung ist transitiv
Steigert Erweiterbarkeit und Wiederverwendbarkeit
Entwurf zuverlassiger Software 53 Vererbung
Vererbung: Neue Moglichkeiten
• Polymorphismus
• Dynamisches Binden
• Trennung von Spezifikation und Implementierung
• Kombination von Klassen
• Modifikation geerbter Merkmale
– Anderung des Export-Status
– Redefinition
– Umbenennung
– Vervielfaltigung und Selektion bei wiederholtem Erben
– Erweiterung von Zusicherungen
Entwurf zuverlassiger Software 54 Vererbung
Klassendefinition mit Vererbung
class ENTLEIHER
inherit PERSON
feature
straße, hausnummer, stadt: STRING;
postleitzahl : INTEGER;
ausweisnummer: INTEGER
end -- class ENTLEIHER
-----------------------------------------------------------• ENTLEIHER ist Erbe (Nachkomme) von PERSON
PERSON ist Vorfahr von ENTLEIHER
• Elternklassen nach Schlusselwort inherit
• Features der Elternklasse automatisch verfugbar
Spezifische features werden erganzt
• Initialisierungsprozedur muß neu vereinbart werden
Entwurf zuverlassiger Software 55 Vererbung
Vererbung als Diagramm
'
&
$
%PERSON
'
&
$
%
*
ENTLEIHER
'
&
$
%
HHHHHHHHHHY
ARBEITNEHMER
ENTLEIHER und ARBEITNEHMER erben von PERSON
Entwurf zuverlassiger Software 56 Vererbung
Polymorphismus
Fahigkeit, verschiedene Formen anzunehmen
benutzerliste-
QQk
AA
AA
AA
AA
AA
AAK
3
Professorenobjekt Studentenobjekt Mitarbeiterobjekt Professorenobjekt
Keine Konvertierung notig
Entwurf zuverlassiger Software 57 Vererbung
Vererbungsregeln I
• Regel der Typvertraglichkeit:
Eine Zuweisung der Form x:=y, wobei x vom Typ A und y vom Typ B ist, ist
nur dann zulassig, wenn B konform zu A ist.
Gleiches gilt fur den Aufruf einer Routine mit formalem Parameter x und
aktuellem Parameter y, wobei x vom Typ A und y vom Typ B ist. Der Aufruf ist
nur dann zulassig, wenn B konform zu A ist.
• Regel des Dynamischen Bindens:
Ist x vom Klassentyp A und r eine in A deklarierte Routine, dann
wird ein Routinenaufruf der Form x.r an die Implementierung
gebunden, welche innerhalb der Klasse definiert wurde, zu der das
mit x zur Laufzeit verbundene Objekt gehort.
Entwurf zuverlassiger Software 58 Vererbung
Konformitat
B konform zu A, wenn eine der folgenden Bedingungen erfullt ist
1. A und B sind identisch,
2. A ist REAL oder DOUBLE und B ist INTEGER oder REAL,
3. A ist eine Klasse ohne generische Parameter und B ist eine Klasse, die A in der
inherit-Klausel auffuhrt,
4. A hat die Form G[A1, ..An] und B hat die Form G[B1, ..Bn], wobei G eine
generische Klasse ist und jedes der Bi zu Ai konform ist,
5. Es gibt einen Typen C mit der Eigenschaft, daß A konform ist zu C und C
konform zu B,
6. A hat die Form expanded B oder B hat die Form expanded A,
7. B hat die Form like anchor und der Typ von anchor ist konform zu A.
Entwurf zuverlassiger Software 59 Vererbung
Export geerbter features
class ENTLEIHER
inherit PERSON
export
name, vornamen, geburtsdatum
end -- feature-Anpassung von PERSON
feature
straße, hausnummer, stadt: STRING;
postleitzahl : INTEGER;
ausweisnummer: INTEGER
end -- class ENTLEIHER
• Schlusselwort export
• Schlusselwort end beendet Modifikationen geerbter features
• Ohne export-Klausel gilt alter Export-Status
Entwurf zuverlassiger Software 60 Vererbung
Selektiver Export geerbter features
class ARBEITNEHMER
inherit PERSON
export
ARBEITGEBER name, vornamen, geburtsjahr;
FINANZAMT all
end -- feature-Anpassung von PERSON
feature
adresse: ADRESSEN;
gehaltsklasse: STRING;
gehalt: REAL is -- Gehalt berechnen
do Result := Gehalt aus Tabelle nach gehaltsklasse end
end -- class ARBEITNEHMER
Syntax ahnlich wie bei feature-Klauselexport
Klassenliste1 featurelist 1;...
Klassenlisten featurelist n
Entwurf zuverlassiger Software 61 Vererbung
Vererbungsregeln II
• Regel der Featureanwendung:
Ist eine Große entity vom Klassentyp K, so ist die Anwendung entity.f eines
feature f nur dann zulassig, wenn f in einem Vorfahren von K definiert wurde.
• Regel des selektiven Exports:
Ein an eine Klasse K selektiv exportiertes feature f darf in allen Nachkommen
von K benutzt werden.
Entwurf zuverlassiger Software 62 Vererbung
Vererbung mit Redefinition
class UNI-ANGESTELLTE
inherit ARBEITNEHMER
redefine
gehalt
export
ARBEITGEBER name, vorname,geburtsjahr,adresse, gehaltsklasse;
FINANZAMT all
end -- feature-Anpassung von ARBEITNEHMER
feature
universitat: STRING;
fachbereich, raum, telephon: INTEGER;
gehalt: REAL is -- Gehalt berechnen
do Result := Gehalt nach Alter und gehaltsklasse end
end -- class UNI-ANGESTELLTE
• Schlusselwort redefine benennt neudefinierte features
• Schlusselwort all zur Abkurzung
• Typdeklarationen und Zusicherungen beachten!
Entwurf zuverlassiger Software 63 Vererbung
Vererbungsregeln III
Regel der Redefinition:
Ein Attribut, Funktionsergebnis oder formales Routinenargument
darf in einer Erbenklasse mit einem neuen Typ redeklariert
werden, wenn der neue Typ konform zum ursprunglichen ist.
Das Attribut oder die zugehorige Routine gilt als redefiniert.
Der Rumpf einer Routine kann redefiniert werden, solange die
obige Typeinschrankung nicht verletzt wird. Parameterlose
Funktionen durfen als Attribute redefiniert werden.
Redefinierte features, die nicht ursprunglich deferred waren, mussen
in einer entsprechenden redefine Klausel aufgefuhrt werden.
Entwurf zuverlassiger Software 64 Vererbung
Namenskonflikt
class STUDENTfeature
universitat: STRING;fachbereich: INTEGER;matrikelnummer: INTEGER
end -- class STUDENT
class HILFSKRAFTinherit
UNI-ANGESTELLTE...end; -- feature-Anpassung von UNI-ANGESTELLTE
STUDENT...end; -- feature-Anpassung von STUDENT
feature...
end -- class HILFSKRAFT
– Feature fachbereich erscheint doppelt
– Mehrfachvererbungen mit Namenskonflikten sind verboten
⇒ Umbenennung notig
Entwurf zuverlassiger Software 65 Vererbung
Umbenennung
class HILFSKRAFT
inherit
UNI-ANGESTELLTE
redefine
gehalt
export
name, vornamen, adresse, gehalt
end; -- feature-Anpassung von UNI-ANGESTELLTE
STUDENT
rename
fachbereich as studienfachbereich
export
universitat, studienfachbereich
end -- feature-Anpassung von STUDENT
feature
monatsstunden: INTEGER;
gehalt: REAL is -- Gehalt berechnen
do Result := Festgehalt nach monatsstunden end
end -- class HILFSKRAFT
Entwurf zuverlassiger Software 66 Vererbung
Vererbungsregeln IV
• Regel des wiederholten Erbens:
Bei wiederholtem Erben wird jedes feature des gemeinsamen
Vorfahren als gemeinsam genutzt (shared) angesehen, wenn es
auf dem gesamten Vererbungspfad nicht umbenannt wurde.
Features, die auf mindestens einem Wege umbenannt wurden,
werden als vervielfaltigt (replicated) angesehen.
• Regel der Generizitat bei wiederholtem Erben:
Bei wiederholtem Erben darf der Typ eines gemeinsam genutzten
features in der Elternklasse kein generischer Parameter sein.
Eine gemeinsam genutzte Routine darf in der Elternklasse keine
formalen Argumente enthalten, deren Typ ein generischer
Parameter ist.
Entwurf zuverlassiger Software 67 Vererbung
Vererbungsregeln V
• Regel der Umbenennung:
In einer Klasse K tritt ein Namenskonflikt auf, wenn zwei Eltern
E1 und E2 von K ein feature mit demselben Namen f enthalten.
Ein Namenskonflikt ist erlaubt, wenn f in einem gemeinsamen
Vorfahren V von E1 und E2 erstmalig definiert wurde, auf keinem
Vererbungspfad von V nach E1 und nach E2 umbenannt wurde
und in seiner Typdeklaration nicht an generische Parameter von
V gebunden ist.
Nicht erlaubte Namenskonflikte mussen durch Umbenennung
aufgelost werden.
Entwurf zuverlassiger Software 68 Vererbung
Vererbung von Kontrakten
• Regel der Elterninvarianten:
Die Invarianten aller Eltern einer Klasse gelten fur die Klasse selbst.
• Regel der Zusicherungsredefinition:
Ist r eine Routine der Klasse K und s eine Redefinition von r in
einem Nachkommen von K, so mussen die Vorbedingungen von s
schwacher sein als die von r und die Nachbedingungen starker.
– Fehlt in einer redefinierten Routine Vor- oder Nachbedingung, so wird die Vor-
bzw. Nachbedingung der ursprunglichen Version ubernommen.
– Vorbedingungen konnen nur durch eine require else-Klausel abgeschwacht werden.
– Nachbedingungen konnen nur durch eine ensure then-Klausel verstarkt werden.
Entwurf zuverlassiger Software 69 Vererbung
Implementierung aufgeschobener Klassen
• Aufgeschobene Klassen = Modulspezifikation
– Namen und Kontrakte von Features werden vereinbart
– Invarianten werden spezifiziert
– Objekte durfen nicht initialisiert werden
• Erbenklasse kann Spezifikation realisieren
– Namen und Kontrakte werden ubernommen
– aufgeschobene Routinen werden programmiert
– Initialisierung von Objekten definierbar
– Weitere Elternklassen zur Realisierung heranziehbar
Entwurf zuverlassiger Software 70 Vererbung
Mehrfachvererbung: Realisierung einer deferred class
class FIXED LIST[X]inherit LIST[X];
ARRAY[X] export allcreation newfeature-- Bereits effektiv deklariert: length: INTEGER;-- empty: BOOLEANnew is -- Erzeuge leere Liste
do make(1,0); length:=0end; -- new
cons(r:X) is -- Hange r vor die Listedo if length = upper then resize(1,length+1) end;
length := length+1;put(r,length)
end; -- conshead: X is -- Erstes Element
do Result := item(length)end; -- head
tail is -- Entferne erstes Elementdo if length/=0 then length:=length-1 endend -- tail
end -- class LIST[X]
Entwurf zuverlassiger Software
Lektion 5
Objektorientierter Entwurf von Softwaresystemen
1. Grundkonzepte eines systematischen Entwurfs
2. Leitbeispiel Bibliotheksverwaltung
– Analyse
– Formalisierung von Bedingungen
– Gestaltung von der Klassenstruktur
– Dienstleistungen einzelner Klassen
Entwurf zuverlassiger Software 71 Entwurfsmethoden
Grundideen des objektorientierten Entwurfs
dezentrale Architektur
uberschaubare, unabhangige, gleichberechtigte Einheiten
• Klassen sind der einzige Strukturierungsmechanismus– keine Schachtelung von Klassen
– Unabhangigkeit (nur Benutzung und Vererbung)
• Dienstleistungen werden gleichermaßen bereitgestellt– keine Operationen mit hoherer oder niedriger Bedeutung
– keine Vorschriften uber Reihenfolge des Aufrufs
• Keine Beschrankung der Anzahl der Dienstleistungen
• Bottom-up Entwurf sinnvoll– Aktivierung fertiger Programmteile anstreben
– Neue Klassen allgemein genug gestalten
• Zentralistisches Denken (“Hauptprogramm”) ablegen
Entwurf zuverlassiger Software 72 Entwurfsmethoden
Wie sinnvolle Klassen identifizieren?
• Lerne, vorhandene Entwurfe zu analysieren
– Starken und Schwachen beurteilen
– Erfahrungen fur eigene Entwurfe sammeln
– Teamarbeit: Brainstorming und Kritik
– Selbst Vorschlage machen und kritisieren lassen
• Fur Routineprobleme Bibliotheken durchforsten
• Klassen an externen Objekten orientieren
– Grobspezifikation liefert viele Mermale und Axiome
aber
– Daten, die sich nicht andern, sind keine Objekte
– Unnotige Klassen vermeiden
Entwurf zuverlassiger Software 73 Entwurfsmethoden
Kunde oder Erbe?
• Import bietet optimale Sicherheit
– saubere Schnittstelle, Kontrakt muß eingehalten werden
– weniger flexibel: nur qualifizierte Zugriffe
• Vererbung umgeht Datenkapselung
– alle Merkmale zugreifbar und veranderbar
– Kontrakt gilt nicht fur Erbenklassen
– globales Vererben kann OO-Struktur zerstoren
⇒ Konzeptioneller Bezug sollte entscheiden
– Erbenobjekte sind spezielle Objekte der Elternklasse
HILFSKRAFT ⊆ STUDENT ⊆ PERSON
– Kundenobjekte haben Lieferantenobjekte als Bestandteil
PERSON ‘ ∈’ BUCH (als Autor)
Abweichungen von diesem Prinzip konnen sinnvoll sein
– Effizienzgrunde oder extrem einfachere Schreibweise
Entwurf zuverlassiger Software 74 Entwurfsmethoden
Schnittstellentechniken
• Strikte Trennung von Prozeduren und Funktionen
– Funktionen sollen nur Werte berechnen
– Seiteneffekte in Funktionen vermeiden
• Datenbehalter aktiv gestalten
– mehr als nur Sammlungen von Information
– selbstandig arbeitender Betrieb (z.B. Cursor in Liste)
• Eine Schnittstelle fur mehrere Implementierungen
– Schnittstelle im Oberbegriff
– spezielle Implementierungen in Erbenklassen
• Mehrere Schnittstellen fur eine Implementierung
– Implementierung im (geheimen) Oberbegriff
– Verschiedene Schnittstellen fur verschiedene Sichten
Entwurf zuverlassiger Software 75 Entwurfsmethoden
Vererbungstechniken
Vererbung gezielt einsetzen
• Vererbung beschreibt Spezialfalle der Elternklasse
– In anderen Fallen Benutzung uber Schnittstellen verwenden
• Verallgemeinerungen erzeugen
– von Hand durch Editieren des Spezialfalls
– in spezielleren Klassen Erbklausel mit Redefinition einfugen
• Redefinition
– falls fur Erbenklasse effizientere Implementierung verfugbar
– Redefinition von Funktionen als Attribute sorgfaltig abwagen
– Semantik der redefinierten Routine muß erhalten bleiben
Entwurf zuverlassiger Software 76 Entwurfsmethoden
Bibliothekenverwaltung: Analyse I
• Bibliotheken– besitzen Bucher
– haben disjunkte Buchbestande
• Bucher– haben Autor, Titel, Themengebiet und Kennung
– sind entleihbar, Prasenzexemplar, Semesterapparat oder ausgeliehen
– Ausleihdaten: letztes Ausleihdatum, Ausleihfrist, Ruckgabedatum
– Ein Buch gehort zu genau einer Bibliothek
– Eine Bibliothek kann mehrere Exemplare eines Buchs(mit verschiedenen Kennungen) haben
– Mehrere Bibliotheken konnen das gleiche Buch enthalten.
• Entleiher– konnen entleihbare Bucher aus einer Bibliothek entnehmen,
deren Bibliotheksausweis sie besitzen
– konnen Bucher zu einer Bibliothek zuruckbringen
Entwurf zuverlassiger Software 77 Entwurfsmethoden
Bibliothekenverwaltung: Analyse II
• Bibliotheksmitarbeiter
– sind Entleiher
– konnen Bucher dem Bestand ihrer Bibliothek hinzufugen
– konnen Bucher aus dem Bestand ihrer Bibliothek entfernen
• Universitatsangestellte
– sind Entleiher
– konnen entleihbare Bucher und Prasenzexemplare entnehmen
• Hochschullehrer
– sind Universitatsangestellte
Entwurf zuverlassiger Software 78 Entwurfsmethoden
Bibliothekenverwaltung: Analyse III
• Ausleihe– Bucher werden nach Autor und Titel ausgeliehen
– Bucher konnen an Entleiher ausgeliehen werden, wenn∗ der Entleiher eine Bibliotheksausweis der Bibliothek besitzt
∗ die Bibliothek ein ausleihbares Exemplar besitzt
– Bucher konnen an Universitatsangestellte ausgeliehen werden, wenn∗ der Universitatsangestellte Zugang hat
∗ die Bibliothek ein ausleihbares Exemplar oder ein Prasenzexemplar besitzt.
– Ausleihdatum und die Ausleihfrist werden vermerkt
– Leihfrist: 4 Wochen nach Entleihdatum
– Leihfrist fur Hochschullehrer: ein Semester nach Entleihdatum
• Leihfrist verlangern– normalerweise um 4 Wochen – ein Semester fur Hochschullehrer
– Nur Entleiher selbst darf verlangern
• Ruckgabe– Jeder darf zuruckgeben
– Ruckgabedatum wird vermerkt
– Ruckgabe nur an Bibliothek, aus der entliehen wurde
Entwurf zuverlassiger Software 79 Entwurfsmethoden
Bibliothekenverwaltung: Analyse IV
• Entnahme von Exemplaren– Nur Mitarbeiter der Bibliothek durfen entfernen
– Entnahme nach Autor, Titel und Kennung
– Das Buch darf nicht entliehen sein
• Hinzufugen neuer Exemplare– Nur Mitarbeiter der Bibliothek durfen hinzufugen
– Hinzufugen nach Autor, Titel und Themengebiet
– Kennung wird automatisch vergeben, Ausleihdaten sind leer
• Allgemeine Verwaltung– Das Datum wird taglich angepaßt
– Datum ist von Hand verstellbar
– Transaktionen werden interaktiv angefordert
Vorzubereitende spatere Erweiterungen– Informationen uber Autoren in einem integrierten Informationssystem
– Erstellung diverser Verzeichnisse
– automatische Mahnungen
Entwurf zuverlassiger Software 80 Entwurfsmethoden
Bibliothekenverwaltung: Klassen des Systems
• Selbstandig agierenden Objekte der realen Welt
– Bibliothek,
– Buch
– Entleiher, Mitarbeiter, Universitatsangestellter, Hochschullehrer
• ‘Datenbanken’ fur Informationsspeicherung
– BuchDB, EntleiherDB, Bibliothekenliste
• Zentrale Verwaltung
– als Wurzelklasse
• Vorgesehene Erweiterung
– Autor, Autoreninformationssystem
Entwurf zuverlassiger Software 81 Entwurfsmethoden
Bibliothekenverwaltung: Verarbeitungsstruktur
Start: Datenbanken und Bibliotheken werden initiiert.
• Anwender wahlt Bibliothek, mit der er kommuniziert (Menu-Loop Verwaltung)
• Anwender gibt Buch zuruck oder identifiziert sich (Menu-Loop Bibliothek)
Bibliothek ladt internes Modell des Anwenders (Anfrage EntleiherDB)
Entleiherobjekt ubernimmt Transaktionsverwaltung mit Berechtigungen
• Anwender wahlt Transaktion und gibt Wunsche an (Menu-Loop Entleiher)
Entleiherobjekt ladt verfugbares Buch je nach Rechten (Anfrage BuchDB)
Entleiherobjekt legt Fristen fest je nach Rechten
Entleiherobjekt lost im konkreten Buch Eintragen der Daten aus
• Wiederholung der jeweiligen Menu-Loops bis Anwender beendet
Ende: Informationen werden gesichert (sofern nicht schon wahrend Transaktion)
Entwurf zuverlassiger Software 82 Entwurfsmethoden
Leistungen von VERWALTUNG und BIBLIOTHEK
Dienstleistung Kunde
VERWALTUNG SystemInit Bei Programmaufruf
Datum setzen mit Uhr
!!Bibliotheken.laden(datum)
!!AutorenInfo.Starten
MenuLoop starten
DatumSetzen(neu) ANWENDERBibliothekAuswahl im Menu ANWENDER!!Bibliotheken.selected.MenuLoop
SystemShutdown ANWENDERDatensicherung auslosen
BIBLIOTHEK Init(Datum,Kenndaten) VERWALTUNG!!BuchDB(.....)
!!EntleiherDB(.....)
MenuLoop VERWALTUNGRuckgabe(InvNr) VERWALTUNGBuchDB.Rucknahme(InvNr,Datum)
TransaktionStart VERWALTUNGNutzerId abfragen
!!EntleiherDB.entleiher(NutzerId).TMenu(BuchDB,Datum)
Entwurf zuverlassiger Software 83 Entwurfsmethoden
Leistungen von ENTLEIHER
Dienstleistung Kunde
Init.... nicht geplant
TMenu(BuchDB,Datum) BIBLIOTHEK
was soll geschehen? via ENTLEIH DB
Daten BuchDB,Datum ubernehmen
Frist(Datum) intern
nach Rechten setzen
Ausleih(Autor,Titel) BIBLIOTHEK
Akt Buch:=BuchDB.FreiesLeihExemplar(Autor,Titel)
Akt Buch.Ausleih(Frist(Datum))
Verlangerung(InvNr) BIBLIOTHEK
Akt Buch:=BuchDB.Exemplar(InvNr)
Akt Buch.Verlangern(Frist(Datum))
Entwurf zuverlassiger Software 84 Entwurfsmethoden
Leistungen der Erben von ENTLEIHER
Dienstleistung Kunde
MITARBEITER redefine TMenu(BuchDB,Datum) BIBLIOTHEK
erweitertes Angebot
Entnahme(InvNr) BIBLIOTHEK
BuchDB.Losche(InvNr)
NeuErwerb BIBLIOTHEK
BuchDB.NeuMenu
UNI ANG redefine Ausleih(Autor,Titel) BIBLIOTHEK
Akt Buch:=BuchDB.FreiesLeihExemplar(Autor,Titel)
im Falle eines Fehlschlags
Akt Buch:=BuchDB.FreiesPrasenzExemplar(Autor,Titel)
Akt Buch.Ausleih(Frist(Datum))
PROFESSOR redefine Frist(Datum) intern
erweiterte Rechte
Entwurf zuverlassiger Software 85 Entwurfsmethoden
Leistungen von BUCH DB
Dienstleistung Kunde
Start BIBLIOTHEKInitialisierung des DBMS
Fiktives Laden aller Bucher
Rucknahme(InvNr,Datum) BIBLIOTHEKBuch:=Exemplar(InvNr)
Buch.Rucknahme(Datum)
FreiesLeihExemplar(Autor,Titel) ENTLEIHERsuche Exemplar mit Status ‘entleihbar’
FreiesPrasenzExemplar(Autor,Titel) UNI ANGsuche Exemplar mit Status ‘Prasenzexemplar’
Exemplar(InvNr) ENTLEIHERsuche Exemplar mit Inventarnummer im Bestand
Losche(InvNr) MITARBEITEREntferne Buch mit Inventarnummer aus Bestand
NeuMenu MITARBEITER!!Buch.InitMenu
Hinzunahme des erzeugten Buchs in den Bestand
Entwurf zuverlassiger Software 86 Entwurfsmethoden
Leistungen von BUCH
Dienstleistung Kunde
InitMenu BUCH DB
Abfrage von Daten des neuen Buchs
Erzeugung eines entsprechenden Objekts
Rucknahme(Datum) BUCH DB
Status:=StatusVorAusleih
RuckDatum:=Datum
Ausleih(Frist) ENTLEIHER
StatusVorAusleih:=Status
Status:=‘ausgeliehen’
Leihfrist:=Frist
Verlangern(Frist) ENTLEIHER
Leihfrist:=Frist
Status BUCH DB
Angabe des Leihstatus
...andere Komponenten mitteilen...
Entwurf zuverlassiger Software 87 Entwurfsmethoden
Formalisierung exemplarischer Zusicherungen
• Bucher sind entleihbar, ausgeliehen, Prasenzexemplar oder SemesterapparatInvariante der Klasse BUCH
Status=‘entleihbar’ or Status=‘ausgeliehen’
or Status=‘Prasenzexemplar’ or Status=‘Semesterapparat’)
• Die Leihfrist eines Buches betragt 4 WochenNachbedingung von Frist bei ENTLEIHER
ensure TagesDiff(Result,Datum) ≥ 28
Zugestandnis an Erweiterbarkeit: man darf mindestes 4 Wochen ausleihen
Hochschullehrer durfen maximal ein Semester ausleihenErweiterte Nachbedingung von Frist bei PROFESSOR
ensure then TagesDiff(Result,Datum) ≥ 183
• Ausleihbare Exemplare durfen verliehen werdenVorbedingung von Ausleih bei ENTLEIHER (Nicht gut zu modellieren)
require Ausleih Buch(Autor,Titel).Status=‘entleihbar’
Universitatsangestellte durfen auch Prasenzexemplare ausleihenErweiterte Vorbedingung von Ausleih bei UNI ANG
require else Ausleih Buch(Autor,Titel).Status=‘Prasenzexemplar’
Viele andere Randbedingungen codiert in der Struktur
Entwurf zuverlassiger Software 88 Entwurfsmethoden
Asthetik der Programmierung
• Struktur fur Andere uberschaubar halten
– Bezug zur Realitat aufrecht erhalten (Namensgebung!)
– Zusicherungen nur mit exportierten Features formulieren
– Sich der Kritik anderer stellen
• Verzicht auf Tricks zur Effizienzsteigerung
. . . solange dies keine signifikanten Verbesserungen bringt
– Standardmethoden verwenden
– Code einzelner Routinen klein halten
– wenn Tricks unvermeidbar, dann ausfuhrlich dokumentieren
• Programmidee muß ersichtlich bleiben
– Korrektheit leichter erkennbar
– Verifikation leichter durchfuhrbar
Entwurf zuverlassiger Software
Lektion 6
Das OMT Objektmodell
1. Klassen, Objekte und Methoden
2. Beziehungen zwischen Objektklassen
3. Diagrammtechniken
Entwurf zuverlassiger Software 91 OMT Objektmodell
OMT: Objekt Modelling Technique (Rumbaugh, 1991)
Technik zur Beschreibung von Softwareentwurfen
• Modellbildung im Zentrum der Softwareentwicklung– Implementierungsdetils werden spater hinzugefugt
• Graphische Darstellung von Modellen der Wirklichkeit– Abstrakte Beschreibung, was das System leisten soll– Unterstutzt Entwurfsphasen von Analyse bis Implementierung– Uberschaubar durch reduzierte Komplexitat– Grundlage fur Architekturentwurfe und computernahe Modellierung– Kommunikationshilfe fur Kontakt mit Anwendern
• Diagrammkonzepte als Hilfsmittel zur Darstellung– sprachunabhangige Reprasentation vermeidet Uberspezifikation– Formalismus als Notationshilfe – sollte i.w. selbsterklarend sein– Naturliche Sprache als Erganzung, wenn Formalismus nicht greift– Unterstutzt durch Werkzeuge zur Entwicklung von Diagrammen am Bildschirm
• Methodik zur Einhaltung von Entwurfsleitlinien– Vorschlage fur Entwicklungsschritte– Prozeß nicht automatisierbar – Abwagen und Beurteilen erforderlich
Entwurf zuverlassiger Software 92 OMT Objektmodell
Konzepte zur Modellierung von Problemstellungen
System wird von drei Sichten aus modelliert
• Objektmodell: Wer ist beteiligt, was wird angeboten?
– Statische Strukturen und Daten– Objektklassen, Attribute, Beziehungen, Operationen und MethodenDarstellung graphisch durch Objektdiagramm
• Dynamisches Modell: Was geschieht, mit wem, in welcher Reihenfolge?
– Verhaltens- und Kontrollaspekte (Interaktionen, zeitliche Abfolgen)– Ereignisse (Events), Kontext (Zustande von Objekten) und ausgeloste AktionenDarstellung graphisch durch Zustandsdiagramme
• Funktionales Modell: Was soll getan werden?
– Zustandsveranderungen, Wertveranderungen, Abbildungen– Spezifikation von Algorithmen und ProzessenDarstellung graphisch durch Datenflußdiagramme (zwischen Prozessen)
• Kombination der Sichten ausgehend vom Objektmodell– einheitliche Notation und Sprechweise– jeder Teilaspekt fur sich alleine verstandlich
Entwurf zuverlassiger Software 93 OMT Objektmodell
Objektdiagramme: Klassen und Objekte
Graphische Notation fur Objekte, Klassen und Beziehungen
• Klassendiagramm– Beschreibung der Beziehungen zwischen Objektklassen– korrespondiert zu unendlicher Menge von Instanzendiagrammen
• Instanzendiagramm– Beschreibung der Beziehungen zwischen konkreten Objekten– Darstellung von Testfallen, Szenarien, Beispielen
• Attribute dargestellt als Teil einer Objektklasse– korrespondieren zu konkreten Werten in einer Instanz– optionale Angabe von Typ und Defaultwert– sollen Attributen der realen Welt entsprechen (keine Navigationsdaten)– Kennzeichnung von Schlusselattributen moglich: candidate key: (A
1,..,An)
Person
Name:string
GebDatum:date
key: (Name,GebDatum)
Klasse mit Attributen
(Person)
Michael Jordan
3.2.1960
'
&
$
%(Person)
David Robinson
6.9.1963
'
&
$
%Instanzen mit Werten
• Kennzeichnung abgeleiteter Objekte und Attribute
Entwurf zuverlassiger Software 94 OMT Objektmodell
Objektdiagramme: Operationen und Methoden
• Funktion/Transformation auf Objekten einer Klasse– Aktuelles Objekt der Klasse als implizites Argument (Zielobjekt)– zusatzliche Argumente (in Klammern) und Ergebnistyp (nach ‘:’) moglich– dargestellt als dritter Teil einer Objektklasse
Datei
Dateiname:string
GroßeByte:int
Geandert:date
GeoObjekt
Farbe
Position
move(delat:array)
sel(p:Point):Boolean
rotate(angle)
• Polymorphismus– Operationen durch Vererbung auf mehrere Klassen anwendbar– verschiedene Implementierungen in Subklassen (Methoden) moglich
dieselbe Operation ist auf verschiedene Weisen ausfuhrbar– Signatur und Integritatsbedingungen mussen erhalten bleiben– dynamisches Binden: Klasse des Zielobjekts bestimmt angewandte Methode
• Operationen mit und ohne Nebeneffekte– Funktionen/Queries = Operationen ohne Nebeneffekte– Abgeleitete Attribute = Queries ohne Parameter
Entwurf zuverlassiger Software 95 OMT Objektmodell
Objektdiagramme: Relationen
• Beziehung: Relation zwischen Objektklasse– mogliche Beziehungen und Zugriffspfade zwischen Objekten
– orig. ‘Association’
– meist bidirektional – Name gibt Semantik der Vorwarts-Richtung
– Graphische Reprasentation als Linie mit Namen
Land
Name
hat-Hauptstadt Stadt
Name
– Bei 3- und mehrstelligen Beziehungen Raute wie im ERM
• Link: Relation zwischen Objektinstanzen– tatsachliche Beziehungen und Zugriffspfade zwischen Objekten
(Land)
Kanada
'
&
$
%hat-Hauptstadt (Stadt)
Ottawa
'
&
$
%(Land)
Frankreich
'
&
$
%hat-Hauptstadt (Stadt)
Paris
'
&
$
%(Land)
Deutschland
'
&
$
%hat-Hauptstadt (Stadt)
Berlin
'
&
$
%
Entwurf zuverlassiger Software 96 OMT Objektmodell
Multiplizitat von Beziehungen
Anzahl von Objekten einer Klasse, die mit
demselben Objekt einer anderen in Beziehung stehen
• Deklaration als Zahl, Intervall oder Aufzahlung
• Graphische Darstellung zusatzlich mit Punkten– schwarzer Punkt •: ‘mehrere’ – 0 oder mehr Teilnehmer
– weißer Punkt : ‘optional’ – 0 oder 1 Teilnehmer
– kein Punkt: ‘eins’ – 1:1 Beziehung
– mehrdeutig bei ternaren Beziehungen (!!)
PKW
Hersteller:string
Typ:L,C
Baujahr:int
hat•
2,4
Tur
Teilnr:int
Elektro:Boolean
ein normaler PKW hat 2 oder 4 Turen
• Sorgffaltig aber nicht ubergenau beschreiben
Entwurf zuverlassiger Software 97 OMT Objektmodell
Attribute von Beziehungen
• Beziehungen konnen eigene Attribute haben
– dargestellt als Box, die durch einen Halbkreis verbunden ist
Person
Ausweisnr
Name
Adresse
arbeitet-bei
• & %Gehalt
Titel
Firma
Name
Adresse
• Attribute, die von Beziehungen zwischen 2 Klassen abhangen, sollen als
Beziehungsattribute, nicht als Klassenattribute modelliert werden
– Gehalt, Titel gehort zum Arbeitsverhaltnis, nicht zur Person
– wichtig bei m:n Beziehungen, sonst integrierbar in Klasse
Entwurf zuverlassiger Software 98 OMT Objektmodell
Rollen und Ordnung in Beziehungen
• Rollenname: Bezeichnung fur eine Komponente einer Beziehung
– eindeutige Klassifizierung beteiligter Objekte
– entspricht abgleitetem ‘Attribut’ der anderen Klasse (nur binar!)
– graphisch am jeweiligen Ende notiert
– besonders wichtig bei Beziehungen zwischen Objekten derselben Klasse
Person
Ausweisnr
Name
Adresse
arbeitet-bei
Arbeitnehmer Arbeitgeber•Firma
Name
Adresse
• Ordnung
– Kennzeichnung, daß die Instanzen in der Beziehungen geordnet sind
– z.B. Reihenfolge der Fenster auf einem Bildschirm im Window-Manager
WINDOWSsichtbar-auf
geordnet• Bildschirm
Entwurf zuverlassiger Software 99 OMT Objektmodell
Qualifizierte Beziehungen
Reduziere effektive Multiplizitat einer Beziehung
Directory Filenameenthalt File
Attribut Filename qualifiziert Beziehung enthalt
– Filename ist Qualifikator fur Directory
– Klasse Directory wird implizit um Qualifikator-Attribut erweitert
– Anzahl der File-Objekte, die mit einem Objekt der ‘erweiterten’ Klasse
in Beziehung stehen, sinkt (manchmal sogar auf 1)
– Partitionierung: Informationsgehalt der Beziehung enthalt steigt
(1:1–Beziehung zwischen Directory+Filename und File)
⇒ Navigationswege besser erkennbar
Nur moglich bei 1:n und m:n-Beziehungen
Entwurf zuverlassiger Software 100 OMT Objektmodell
Generalisierung
Abstraktionsmechanismus zur Beschreibung von Ahnlichkeiten
E
E1
E2 . . . En
AA Diskriminator• Beziehung mit IS A Semantik
– Graphisch dargestellt durch Dreieck in Beziehungslinie
– E generalisiert Ei (Ei spezialisiert E)
– Diskriminator: Attribut von AA = Grundlage der Generalisierung
– Elemente von Ei sind Elemente von E
– Unterklasse Ei erbt Attribute und Operationen (Features) von Oberklasse E
– Unterklassen durfen Features einschranken (Restriktion)
– Unterklassen durfen neue Features einfuhren (Erweiterung)
• Transitive Beziehung E1
HHH
E2
HHH
E3
– E1 generalisiert E2 und E3
– Kurze Generalisierungshierarchien empfehlenswert
⇒ Entwurf wird ubersichtlicher, Performanz der Implementierung besser
Reduziert Anzahl unabhangiger Konzepte
Erhoht Wiederverwendung von Programmcode
Entwurf zuverlassiger Software 101 OMT Objektmodell
Generalisierungshierarchie in OMT
OMT Bild 3.24 Seite 41 150%
Entwurf zuverlassiger Software 102 OMT Objektmodell
Redefinition
Veranderung von Features der Vorfahren
• Redefinition bei Erweiterung– Erbenklasse erganzt Attribute (⇒ Operationen mussen ggf. mehr tun)– zusatzliche Effekte fur neue Attribute der Erbenklasse
• Redefinition bei Restriktion– Erbenklasse beschrankt Attributwerte– Abschlußeigenschaften verlangen Typeinengung von Argumenten– Protokoll der Vorfahren darf nicht zu spezifisch sein
• Redefinition zur Optimierung– effizientere Losung fur spezielle Situationen– identische Resultate mit speziellerer Methode
• Redefinition der Einfachheit halber (Mißbrauch!!)– Ahnliche Klassen ‘beleihen’ / unbrauchbare Features anpassen
• Semantische Regeln fur Vererbung– Alle Queries werden i.w. unverandert vererbt– Anderungsoperationen an Erweiterungen vererbbar– Operationen, die beschrankte Attribute andern, in Restriktionen abblocken– Redefinition muß Signatur und Protokoll der Vorfahren einhalten
Entwurf zuverlassiger Software 103 OMT Objektmodell
Mehrfach-Generalisierung
Fahrzeug
AA
L-Fzg
AA
W-Fzg
AA
PKW Amphibie Boot
• Klasse erbt von mehreren Oberklassen– Subklasse ist Join-Klasse (Summe aller Features)
– Identische Features eines Ahnen werden nur einmal geerbt
– Mehrdeutigkeiten und Konflikte explizit auflosen (!)
• Uberlappende Erben-Klassen (gemeinsame Objekte)– Dargestellt durch schwarzes Dreieick AA
• Disjunkte Erben-Klassen (keine gemeinsamen Objekte)– Dargestellt durch leeres Dreieick AA
Entwurf zuverlassiger Software 104 OMT Objektmodell
Abstrakte Klassen
Klasse• •
AAA
Instanz • -hat
Instanzen konkret
AAA
abstrakt •
mit Erben•
hat Unterklassenhat Unterklassen
Oberklasse
Oberklasse
Unterklasse Unterklasse
Blatt
• Klassen ohne eigene Instanzen– Nachkommenklassen sind konkret (mit Instanzen)
• Definition allgemeiner Methoden– vollstandig implementiert zur Weitergabe an Erben– Methode unabhangig vom Spezialfall aber keine allgemeinen Objekte
• Spezifikation abstrakter Operationen– Signatur, Kontrakt (Protokoll), aber keine Implementierung moglich– Erbenklassen realisieren konkrete Implementierung
Entwurf zuverlassiger Software 105 OMT Objektmodell
Aggregation
E
E1
E2 . . . En
@@@@
• Beziehung mit PART-OF Semantik– Ei sind Komponenten der Aggregatsklasse E
– Graphisch dargestellt durch Raute am Aggregatsende der Beziehung
• Transitive und antisymmetrische Beziehung– Teile von Teilen sind selbst Teile
– Formal: Beziehung zwischen einem einzelnen Ei und E
• Propagation von Features auf Komponenten moglich– Autoteile bewegen sich, wenn Auto sich bewegt
PKW
Hersteller:string
Typ:L,C
Baujahr:int...
@@@@
bewegt-
hat •
Tur
Teilnr:int
Elektro:Boolean...
• Vorsichtig einsetzen– nur wenn Teil-Beziehung deutlich und gemeinsame Eigenschaften erkennbar
Entwurf zuverlassiger Software 106 OMT Objektmodell
Aggregation vs. Generalisierung
OMT Bild 4.2 Seite 59 200%
Aggregation: ‘UND’ Beziehung zwischen verschiedenen Instanzen
Generalisierung: ‘ODER’ Beziehung zwischen Klassen (gleiche Instanzen)
Entwurf zuverlassiger Software 107 OMT Objektmodell
Klassifizierung von Aggregatsklassen
• Feste Aggregatsklasse– Anzahl und Typ der Komponenten eines Objektes fixiert
(eine Lampe besteht aus einem Fuß, einem Schirm, einem Schalter, . . . )
• Variable Aggregatsklasse– Objekte haben verschiedene Anzahlen von Komponenten
Firma @@@@ • Abteilung
• Rekursive Aggregatsklasse– Objekte der gleichen Klasse sind Komponenten
– Terminierung durch Unterklasse einer Komponente
– Kombination von Generalisierung und Aggregation
Program
@@@@
•Block•
@@@@ Compound Statement
AAA
Entwurf zuverlassiger Software 108 OMT Objektmodell
Constraints (Integritatsbedingungen)
Einschrankungen an Objekte und Beziehungen
• Strukturelle Constraints– Schlussel fur Klassen und Beziehungen
– Multiplizitaten und Ordnung fur Beziehungen
Student
Universitat
betreut
HHHH
HHHH
Professor
key:(Student,Universitat)• Logische Constraints– Einschrankung der Werte von Attributen
– auch zwischen zwei Objekten oder zwei Beziehungen
– Gleiche Notation constraint, ggf. mit gepunkteter Verbindungslinie
– Formuliert in Formeln oder naturlicher Sprache
Angestellter
Gehalt:int •
chef
Gehalt ≤ chef.Gehalt
Fenster
lg:int
br:int
0.8 ≤ lg/br ≤ 1.5
Person•
•
•Mitglied
Vorsitz
Teilmenge6
Komitee
Entwurf zuverlassiger Software 109 OMT Objektmodell
Entwurfshilfen fur komplexe Diagramme
• Module: logische Strukturierung eines Datenmodells
– reprasentiert uberschaubare Teilansicht auf das Problem
– Logische Untereinheit eines Datenmodells
– Gruppierung konzeptionell zusammengehoriger Klassen und Beziehungen
– Kennzeichnung nur durch Modulnamen
– Bezeichner innerhalb eines Moduls mussen verschieden sein
– Empfehlung: Anzahl der Beziehungen zwischen Modulen klein halten
Darstellung im Modul durch Referenz auf externe Klasse
• Sheets: notationelle Strukturierung eines Moduls
– Aufteilung eines Moduls auf druckbare Seiten
– Gruppierung graphisch zusammengehoriger Klassen und Beziehungen
– Kennzeichnung mit Namen oder Nummer
– Schnittklassen auf mehreren Sheets zeigen – Beziehungen nur auf einem Sheet
– Empfehlung: Anzahl der Schnittklassen (auf mehreren Sheets) klein halten
Kennzeichnung: Namen fremder Sheets in Kreisen neben Schnittklassen
Entwurf zuverlassiger Software 110 OMT Objektmodell
Tips fur den Entwurf von Objektdiagrammen
• Erkennbarer Bezug zur Realitat– Versuche, das zu modellierende Problem genau zu verstehen
– Gestalte das Modell einfach und selbsterklarend
– Wahle Namen sorgfaltig
• Spezielle Aspekte– Keine Implementierungsdetails im Modell (Pointer sind keine Attribute!)
– Vermeide Beziehungen vom Grad 3 oder hoher (zerlegen!)
– Beziehungsattribute nicht als Klassenattribute darstellen
– Multiplizitaten zu Beginn nicht zu genau fixieren (Uberspezifikation droht)
– Qualifikatoren so oft wie moglich einsetzen
– Zu lange Generalisierungsketten vermeiden
– 1:1 Beziehungen kritisch uberprufen (total oder partiell?)
• Allgemeine Arbeitsmethodik– Nicht alle OMT-Konstrukte konnen sinnvoll eingesetzt werden
– Entwurf mehrmals uberarbeiten
– Andere den Entwurf beurteilen lassen (vielleicht beteiligen sie sich)
– Modelle dokumentieren (wie ist es zu lesen, warum so und nicht anders?)
Entwurf zuverlassiger Software 111 OMT Objektmodell
Dynamisches Modell
Diagramm moglicher Veranderungen von Objekten
• Ereignisse (Ereignisklassen) = externe Stimuli– z.B. Abflug oder Ankunft von Flugen, Schneefall, Eingabe einer Geheimzahl– nebenlaufig, wenn ohne gegenseitige Einflusse (kausale Unabhangigkeit)
• Szenario: Hilfsmittel zur Identifikation von Ereignissen– typische Folge von Ereignissen mit betroffenen Objekten, incl. Fehler-/Sonderfalle
• Zustande = Werte von Objekten und Links
• Operationen– Reaktion eines Objekts auf ein Ereignis, beeinflußt durch Zustand– Aktivitat (andauernde Handlung) = Folgezustand– Aktion (unmittelbar beendete Handlung) = Zustandsubergang (Transition)
• Zustandsdiagramm fur Klassen mit wichtigem dynamischem Verhalten– Knoten = Zustande, Kanten = von Ereignis ausgeloste Transition
+ Constraints fur Einschrankung von Transitionen
+ Verschachtelung, Generalisierung, Nebenlaufigkeit, Synchronisation
⇒ Modellierung von Kontrolle– Folge von Operationen, die als Konsequenz von Ereignissen auftreten
Entwurf zuverlassiger Software 112 OMT Objektmodell
Zustandsdiagramm
Bild 5.10, S.94 120%
Entwurf zuverlassiger Software 113 OMT Objektmodell
Funktionales Modell
• Datenflußdiagramm– Mogliche Verarbeitungspfade der Ein- und Ausgaben von Prozessen
• Prozeß: Transformation von Daten durch Berechnung– Funktional (ohne Seiteneffekte) oder prozedural– mussen durch Operationen auf Objekten realisiert werden
• Datenfluß: Weitergabe von Daten zwischen Prozessen
• (aktive) Aktoren erzeugen oder ‘verbrauchen’ Daten(passive) Datenspeicher speichern Daten fur spatere Zugriffe
• Kontrollfluß:– (Boolesche) Entscheidungen, welche Aktivierung von Prozessen kontrollieren– Kriterien zur Auswahl tatsachlicher Verarbeitungspfade
⇒ Spezifikation von Operationen– Zugriffe, Queries, Aktionen oder Aktivitaten– Beschreibe Zusammenhange zwischen Ein- und Ausgabe ohne zeitliche Abfolge
durch Funktionen, Tabellen, Gleichungen, Vor-/Nachbedingungen, Pseudocode, nat. Sprache
Entwurf zuverlassiger Software 114 OMT Objektmodell
Datenflußdiagramm
Bild 6.9, S.134 120%
+ Vorgriff auf Folie OMT Methodik aus Lektion 7
Entwurf zuverlassiger Software
Lektion 7
Objektorientierter Entwurf mit OMT
1. Die OMT Entwurfsmethdik
2. OMT Problemanalyse
– Entwurf von Objektmodellen
– Entwurf von dynamischem und funktionalem Modell
3. Entwurfsschritte bis zur Implementierung
Entwurf zuverlassiger Software 115 Entwurf mit OMT
OMT Methodik: Unterstutzung der
Softwareentwicklung
Nutzung von Konzepten beim Entwurf von Modellen
• Analyse: Problem verstehen und prazisieren
– Problemformulierung fur konzeptuellen Uberblick
+ Nutzerinterview, Allgemeinwissen, Kenntnisse uber Anwendungsbereich
⇒ Formales Objektmodell + Dynamisches Modell + Funktionales Modell
• Systementwurf: Gesamtarchitektur fixieren
– Aufteilung in Subsysteme auf Basis des Objektmodells
– Nebenlaufigkeit, Kommunikation, Datenspeicherung, Prioritaten
– Realisierung des dynamischen Modells
• Objektentwurf: Computernahe Modellierung
– Abbildung der Analysemodelle durch effiziente Strukturen
– Algorithmen und Datenstrukturen zur Reprasentation der Konzepte
Entwurf zuverlassiger Software 116 Entwurf mit OMT
Ausgangspunkt: Problemformulierung
• Wichtige Anforderungen– Problembereich, Kontext, Annahmen
– Notwendige und optionale Leistungen des gewunschten Systems
– Performanzanforderungen
• Legitime Anforderungen– Modularitat, Erweiterbarkeit, Testbarkeit
– Programmiersprache (Kompatibilitat, . . . )
• Pseudoanforderungen (unnotige Beschrankungen)– Entwurfs- und Implementierungsdetails
(Architektur, Algorithmen, Datenstrukturen)
– Uberspezifizikation
• Nur ein erster Ausgangspunkt– mehrdeutige oder unvollstandige Anforderungen?
– inkonsistente und falsche Anforderungen?
– nicht realisierbare Anforderungen?
⇒ standige Kommunikation mit Auftraggeber erforderlich
Entwurf zuverlassiger Software 117 Entwurf mit OMT
Leitbeispiel: Verwaltung von Geldautomaten
Fig 8.3, S151 – 140%
Entwurf zuverlassiger Software 118 Entwurf mit OMT
Analyse
Wichtigste Phase der Softwareentwicklung
• Ziel: Prazisierung der Problemformulierung– Was soll getan werden? (keine Details zum ‘wie’)
– Voraussetzungen + Konsequenzen verstehen und formulieren
– Mißverstandnisse ausraumen
– Abstrakte Darstellung: was soll getan werden?
⇒ Prazises, verstandliches, korrektes Modell der Wirklichkeit
• Analyse aus drei Sichten– Statische Struktur (Objektmodell) – Abbildung der realen Welt
+ Abfolge moglicher Interaktionen (Dynamische Modell)
+ Veranderung von Daten (Funktionales Modell)
Liefert Objektstruktur und notwendige Operationen
• Analyse nicht mechanisierbar– Kommunikation und Visualisierung wichtig
Entwurf zuverlassiger Software 119 Entwurf mit OMT
Entwurf von Objektmodellen
• Wichtigster Bestandteil der Problemanalyse
– Funktionales und dynamisches Modell abhangig von statischer Struktur
– statische Struktur klarer zu definieren
– statische Struktur unabhangig von Details, stabiler bei Modifikationen
• Diagramme unterstutzen Kommunikation
– zwischen Software- und Anwendungsspezialisten
– wichtig, wenn Anforderungen zu klaren sind
• Schrittweise Modellierung – ausgehend von Klassen
– Identifiziere (unabhangige) relevante Klassen des Problems
– Identifiziere (unabhangige) relevante Beziehungen
– Identifiziere (unabhangige) relevante Attribute
– Verfeinere Klassenstruktur mit Generalisierung
– Revision und Iteration des Entwurfs
– Aufteilung in Module und Sheets
Entwurf zuverlassiger Software 120 Entwurf mit OMT
Bestimmung sinnvoller Klassen
Einfache Reprasentation wichtiger Grundkonzepte
• Identifiziere mogliche Objektklassen– Kandidaten aus Problemformulierung extrahieren (Substantive)– Erganze Klassen des Anwendungsbereichs mit moglichem Bezug
• Eliminiere uberflussige und inkorrekte Klassen– Redundante Klassen – die aussagekraftigste Klasse behalten– Irrelevante Klassen (wenig Bezug zum Problem)– Unklare Klassen (unscharfe Abgrenzung, zu groß)– Attribute (keine unabhangige Existenz)– Operationen (die nicht selbst manipuliert werden)– Rollenbezeichner – verallgemeinern– Implementierungskonstrukte (kein echtes Objekt der Außenwelt)Grundliches Abwagen bei der Beurteilung erforderlich
• Entwerfe Begriffslexikon– Definierende Texte vermeiden Fehlinterpretationenvon Namen– erklare Einflußbereich, Annahmen, mogliche Einschrankungen
Attribute, Beziehungen und mogliche Operationen
Entwurf zuverlassiger Software 121 Entwurf mit OMT
ATM Netzwerk: mogliche und sinnvolle Objektklassen
Fig 8.5/6 200% – LIVE farbig umrahmen, Farben unten vorbereiten
— Irrelevant — Redundant — Undeutlich
— Implementierungsnah – Attribute
Entwurf zuverlassiger Software 122 Entwurf mit OMT
Bestimmung sinnvoller Beziehungen
• Identifiziere mogliche Beziehungen– Kandidaten aus Problemformulierung extrahieren
Verben und Aussagen uber Ort, Aktion, Kommunikation, Besitz, . . .– Erganze implizite und vermutete Beziehungen (Rucksprache!)
• Eliminiere uberflussige und inkorrekte Beziehungen– Beziehungen zwischen eliminierten Klassen – ggf. umformulieren– Irrelevante oder implementierungsbezogene Beziehungen– Operationen – ggf. umformulieren– Ternare Beziehungen – wenn moglich aufbrechen oder qualifizieren– Abgeleitete Beziehungen (oft bei mehreren Beziehungen zwischen zwei Klassen)
• Prazisiere die Semantik von Beziehungen– Namensgebung uberprufen (wie ist die Beziehung)– Rollennamen erganzen (wenn nicht eindeutig im Namen der Beziehung)– Sinnvolle Qualifikatoren erganzen– Multiplizitaten erganzen (1:1 Beziehungen uberprufen!)– Gibt es Ordnungen auf der “viele’-Seite einer Beziehung?– Offensichtlich ubersehene Beziehungen erganzen
Entwurf zuverlassiger Software 123 Entwurf mit OMT
ATM Netzwerk: mogliche Beziehungen
Fig 8.9 160%, dann markiere was gestrichen/verandert wird
Entwurf zuverlassiger Software 124 Entwurf mit OMT
ATM Netzwerk: Erstentwurf eines Objektmodells
Fig 8.11 160%,
Entwurf zuverlassiger Software 125 Entwurf mit OMT
Bestimmung sinnvoller Attribute
• Identifiziere mogliche Attribute
– Kandidaten aus Problemformulierung extrahieren (Eigenschaften)
– Aus Anwendungsbereichs- und Alltagswissen erganzen
– Auf wesentliche Attribute konzentrieren – Details konnen spater hinzukommen
• Eliminiere uberflussige und inkorrekte Attribute
– unabhangig existierende Objekte (abhangig von Anwendunsgzielen)
– Qualifikatoren – sollten in die Beziehung verlagert werden
– Namen und Bezeichner sind meist Qualifikatoren – verlagern
– Identifikatoren (sind Implementierungsdetails)
– Beziehungsattribute – als solche auch darstellen
– Interne Werte (die außen nicht sichtbar werden)
– Details, die wenig Einfluß auf Operationen haben werden
– Attribute mit wenig Bezug zu anderen Attributen – Klasse aufspalten?
Entwurf zuverlassiger Software 126 Entwurf mit OMT
ATM Netzwerk: Objektmodell mit Attributen
Fig 8.12 140%,
Entwurf zuverlassiger Software 127 Entwurf mit OMT
Verfeinerung der Struktur durch Generalisierung
• Bottom-Up: Gemeinsame Aspekte generalisieren
– Klassen mit ahnlichen Attributen, Beziehungen und Operationen suchen
– Oberklasse definieren, wenn konzeptionelle Bezuge vorhanden
– Oberklasse moglichst an Begriffen der Realitat orientieren
– Attributen, Beziehungen und Operationen nach oben verlagern
• Top-Down: Spezielle Unterklassen erzeugen
– Adjektive mit Bezug zu modellierter Klasse (Aufzahlungen) extrahieren
– Attribute und Beziehungen fur Spezialfalle erganzen
– Vermeide Uberspezialisierung
– Mehrfachvererbung vorsichtig einsetzen
Entwurf zuverlassiger Software 128 Entwurf mit OMT
ATM Netzwerk: Objektmodell mit Generalisierung
Fig 8.13 125%,
Entwurf zuverlassiger Software 129 Entwurf mit OMT
Revision und Iteration des Entwurfs (I)
• Zugriffspfade analysieren
– Gibt es sinnvolle Fragen, die das Modell nicht beantwortet?
z.b. ”Auf welchem Pfad erhalte ich bestimmte Werte?”
– Gibt es einfache Zusammenhange, die im Modell kompliziert erscheinen?
• Anzeichen fur fehlende Klassen
– Assymmetrien in Beziehungen und Generalisierung – analoge Klassen erganzen
– Attribute mit wenig Bezug zu anderen Attributen – Klasse aufspalten?
– Saubere Generalisierung schwierig (Klasse mit zwei Rollen?) – aufspalten
– Operation ohne gute Zielklasse – erganzen
– Mehrere Beziehungen mit gleicher Semantik – Klassen generalisieren
– Rolle mit starkem Einfluß auf eine Klasse – Rolle zur Klasse umwandeln
• Anzeichen fur uberflussige Klassen
– Keine sinnvollen Attribute, Operationen und Beziehungen (wofur ist sie gut?)
Entwurf zuverlassiger Software 130 Entwurf mit OMT
Revision und Iteration des Entwurfs (II)
• Anzeichen fur fehlende Beziehungen
– Fehlende Zugriffspfade fur Ausfuhrung einer Operation – erganze Beziehung
• Anzeichen fur uberflussige Beziehungen
– Redundante Informationen – entfernen oder als abgeleitet kennzeichnen
– Keine Operationen, welche sie benutzen – kennzeichnen, spater ggf. entfernen
• Anzeichen fur falsch plazierte Beziehungen
– Rolle fur Klasse zu eng oder breit – in Generalisierungshierarchie verlagern
• Anzeichen fur falsch plazierte Attribute
– Objekt nur uber Attribut erreichbar – umwandeln in Qualifikator
Erstentwurfsphasen konnen bereits Revisionsschritte enthalten
Entwurf zuverlassiger Software 131 Entwurf mit OMT
ATM Netzwerk: Objektmodell nach Revision
Fig 8.14 140%, Farbig gestalten fur Module
Entwurf zuverlassiger Software 132 Entwurf mit OMT
Entwurf eines dynamischen Modells
• Entwerfe Szenarien fur typische Interaktionsfolgen– Typische Dialoge zwischen Benutzer und System
– Zuerst normale Falle, spater seltene Extremfalle und Fehlersituationen
– Aktoren (System, Benutzer, externe Stimuli) und Parameter identifizieren
– Darstellungsformate sind unabhangig von Kontrolle (7→ separat behandeln)
• Identifiziere Ereignisse in Szenarien– Sichtbare Stimuli (Signal, Eingabe, Entscheidung, Unterbrechung, Transition, Aktion)
– Klassifiziere Ereignisse mit gleichem Effekt auf Kontrollfluß
– Weise jeder Ereignisklasse Sender- und Empfangerobjekte zu
• Beschreibe Fluß der Ereignisse in den Szenarien– Event-Traces: geordnete Liste von Ereignissen fur jede Objektklasse
– Ereignisflußdiagramm: welche Ereignisse beruhren welche Module
• Darstellung im Zustandsdiagramm
Entwurf zuverlassiger Software 133 Entwurf mit OMT
Dynamisches Modell: Entwurf eines
Zustandsdiagramms
• Nur fur Klassen mit wichtiger Dynamik
– Extrahiere aus Folge von Events aus Event-Trace
– Knoten (Zustand) = Intervall zwischen Ereignissen, Kante = Event
– Ersetze lange Ereignisfolgen durch Schleifen
– Integriere weitere Szenarien – isb. Extremfalle und Fehlersituationen
• Uberprufe Konsistenz und Vollstandigkeit
– Generiere neue Szenarien aus Lucken in Zustandsdiagrammen
– Vergleiche Ereignisse, die in mehreren Zustandsdiagrammen vorkommen
– Prufe Synchronisation abhangiger Ereignisse
Entwurf zuverlassiger Software 134 Entwurf mit OMT
ATM Netzwerk: Event-Trace
Fig 8.18 100%,
Entwurf zuverlassiger Software 135 Entwurf mit OMT
ATM Netzwerk: Ereignisflußdiagramm
Fig 8.19 160%,
Entwurf zuverlassiger Software 136 Entwurf mit OMT
ATM Netzwerk: Zustandsdiagramm der Klasse ATM
Fig 8.20 110%,
Entwurf zuverlassiger Software 137 Entwurf mit OMT
Entwurf eines funktionalen Modells
• Identifiziere Ein- und Ausgabewerte von Prozessen– Parameter von Ereignissen zwischen System und Außenwelt
– Erganze anhand der Problembeschreibung
• Entwerfe Datenflußdiagramme– Beschreibe funktionale Abhangigkeiten von Daten
‘Welcher Wert wird durch welchen Prozeß aus welchen Werten bestimmt?’Prozeß = geplante Reaktion auf Ereignis, abhangig vom Zustand
– Zerlege nichttriviale Prozesse in Teilprozesse (separate Diagramme)
• Spezifiziere, was jede Funktion tun soll– Deklarative Beschreibung der Beziehung zwischen Ein- und Ausgabe
– Prozedurale Beschreibung (keine Detailalgorithmen), wenn dies naturlicher ist
– nat. Sprache, Logik, Gleichungen, Pseudocode, Tabellen, . . .
• Erganze Constraints und Optimierungskriterien– Abhangigkeiten zwischen Objekten (Vorbedingungen, Invarianten, Beziehungen)
– Werte, die optimiert werden sollten, und ihre Prioritaten
Entwurf zuverlassiger Software 138 Entwurf mit OMT
ATM Netzwerk: Datenflußdiagram und
Prozeßverfeinerung
Fig 8.24/25 125%,
Entwurf zuverlassiger Software 139 Entwurf mit OMT
Erganzung zusatzlicher Operationen
• Operationen des Objektmodells– Attribute liefern Queries (Punktnotation!)– Rollen in Beziehungen und Qualifikatoren liefern Queries fur Pseudo-Attribute– Zentrale Operationen sollten direkt im Objektmodell genannt werden
• Operationen des dynamischen Modells– Ereignisse und Zustande initiieren Aktionen und Aktivitaten
• Operationen des funktionalen Modells– Funktionen sind Operationen 7→ gruppiere Funktionen in Objektklassen– Wiederholt auftretende Teilbeschreibungen von Funktionen = Operationen
• Shopping-Liste: Operationen der realen Welt– Erganze Operationen einer Klasse, die unabhangig vom Problem sind⇒ Wiederverwendbarkeit in anderen Kontexten
• Generalisierung zugunsten von Vereinfachung– Definition ahnlicher Operationen verallgemeinern– Operationen in Generalisierungshierarchie verlagern,– ggf. neue (sinnvolle) Oberklasse erzeugen
Entwurf zuverlassiger Software 140 Entwurf mit OMT
OMT Analyse: Zusammenfassung
1. Erstelle (oder erhalte) Problembeschreibung
2. Entwerfe Objektmodell (Objektdiagramm + Begriffslexikon)– Identifiziere relevante Klassen, Beziehungen und Attribute
– Verfeinere Klassenstruktur mit Generalisierung
– Revision und Iteration des Entwurfs
– Aufteilung in Module und Sheets
3. Entwerfe dynamisches Modell (Zustandsdiagramme + Ereignisdiagramm)– Entwerfe Szenarien fur typische Interaktionsfolgen
– Identifiziere Ereignisse zwischen Objekten
– Beschreibe den Fluß der Ereignisse in einem Diagramm
– Entwickle ein Zustandsdiagramm fur jede Klasse mit wichtigem dynamischem Verhalten
– Uberprufe Konsistenz und Vollstandigkeit der Ereignisse mehrerer Zustandsdiagramme
4. Entwerfe funktionales Modell (Datenflußdiagramme + Constraints)– Identifiziere Ein- und Ausgaben
– Beschreibe funktionale Abhangigkeiten durch Datenflußdiagramme
– Beschreibe, was jede Funktion tun soll
– Identifiziere Constraints und spezifiziere Optimierungskriterien
5. Verifiziere und verfeinere die Modelle iterativ– erganze wichtige Operationen des funktionalen Modells im Objektmodell
– Uberprufe Konsistenz+Vollstandigkeit von Klassen, Beziehungen, Attributen und Operationen
– Entwickle detailliertere Szenarien
Entwurf zuverlassiger Software 141 Entwurf mit OMT
OMT: System- und Objektentwurf
• Systementwurf (keine zusatzliche Unterstutzung durch Objektorientierung)
– Zerlege das System in Teilsysteme – Identifiziere inharente Nebenlaufigkeit– Verteile Teilsysteme auf Prozessoren und Tasks– Entwickle Strategie zur Realisierung von Datenspeichern– Identifiziere vorhandene Resourcen und Zugriffsmechanismen fur diese– Wahle eine Methode um Softwarekontrolle zu implementieren– Betrachte Rahmenbedingungen und lege Prioritaten fest⇒ Entwurfsdokument: Systemarchitektur + strategische Entscheidungen
• Objektentwurf– Erganze Objektmodell um wichtige Operationen aus den anderen Modellen– Entwickle Algorithmen fur jede Operation 7→ Programmsynthese
– Optimiere Datenzugriffspfade– Entwerfe Details der Softwarekontrollmethode des Systementwurfs– Verstarke die Vererbungsstruktur der Klassen– Entwerfe die Implementierung der verbleibenden Beziehungen– Bestimme die genaue Reprasentation der Objektattribute– Fasse Klassen und Beziehungen in Modulen zusammen⇒ Entwurfsdokument: Computernahe Reprasentation der Analysemodelle
Dann erst Implementierung in konkreter Programmiersprache
Entwurf zuverlassiger Software 142 Entwurf mit OMT
Object Modelling Technique – Resumee
OMT = Analyse + Systementwurf + Objektentwurf
• Unterstutzung des gesamten Softwareentwurfszyklus– Leitlinien fur Entwurf, Revision und Iteration– Graphische Notation fur Ubersichtlichkeit und bessere Kommunikation⇒ Klarer, leicht verstandlicher Entwurf
• Nahtloser Ubergang der Entwicklungsphasen– keine Ubersetzungsverluste, leichtere Iteration des Entwurfs
• Unabhangig von konkreter Programmiersprache– Methode wichtiger als Eigenarten spezifischer Sprachen– Ausprogrammieren ist der unbedeutendste Teil eines Projekts– Ubertragung laßt sich mechanisieren
• Objektorientierte Methodik liefert praktische Vorteile– Flexibilitat durch Verlagerung von Entwicklungsarbeit in die Analyse– Modifizierbarkeit durch Betonung von Datenstrukturen (statt Algorithmen)– Wartbarkeit, Uberprufbarkeit, Erweiterbarkeit– Uberschaubare Einheiten = leichtere Implementierung 7→ Programmsynthese
Entwurf zuverlassiger Software
Lektion 8
Synthese von Algorithmen
1. Formale Grundbegriffe
2. Beispiel einer formalen Synthese
3. Syntheseparadigmen
Entwurf zuverlassiger Software 143 Programmsynthese
Programmsynthese
Automatisierung des Schrittes von der Spezifikation
zum korrekten, ausfuhrbaren Programm
und Dokumentation getroffener Entscheidungen
• Formale Spezifikation des Problems– Formulierung in fest vorgebenem formalen Rahmen
– Verlangt Fixierung einer formalen Sprache
• Strategien zur automatischen Algorithmensynthese– Benotigen theoretische Resultate uber Korrektheit erzeugter Algorithmen
– Syntheseparadigma: zulassige Manipulationen garantieren Korrektheit
– Synthesestrategie automatisiert Anwendung zulassiger Operationen
• Optimierung und Datentypverfeinerung
Entwurf zuverlassiger Software 144 Programmsynthese
Formale Sprache: Grundbestandteile
Logische OperatorenP ∧ Q Konjunktion von P und Q
P ∨ Q Disjunktion von P und Q
¬P Negation von P
P ⇒ Q Implikation∀x:T. P(x) Fur alle x vom Typ T gilt P(x) (unbeschrankt!)
∃x:T. P(x) Es gibt ein x vom Typ T fur das P(x) gilt (unbeschrankt!)
DatentypenZ, N Ganze und naturliche ZahlenB Boole’sche Werteα×β Paare von Werten aus α und β
α→β Funktionen von α nach β
Set(α) Endliche Mengen uber α
Seq(α) Endliche Listen (Sequenzen) uber α
λ-Kalkulλx.term Abstraktion: Funktion f mit f(x)=term
f(a) Applikation: Anwendung von f auf a(λx.term)(a) Reduktion: liefert term[a/x]term[a/x] Jedes Vorkommen von x in term wird durch a ersetzt
Entwurf zuverlassiger Software 145 Programmsynthese
Formale Sprache: wichtigste Operationen
B , true, false Boolean truth values
¬, ∧, ∨, ⇒ , ⇐ , ⇔ Boolean connectives
∀x ∈S.p, ∃x ∈S.p Limited boolean quantifiers (on finite sets and sequences)
if p then a else b Conditional
Seq(α) Data type of finite sequences over members of α
null?, ∈, v Decision procedures: emptiness, membership, prefix
[], [a], [i..j], [a1...an] Empty/ singleton sequence, subrange, literal sequence former
a.L, L·a Prepend a, append a to L
[f(x)|x ∈L ∧p(x)], |L|, L[i] General sequence former, length of L, i-th element,
domain(L), range(L) The sets 1..|L| and L[i]|i ∈domain(L)
nodups(L) Decision procedure: all the L[i] are distinct (no duplicates)
Set(α) Data type of finite sets over members of α
empty?, ∈, ⊆ Decision procedures: emptiness, membership, subset
∅, a, i..j, a1...an Empty set, singleton set, integer subset, literal set former
S+a, S-a Element addition, element deletion
f(x)|x ∈S ∧p(x), |S| General set former, cardinality
S∪T, S∩T, S\T Union, intersection, set difference⋃
FAMILY, ∩FAMILY Union, intersection of a family of sets
Entwurf zuverlassiger Software 146 Programmsynthese
Programmsynthese: Formale Grundbegriffe
• Spezifikation: Tupel spec = (D,R,I,O)
Notation : FUNCTION f(x:D):R WHERE I(x) RETURNS y SUCH THAT O(x,y)
– D (Domain) und R (Range): Datentypen
– I (Input-Bedingung an zulassige Eingaben): Pradikat uber D
– O (Output-Bedingung an mogliche Ausgaben): Pradikat uber D×R
D,R,I,O in Spezifikationssprache zu beschreiben
• Programm: Tupel p = (D,R,I,O, body )
FUNCTION f(x:D):R WHERE I(x) RETURNS y SUCH THAT O(x,y) ≡ body(x)
– (D,R,I,O): Spezifikation
– body:D6→R (Programmkorper): berechenbare Funktion
body in Programmiersprache zu beschreiben (f darf vorkommen)
• Programm p korrekt, falls gilt: ∀x:D. I(x) ⇒ O(x,body(x))
• Spezifikation spec erfullbar (synthetisierbar), falls eine Funktion body:D6→R
existiert, so daß p=(spec,body) korrekt ist
Entwurf zuverlassiger Software 147 Programmsynthese
Phasen einer formalen Entwicklung von Algorithmen
1. Erstellen der notigen “Objekttheorie”:– Formalisierung vorkommender Begriffe
– Aufstellen mathematischer Gesetze
2. Erstellen der formalen Spezifikation
3. Entwurf eines lauffahigen, korrekten Algorithmus
4. Verifizierte algorithmische Optimierung
5. Implementierung abstrakter Datentypen
6. Compilierung und sprachabhangige Optimierung
Entwurf zuverlassiger Software 148 DEMO: Costas Arrays Synthese
Costas-Arrays: Problemstellung
Costas Array der Große n:
Permutation von 1..n ohne doppelte Elemente in den Zeilen der Differenzentafel
2 4 1 6 5 3
-2 3 -5 1 2
1 -2 -4 3
-4 -1 -2
-3 1
-1
Costas Array der Ordnung 6 und seine Differenzentafel
Ziel: Berechnung aller Costas Arrays der Große n
Entwurf zuverlassiger Software 149 DEMO: Costas Arrays Synthese
Costas-Arrays (1): Objekttheorie
• Formalisierung vorkommender Begriffe:dtrow(L,j) ≡ [L[i]-L[i+j]| i ∈[1..|L|-j]]
perm(L,S) ≡ nodups(L) ∧ range(L)=S
• Aufstellen mathematischer Gesetze:∀L,L’:Seq(Z).∀i:Z.∀j:N.
1. dtrow([],j) = []
2. j≤|L| ⇒ dtrow(i.L,j) = (i-L[j]).dtrow(L,j)
3. j6=0 ⇒ dtrow([i],j) = []
4. LvL’ ⇒ dtrow(L,j) v dtrow(L’,j)
5. j≥|L| ⇒ dtrow(L,j) = []
6. j≤|L| ⇒ dtrow(L·i,j) = dtrow(L,j)·(L[ |L|+1-j]-i)
Entwurf zuverlassiger Software 150 DEMO: Costas Arrays Synthese
Costas-Arrays (2): formale Spezifikation
FUNCTION Costas (n:Z):Set(Seq(Z)) WHERE n≥1
RETURNS All-p
SUCH THAT All-p =
p:Seq(Z)| perm(p,1..n)
∧ ∀j ∈domain(p).nodups(dtrow(p,j))
Kurzschreibweise
FUNCTION Costas (n:Z) WHERE n≥1
RETURNS p:Seq(Z)| perm(p,1..n)
∧ ∀j ∈domain(p).nodups(dtrow(p,j))
Entwurf zuverlassiger Software 151 DEMO: Costas Arrays Synthese
Costas-Arrays (3): lauffahiger Algorithmus
FUNCTION Costas (n:Z) WHERE n≥1
RETURNS p:Seq(Z)| perm(p,1..n) ∧ ∀j ∈domain(p).nodups(dtrow(p,j))
= if nodups([]) ∧ ∀j ∈domain([]).nodups(dtrow([],j))
then Costasaux(n,[]) else ∅
FUNCTION Costasaux (n:Z,V:Seq(Z))
WHERE n≥1 ∧ range(V)⊆1..n ∧ nodups(V) ∧ ∀j ∈domain(V).nodups(dtrow(V,j))
RETURNS p:Seq(Z)| perm(p,1..n) ∧ Vvp ∧ ∀j ∈domain(p).nodups(dtrow(p,j))
= p | p ∈V ∧ perm(p,1..n) ∧ ∀j ∈domain(p).nodups(dtrow(p,j))
∪⋃
Costasaux(n,W) | W ∈V·i|i ∈1..n ∧ nodups(W)
∧ ∀j ∈domain(W).nodups(dtrow(W,j))
Entwurf zuverlassiger Software 152 DEMO: Costas Arrays Synthese
COSTAS-ARRAYS (4a): CI-Simplifikationen
FUNCTION Costas (n:Z) WHERE n≥1
RETURNS p:Seq(Z)| perm(p,1..n) ∧ ∀j ∈domain(p).nodups(dtrow(p,j))
= Costasaux(n,[])
FUNCTION Costasaux (n:Z,V:Seq(Z))
WHERE n≥1 ∧ range(V)⊆1..n ∧ nodups(V) ∧ ∀j ∈domain(V).nodups(dtrow(V,j))
RETURNS p:Seq(Z)| perm(p,1..n) ∧ Vvp ∧ ∀j ∈domain(p).nodups(dtrow(p,j))
= (if perm(V,1..n) ∧ ∀j ∈domain(V).nodups(dtrow(V,j)) then V else ∅)
∪⋃
Costasaux(n,V·i) |i ∈1..n ∧ nodups(V·i)
∧ ∀j ∈domain(V·i).nodups(dtrow(V·i,j))
Entwurf zuverlassiger Software 153 DEMO: Costas Arrays Synthese
Costas-Arrays (4b): CD-Simplifikationen
FUNCTION Costas (n:Z) WHERE n≥1
RETURNS p:Seq(Z)| perm(p,1..n) ∧ ∀j ∈domain(p).nodups(dtrow(p,j))
= Costasaux(n,[])
FUNCTION Costasaux (n:Z,V:Seq(Z))
WHERE n≥1 ∧ range(V)⊆1..n ∧ nodups(V) ∧ ∀j ∈domain(V).nodups(dtrow(V,j))
RETURNS p:Seq(Z)| perm(p,1..n) ∧ Vvp ∧ ∀j ∈domain(p).nodups(dtrow(p,j))
= (if 1..n⊆range(V) then V else ∅)
∪⋃
Costasaux(n,V·i) |i ∈1..n ∧ i 6∈V
∧ ∀j ∈domain(V). (V[|V|+1-j]-i) 6∈dtrow(V,j)
Entwurf zuverlassiger Software 154 DEMO: Costas Arrays Synthese
Costas-Arrays (4c): Finite Differencing
FUNCTION Costas (n:Z) WHERE n≥1
RETURNS p:Seq(Z)| perm(p,1..n) ∧ ∀j ∈domain(p).nodups(dtrow(p,j))
= Costasaux1(n,[],1..n)
FUNCTION Costasaux1 (n:Z,V:Seq(Z),Pool:Set(Z))
WHERE n≥1 ∧ range(V)⊆1..n ∧ nodups(V) ∧ ∀j ∈domain(V).nodups(dtrow(V,j))
∧ Pool = 1..n\range(V)
RETURNS p:Seq(Z)| perm(p,1..n) ∧ Vvp ∧ ∀j ∈domain(p).nodups(dtrow(p,j))
= (if empty?(Pool) then V else ∅)
∪⋃
Costasaux1(n,V·i,Pool−i) |i ∈Pool
∧ ∀j ∈domain(V). (V[|V|+1-j]-i) 6∈dtrow(V,j)
Entwurf zuverlassiger Software 155 DEMO: Costas Arrays Synthese
Costas-Arrays (4d): Case Analysis
FUNCTION Costas (n:Z) WHERE n≥1
RETURNS p:Seq(Z)| perm(p,1..n) ∧ ∀j ∈domain(p).nodups(dtrow(p,j))
= Costasaux2(n,[],1..n,1)
FUNCTION Costasaux2 (n:Z,V:Seq(Z), Pool:Set(Z),Vsize:Z)
WHERE n≥1 ∧ range(V)⊆1..n ∧ nodups(V) ∧ ∀j ∈domain(V).nodups(dtrow(V,j))
∧ Pool = 1..n\range(V) ∧ Vsize = |V|+1
RETURNS p:Seq(Z)| perm(p,1..n) ∧ Vvp ∧ ∀j ∈domain(p).nodups(dtrow(p,j))
= if empty?(Pool)
then V
else⋃
Costasaux2(n,V·i,Pool−i,Vsize+1) |i ∈Pool
∧ ∀j ∈domain(V). (V[Vsize-j]-i) 6∈dtrow(V,j)
Entwurf zuverlassiger Software 156 DEMO: Costas Arrays Synthese
Datentypverfeinerung
Ersetze abstrakte Definitionen von Datentypen
durch effiziente konkrete Implementierungen
• Endliche Mengen– Listen: Standardimplementierung
– Bitvektor: Mengen uber endlichem Domain
– charakteristische Funktion (effiziente Elementrelation)
• Folgen– verkettete Liste: Standardimplementierung
– umgekehrte Liste (gut fur append-Operation ·)
• System stellt Auswahl von Implementierungen bereit
Benutzer legt Nichtstandard-Implementierung fest– separate fur jede einzelne Variable
Entwurf zuverlassiger Software 157 DEMO: Costas Arrays Synthese
Syntheseparadigmen
• Unterscheidungsmerkmale
– Interne Aufgabenstellung (Darstellung des Problems)
– Interne Losungsmethode (Art der Inferenzen)
– Konstruktionsmethode fur Algorithmus (aus interner Losung)
• Beweise als Programme
– Extraktion aus konstruktivem Beweis eines Theorems
• Synthese durch Transformationen
– Aquivalenzumformungen in ausfuhrbare (rekursive) Form
• Verwendung von Algorithmenschemata
– Verfeinerung von Standardlosungen fur bekannte algorithmische Strukturen
Entwurf zuverlassiger Software 158 DEMO: Costas Arrays Synthese
Syntheseparadigmen: Beweise als Programme
Gegeben sei die Spezifikation:
FUNCTION f(x:D):R WHERE I(x) RETURNS y SUCH THAT O(x,y)
1. Wandle um in Spezifikationstheorem:
– ∀x:D.∃y:R. I(x) ⇒ O(x,y)
2. Suche formalen Beweis in konstruktivem logischen Kalkul.
3. Extrahiere aus Beweis eine Methode, y aus x zu berechnen
Forschung:
– Ausdrucksstarke Kalkule
– Effiziente Beweisstrategien und Beweisplaner (Induktion)
– Effiziente Extraktionsmechanismen
Entwurf zuverlassiger Software 159 DEMO: Costas Arrays Synthese
Syntheseparadigmen: Synthese durch Transformation
Gegeben sei die Spezifikation:
FUNCTION f(x:D):R WHERE I(x) RETURNS y SUCH THAT O(x,y)
1. Definiere neues Pradikat F uber D×R durch:
– ∀x:D.∀y:R. I(x) ⇒ (F(x,y) ⇔ O(x,y)).
2. Transformiere in aquivalente Formel der Gestalt:
– ∀x:D.∀y:R. I(x) ⇒ (F(x,y) ⇔ Of(x,y))
Of(x,y) darf nur aus erfullbaren Pradikaten und Vorkommen von F bestehen
3. Extrahiere aus der rekursiven Formel ein Programm.
– Alternativ: Interpretation als Logik-Programm
Forschung:
– Leistungsfahige Transformationsregeln
– effiziente Rewrite Techniken und Heuristiken
Entwurf zuverlassiger Software 160 DEMO: Costas Arrays Synthese
Syntheseparadigmen: Algorithmenschemata
Erzeuge Algorithmus in einem Schritt
Gegeben sei die Spezifikation:
FUNCTION f(x:D):R WHERE I(x) RETURNS y SUCH THAT O(x,y)
1. Wahle algorithmischen Klasse und (partielles) Schema
2. Verfeinere Schema auf das Problem
Vervollstandige unbesetzte Parameter
3. Instantiiere Algorithmenschema
Forschung:
– Analyse der Struktur einer Klasse von Algorithmen
– Komponenten und Axiome fur Korrektheit
– Techniken zur Verfeinerung von Standardlosungen
Entwurf zuverlassiger Software 161 DEMO: Costas Arrays Synthese
Synthese–Strategien
Konkrete Verfahren zur
Synthese von Algorithmen aus Spezifikationen
• Steuern die Anwendung eines logischen Formalismus
• Strukturieren den Losungsweg durch interne Teilziele
• Verarbeiten Programmierwissen
• Losen Teilziele durch heuristisch kontrollierte Suche
• Hangen ab von Ruckfragen an den Benutzer
Entwurf zuverlassiger Software 162 DEMO: Costas Arrays Synthese
Synthesestrategien: Historisch relevante Verfahren
• Informale Methoden– Polya, Dijkstra, Gries, . . .
• Beweiser mit Skolemisierung und Resolution– Green, 1969 (Stanford/Kestrel Institute)
– Manna/Waldinger, 1971,75 (SRI International)
Transformations- und Formationsregeln
– Manna/Waldinger, 1972–1980
Beweiskalkul gekoppelt mit Transformationen
– Manna/Waldinger, 1980–
• Fold/Unfold Techniken– Burstall/Darlington (Edinburgh) 1975–81
• Modifizierte Knuth-Bendix Vervollstandigung– Dershowitz (Illinois) 1985–
• Synthese von Logikprogrammen– Clark, Hogger (London) 1980 –
Entwurf zuverlassiger Software
Lektion 9
Beweise als Programme
1. Prinzip und Rechtfertigung
2. Kalkule fur konstruktives Beweisen
3. Algorithmenkonstruktion
4. Zur Automatisierung konstruktiver Beweise
Entwurf zuverlassiger Software 163 Beweise als Programme
Beweise als Programme
Gegeben sei die Spezifikation:
FUNCTION f(x:D):R WHERE I(x) RETURNS y SUCH THAT O(x,y)
1. Wandle um in Spezifikationstheorem:
– ∀x:D.∃y:R. I(x) ⇒ O(x,y)
2. Suche formalen Beweis in konstruktivem logischen Kalkul.
3. Extrahiere aus Beweis eine Methode, y aus x zu berechnen
Forschung:
– Ausdrucksstarke Kalkule
– Effiziente Beweisstrategien und Beweisplaner (Induktion)
– Effiziente Extraktionsmechanismen
Entwurf zuverlassiger Software 164 Beweise als Programme
Rechtfertigung des Prinzips
Programmentwicklung ist konstruktive Beweisfuhrung
• Satz: Ist ∀x:D.∃y:R. I(x) ⇒ O(x,y) beweisbar,
so gibt es eine berechenbare Funktion f :D→R
mit der Eigenschaft ∀x:D. I(x) ⇒ O(x,f(x))
d.h. f ist ein Algorithmus, der die Ausgangsspezifikation erfullt
• Beispiel: ∀x:N. ∃y:N. y2≤x ∧ x<(y+1)2
– Beweis liefert Funktion zur Berechnung der Quadratwurzel von x
• Konstruktive Interpretation logischer Symbole– P ⇒Q: ‘Aus einer Evidenz fur P kann man eine fur Q erzeugen’
– P ∨Q: ‘Man kann P beweisen oder man kann Q beweisen’
· P ∨ ¬P kann nicht als allgemeines Prinzip gesehen werden !!
– ∃x:T .P : ‘Man kann ein x aus T angeben, fur das P gilt’
– Notwendige Voraussetzung fur Erzeugung von Programmen aus Beweisen
Entwurf zuverlassiger Software 165 Beweise als Programme
Kalkule
Simulation mathematisch-semantischer Argumentation
durch Regeln zur Symbolmanipulation
• Anwendung formaler Vorschriften ohne Nachdenken– umgeht Mehrdeutigkeiten der naturlichen Sprache
– schematische Losung mathematischer Probleme
• Kernbestandteile:– Formale Sprache (Syntax + Semantik)
– Ableitungssystem (Regeln + Axiome)
• Wichtige Eigenschaften:– korrekt + vollstandig bzgl. Semantik
– leicht zu verstehen
– leicht zu verarbeiten (automatisierbar)
Entwurf zuverlassiger Software 166 Beweise als Programme
Kalkularten
synthetisch/bottom-up: Schlusse Axiomen zur Aussage
analytisch/top-down: von Zielaussage zu Voraussetzungen
• Frege–Hilbert–Kalkule:– viele Axiome, kaum echte Regeln; sehr machtig;
– synthetisch, Beweissuche aufwendig
• Gentzens naturliches Schließen (NK / NJ)– synthetisch, nahe am naturlichen mathematischen Schließen, kaum Axiome,
– 2 Regeln pro logisches Zeichen, Verwaltung von Annahmen notig
• Sequenzenkalkule (LK / LJ)– Modifikation von NK/NJ: Schließen uber Urteile statt Aussagen
– lokale Sicht, keine Verwaltung von Annahmen, gut fur interaktive Beweiser
– synthetisch oder analytisch formulierbar
• Resolutions- und Konnektionskalkule– analytisch, maschinennah, gut fur automatisches Beweisen, kaum lesbar
Entwurf zuverlassiger Software 167 Beweise als Programme
Sequenzenkalkul (erweiterte Pradikatenlogik)
• Sequenz l1:H1,...,ln:Hn ` C btc– ‘Unter Hypothesen H1,. . . ,Hn gilt Konklusion C’
– Term t ist eine (implizite) Darstellung des Beweises
– Labels li fur Deklaration von Hypothesen und Variablen
· Namensgebung zur Identifikation von Hypothesen im Beweis
• Beweismethodik: schrittweise Verfeinerung– Anwendung schematischer Beweisregeln liefert Menge von Untersequenzen
– Wiederholung, bis Regeln nur noch leere Mengen von Teilzielen liefern
• Formaler Beweis fur Theoreme– Baum markiert mit Sequenzen und Namen von Verfeinerungsregeln
– Wurzelknotens enthalt Beweisziel als Sequenz
– Nachfolgerknoten enthalt Ergebnis der Regelanwendung auf Sequenz
– unvollstandiger Beweis: manche Blatter ohne Regel
– Beweisbaum wird wahrend des Beweises schrittweise aufgebaut
– Beweisterm t wird (bottom-up) aus vollstandigem Beweis konstruiert
• Beweisterm als Programm interpretierbar
Entwurf zuverlassiger Software 168 Beweise als Programme
Sequenzenkalkul: Struktur der Regeln
• Top-Down Zerlegung von ZielsequenzenΓ ` C be(t1...tn)c by rname parm-list
Γ1 ` C1 bt1c...Γn ` Cn btnc
– Regelschema: aktuelle Zielsequenz muß gleiche Struktur wie ‘Γ ` C’ haben– Regelname und Parameterliste legen Art der Dekomposition fest– Regel erzeugt Unterziele Γi ` Ci
– Regel sagt, wie Beweisterme ti der Unterziele zusammengesetzt werden· liefert Beweisterm e(t1. . . tn) fur ‘Γ ` C’
• Einfuhrungsregeln (name i):– Strukturelle Zerlegung (Analyse) der Konklusion C
– Unter welchen Voraussetzungen ist C gultig?– Wie setzt sich der Beweisterm fur C zusammen?
• Eliminationsregeln (name e):– Strukturelle Zerlegung einer Hypothese Hj
– Was folgt aus der Hypothese Hj fur eine beliebige Konklusion C?– Wie wird ein Beweisterm l fur Hj zerlegt, um einen fur C zu konstruieren?
Entwurf zuverlassiger Software 169 Beweise als Programme
Sequenzenkalkul: Aussagenlogische Regeln
Γ ` A ∧B b(a,b)c
by and i
Γ ` A bac
Γ ` B bbc
Γ, l:A ∧B, ∆ ` C blet (a,b)=l in tc
by and e l a b
Γ, a:A, b:B, ∆ ` C btc
Γ ` A ∨B binl(a)c
by or i1
Γ ` A bac
Γ, l:A ∨B, ∆ ` C
bcase l of inl(a)7→t1 | inl(b)7→t2c
by or e l a b
Γ, a:A, ∆ ` C bt1c
Γ, b:B, ∆ ` C bt2c
Γ ` A ∨B binr(b)c
by or i2
Γ ` B bbc
Γ ` A ⇒ B bλa.bc
by imp i a
Γ, a:A ` B bbc
Γ, l:A ⇒ B ` C bt[l(a)/b]cby imp e l b
Γ, l:A ⇒ B, ∆ ` A bac
Γ, ∆, b:B ` C btc
Γ ` ¬A bλa.bc
by not i a
Γ, a:A ` Λ bbc
Γ, l:¬A, ∆ ` C bt[l(a)/b]cby not e l b
Γ, l:¬A, ∆ ` A bac
Γ, ∆, b:Λ ` C btc
Γ, l:Λ, ∆ ` C bany(l)c
by false e l
Entwurf zuverlassiger Software 170 Beweise als Programme
Sequenzenkalkul: Quantorregeln + Gleichheit
Γ ` ∀x:T .A bλx′.ac
by all i x′ ∗
Γ, x′:T ` A[x′/x] bac
Γ, l:∀x:T .A, ∆ ` C bt[l(c)/a]cby all e l c a
Γ, l:∀x:T .A, ∆, a:A[c/x] ` C btc
Γ ` ∃x:T .A b(c,a)c
by ex i c
Γ ` A[c/x] bac
Γ, l:∃x:T .A, ∆ ` C blet (x′,a)=l in tc
by ex e l x′ a ∗∗
Γ, x′:T , a:A[x′/x], ∆ ` C btc
Γ ` t=t
Ax
by reflexivity
Γ ` t1=t2
Ax
by symmetry
Γ ` t2=t1
Ax
Γ ` t1=t2
Ax
by transitivity u
Γ ` t1=u
Ax
Γ ` u=t2
Ax
Γ ` C[t1/x] btc
by substitution t1=t2
Γ ` t1=t2
Ax
Γ ` C[t2/x] btc
∗: Umbenennung [x′/x] notig, wenn x in Γ frei vorkommt (automatisch!)∗∗: Umbenennung [x′/x] notig, wenn x in C frei vorkommt (automatisch!)
Entwurf zuverlassiger Software 171 Beweise als Programme
Sequenzenkalkul: nichtlogische Regeln
• Verwendung einer bekannten Losung (Hypothese oder Lemma)
Γ, l:C, ∆ ` C blcby hyp l
Γ ` C btcby lemma theorem-name
– C/ t: Konklusion bzw. Beweisterm des Lemma theorem-name
• Lokale Zwischenbehauptungen (Cut): Γ ` C bt[a/l]cby cut l AΓ ` A bac
Γ, l:A ` C btc
• Entfernen uberflussiger Hypothesen: Γ, l:A, ∆ ` C btcby thin lΓ, ∆ ` C btc
• Entscheidung trivialer Gleichungen: Γ ` s = t ∈ T
Ax
by equality
– Gleichheit muß aus Symmetrie, Reflexivitat und Transitivitat folgen
• Auswertung von Teilausdrucken:
Γ ` C[u] btcby compute uΓ ` C[u ↓] btc
Γ, l:A[u], ∆ ` C btcby computeHyp l uΓ, l:A[u ↓], ∆ ` C btc
– u ↓ ergibt sich aus u durch Reduktion (Steuerungsparameter moglich)
Entwurf zuverlassiger Software 172 Beweise als Programme
Sequenzenkalkul: Zahlen und Listen
Induktive Beweisfuhrung = primitive Rekursion
• Induktion als Elimination naturlicher ZahlenΓ, n:N, ∆ ` C bind(n; b;m,hyp.t)c
by nat e n m hypΓ, n:N, ∆ ` C[0/n] bbc
Γ, n:N, ∆, m:N, hyp:C[m/n] ` C[m+1/n] btc
– ind-Term entspricht primitiver Rekursion
– Fur f =λn.ind(n; b;m,hyp.t) gilt f(0)=b und f(n+1) = t[n,f(n) /m, hyp]
• Elementare Arithmetik Γ ` C btc
by arith
arith anwendbar, wenn C aus Γ durch arithmetische Schlusse uber +,-,*,/,mod,<,= und
Integer-Konstanten folgt. Beweisterm t ist Ax oder eine Entscheidungsprozedur der Art
‘if x<y then a else b’ bzw. ‘if x=y then a else b’
• Induktion auf Folgen von Werten (Sequenzen)Γ, L:Seq(α), ∆ ` C bseqind(L; tb; a,L′,hyp.tu)c
by seq e a L′ hypΓ, L:Seq(α), ∆ ` C[[]/L] btbc
L:Seq(α), ∆, a:α, L′:Seq(α), hyp:C[L′ / L] ` C[a.L′ / L] btuc
– seqind-Term entspricht primitiver Rekursion auf Listen
Weitere Regeln je nach formaler Theorie
Entwurf zuverlassiger Software 173 Beweise als Programme
Formaler Beweis: Wurzel
` ∀x:N.∃y:N. y2≤x ∧ x<(y+1)2
by all i x THEN nat e x n v|\| x:N ` ∃y:N. y2≤0 ∧ 0<(y+1)2
| by ex i 0| \| x:N ` 02≤0 ∧ 0<(0+1)2
| by and i THEN arith\x:N, n:N, v:∃y:N. y2≤n ∧ n<(y+1)2 ` ∃y:N. y2≤n+1 ∧ n+1<(y+1)2
\by ex e v y %1 THEN and e %1 %2 %3\... y:N, %2: y2≤n, %3: n<(y+1)2 ` ∃y:N. y2≤n+1 ∧ n+1<(y+1)2
by cut X n+1<(y+1)2∨ n+1=(y+1)2
|\| ...y2≤n, n<(y+1)2 ` n+1<(y+1)2
∨ n+1=(y+1)2
| by arith\...y2≤n, n<(y+1)2, X: n+1<(y+1)2
∨ n+1=(y+1)2 ` ∃y:N. y2≤n+1 ∧ n+1<(y+1)2
by or e X %4 %5|\| ... y2≤n, n<(y+1)2, %4: n+1<(y+1)2 ` ∃y:N. y2≤n+1 ∧ n+1<(y+1)2
| by ex i y| \| ... y2≤n, n<(y+1)2, n+1<(y+1)2 ` y2≤n+1 ∧ n+1<(y+1)2
| by and i ... arith\... y2≤n, n<(y+1)2, %5: n+1=(y+1)2 ` ∃y:N. y2≤n+1 ∧ n+1<(y+1)2
by ex i y+1\... y2≤n, n<(y+1)2, n+1=(y+1)2 ` (y+1)2≤n+1 ∧ n+1<(y+1+1)2
by and i ... arith
Entwurf zuverlassiger Software 174 Beweise als Programme
Beweisterm: Wurzel
λx.ind(x; (0, (Ax,Ax) );n,v. let (y,%1)=v in
let (%2,%3)=%1 in(case X of inl(%4) 7→ (y, (Ax,Ax) )
| inr(%5) 7→ (y+1, (Ax,Ax) ))[if n+1<(y+1)2 then inl(Ax) else inr(Ax)/X]
)
• Beweisterm t nach Reduktionenλx.ind(x; (0, (Ax,Ax) );
n,v. let (y,%1)=v inlet (%2,%3)=%1 in
if n+1<(y+1)2 then (y, (Ax,Ax) )else (y+1, (Ax,Ax) )
)
• Algorithmus sqrt(x):= fst(t(x)) nach Vereinfachung
sqrt(x):= if x=0 then 0
else let y = sqrt(x-1) in
if x<(y+1)2 then y else y+1
Entwurf zuverlassiger Software 175 Beweise als Programme
Algorithmenkonstruktion aus Beweisen
Satz: Ist t ein Beweisterm fur ` ∀x:D.∃y:R. I(x) ⇒ O(x,y),
so ist das folgende Program korrekt
FUNCTION f(x:D):R WHERE I(x) RETURNS y SUCH THAT O(x,y)≡ fst( t(x) )
d.h. der Algorithmus entsteht durch Unterdruckung des Korrektheitsbeweises
1. Extrahiere Beweisterm t aus vollstandigem Beweis fur
` ∀x:D.∃y:R. I(x) ⇒ O(x,y)
entsprechend den angewandten Regeln
2. Konstruiere den Programmkorper λx. fst( t(x) )
3. Optimiere durch Elimination uberflussiger Information
Entwurf zuverlassiger Software 176 Beweise als Programme
Maximale Segmentsumme: Losungsidee
• Gegeben eine Folge a1, a2, . . . , an ganzer Zahlen
Bestimme die Summe Σqi=pai eines Segmentes, die maximal im Bezug
auf alle moglichen Summen von Segmenten ist
Mn ≡ max(Σqi=pai | 1≤p≤q≤n)
• Direkte Losung leicht zu finden, aber ineffizient
• Induktive Betrachtung liefert
M1 = a1, Mn+1 = max(Mn,Ln+1)
wobei Ln ≡ max(Σni=pai | 1≤p≤n)
L1 = a1, Ln+1 = max(Ln+an+1,an+1) )
→ eleganterer, effizienterer und korrekter Algorithmus
Entwurf zuverlassiger Software 177 Beweise als Programme
Maximale Segmentsumme: Objekttheorie
max(i,j) ≡ if i<j then j else i
|a| ≡ seqind(a; 0; x,a’,lga′.lga′+1)
hd(a) ≡ seqind(a; 0; x,a’,hda′.x)
tl(a) ≡ seqind(a; []; x,a’,tla′.a’)
ai ≡ hd(ind(i;a; x,a’.tl(a’)tl(s)))
Σqi=pai ≡ ind(q-p;ap; i,sum. sum+ap+i+1)
M = maxseq(a)≡ ∃k,j:Z. 1≤k≤j≤|a| ∧ M=Σji=kai
∧ ∀p,q:Z. 1≤p≤q≤|a| ⇒ M≥Σqi=pai
L = maxbeg(a) ≡ ∃j:Z. 1≤j≤|a| ∧ L=Σji=1ai
∧ ∀q:Z. 1≤q≤|a| ⇒ L≥Σqi=1ai
• Gesetze der Maximalen Segmentsumme
M1: a1= maxbeg([a1]) = maxbeg(a1.[])
M2: a1= maxseq([a1]) = maxseq(a1.[])
M3: L = maxbeg(a) ⇒ max(L+a1,a1) = maxbeg(a1.a)
M4: M = maxseq(a) ∧ L = maxbeg(a1.a) ⇒ max(M,L) = maxseq(a1.a)
Entwurf zuverlassiger Software 178 Beweise als Programme
Maximale Segmentsumme: formale Spezifikation
• Voraussetzung: Folge a ist nicht leer:– Leichter darzustellen als a hat die Form a1.a fur ein a1
∈ Z
• Spezifikation der gemeinsamen Berechnung von L und M
FUNCTION MAXSEG(a1:Z,a:Seq(Z)):Z×Z WHERE true
RETURNS L,M SUCH THAT L = maxbeg(a1.a) ∧ M = maxseq(a1.a)
• Spezifikationstheorem∀a:Seq(Z).∀a1:Z.∃L:Z.∃M:Z. L = maxbeg(a1.a) ∧ M = maxseq(a1.a)
• Struktur des Beweistermsλa.λa1. seqind(a; 〈a1,a1,pfbase〉; x,l,v.λa1.let 〈L,〈M,v2,v3
〉〉 = v x
in 〈max(L+a1,a1),max(M,max(L+a1,a1)),pfind〉)
• Algorithmus nach Optimierung
FUNCTION MAXSEG(a1:Z,a:Seq(Z)):Z×Z WHERE true
RETURNS L,M SUCH THAT L = maxbeg(a1.a) ∧ M = maxseq(a1.a)
≡ if a=[] then (a1,a1)else let x.l = a
let (L,M)= MAXSEG(x,l)let new-L = max(L+a1,a1)in (L, max(M,L))
Entwurf zuverlassiger Software 179 Beweise als Programme
Maximale Segmentsumme: formaler Beweis (Labels unterdruckt)
` ∀a:Seq(Z).∀a1:Z.∃L:Z.∃M:Z. L = maxbeg(a
1.a) ∧ M = maxseq(a
1.a)
by all i THEN seq e 1 THEN all i (Induktion auf a)|\| a:Seq(Z), a
1:Z ` ∃L:Z.∃M:Z. L = maxbeg(a
1.[]) ∧ M = maxseq(a
1.[])
| by ex i a1THEN ex i a
1THEN and i
| |\| | a:Seq(Z), a
1:Z ` a
1= maxbeg(a
1.[])
| | by lemma M1| \| a:Seq(Z), a
1:Z ` a
1= maxseq(a
1.[])
| by lemma M2\... x:Z, l:Seq(Z), v:∀a
1:Z.∃L:Z.∃M:Z. L = maxbeg(a
1.l) ∧ M = maxseq(a
1.l)
` ∃L:Z.∃M:Z. L = maxbeg(a1.(x.l)) ∧ M = maxseq(a
1.(x.l))
by all e 4 x THEN thin 4\... v
1:∃L:Z.∃M:Z. L = maxbeg(x.l) ∧ M = maxseq(x.l)
` ∃L:Z.∃M:Z. L = maxbeg(a1.(x.l)) ∧ M = maxseq(a
1.(x.l))
by ex e 5 THEN ex e 6 THEN and e 7\... L:Z, M:Z, v
2: L = maxbeg(x.l), v
3: M = maxseq(x.l)
` ∃L:Z.∃M:Z. L = maxbeg(a1.(x.l)) ∧ M = maxseq(a
1.(x.l))
by ex i max(L+a1,a
1) THEN ex i max(M, max(L+a
1,a
1)) THEN and i
|\| ... v
2: L = maxbeg(x.l), v
3: M = maxseq(x.l)
| ` max(L+a1,a
1) = maxbeg(a
1.(x.l))
| by lemma M3\... v
2: L = maxbeg(x.l), v
3: M = maxseq(x.l)
` max(M, max(L+a1,a
1)) = maxseq(a
1.(x.l))
by ... lemma M3 ... lemma M4
Entwurf zuverlassiger Software 180 Beweise als Programme
Beweise als Programme: OYSTER/CLAM Beweisplaner
• Planer simuliert Kalkul — Beweiser fuhrt Beweisplan aus
– Verzogerung von Entscheidungen durch Skolemvariablen und Unifikation
• Induktionsbeweise
– Induktionsschema ⇐ Analyse der Rekursionsstruktur + globales Schema
– Rippling: Verschiebe Unterschiede zwischen Induktionshypothese und -schluß
bis Funktion der Hypothese entsteht
Literatur:– A. Bundy, A. Smaill, G. Wiggins. The synthesis of logic programs from inductive proofs.
Computer Logic Proceedings, Brussels. Springer Verlag, 1990.
– A. Bundy, F. van Harmelen, J. Hesketh, A. Smaill. Experiments with proof plans for induction.
JAR 7:303–324, 1991.
– A. Bundy. The use of explicit plans to guide inductive proofs. Proc. CADE-9, Springer LNCS 310,
111–120, 1988.
– A. Bundy. Automatic guidance of program synthesis proofs. Workshop on Automating Software
Design, IJCAI-89, 57–59, 1989.
– A. Bundy, F. van Harmelen, A. Smaill, A. Ireland. Extensions to the rippling-out tactic for
guiding inductive proofs. Proc. CADE-10, Springer LNCS 449, 132–146, 1990.
Entwurf zuverlassiger Software 181 Beweise als Programme
Beweise als Programme: Eigenschaften
• Korrektheit des Programms ist garantiert
• Verschiedene Kalkule sind theoretisch aquivalent
– große praktische Unterschiede
– Sequenzenkalkule fur Mensch und Maschine geeignet
• Verschiedene Extraktionsverfahren
– beeinflussen Effizienz erzeugter Programme
• Beweisschritte zu atomar (Assemblerniveau)
– Beweise interaktiv kaum durchfuhrbar
– Automatisierung schwierig:
Analyse der Formel, Unifikation, Suche nach geeigneten Induktionen
7→ praktisch nur sinnvoll in Kombination mit Definitionen und Spezialtaktiken
Entwurf zuverlassiger Software
Lektion 10
Synthese durch Transformationen
1. Prinzip
2. Die LOPS-Strategie
– GUESS/DOMAIN
– GET-REC
– Programmkonstruktion
– Unterstutzende Spezialstrategien
Entwurf zuverlassiger Software 182 Synthese durch Transformationen
Syntheseparadigmen: Synthese durch Transformation
Gegeben sei die Spezifikation:
FUNCTION f(x:D):R WHERE I(x) RETURNS y SUCH THAT O(x,y)
1. Definiere neues Pradikat F uber D×R durch:
– ∀x:D.∀y:R. I(x) ⇒ (F(x,y) ⇔ O(x,y)).
2. Transformiere in aquivalente Formel der Gestalt:
– ∀x:D.∀y:R. I(x) ⇒ (F(x,y) ⇔ Of(x,y))
Of(x,y) darf nur aus erfullbaren Pradikaten und Vorkommen von F bestehen
3. Extrahiere aus der rekursiven Formel ein Programm.
– Alternativ: Interpretation als Logik-Programm
Forschung:
– Leistungsfahige Transformationsregeln
– effiziente Rewrite Techniken und Heuristiken
Entwurf zuverlassiger Software 183 Synthese durch Transformationen
Synthese durch Transformation
• Historisch: Optimierung von Programmen
– Erzeuge abstraktes, verifiziertes Prototyp-Programm
– Transformiere in aquivalentes effizienteres Programm
• Synthese: Optimierung “nichtausfuhrbarer” Programme
– Spezifikation ≡ nichtausfuhrbares Programm
– Transformiere in aquivalente, ausfuhrbare Formel
Individuelle Formalismen variieren sehr stark
• Forschung:
– effiziente Rewrite-Techniken
– Heuristiken zur Steuerung von Vorwartsinferenzen
Literatur:– R. M. Burstall, J. Darlington: A Transformation System for Developing Recursive Programs,
JACM 24:44-67, 1977.
– C. J. Hogger: Derivation of Logic Programs, JACM 28:372–392, 1981.
– Z. Manna, R. J. Waldinger: Synthesis: Dreams ⇒ Programs, IEEE.SE SE-5 (4):294–328, 1979.
Entwurf zuverlassiger Software 184 Synthese durch Transformationen
Transformationen
• Anwendung bedingter Ersetzungsregeln der Form
∀z:T. P(z) ⇒ ( Q(z) ⇔ Q’(z) )
“Ersetze Vorkommen von Q(z) durch Q’(z), falls Bedingung P(z) erfullt”
Aquivalenzen oder Verfeinerungen (Implikationen)
• Regeln ergeben sich aus
– Lemmata der Wissensbasis
– Dynamisch erzeugte Definitionen
– Elementare Tautologien und Abstraktionen
– Dynamisch erzeugte Kombinationen
• Kalkul nicht zielgerichtet
⇒ heuristische Steuerung notwendig
Entwurf zuverlassiger Software 185 Synthese durch Transformationen
Transformationen: Maximale Segmentsumme (1)
Bestimme maximale Summe Σp+qi=pL[i] der Teilfolgen einer Liste L
1. Definiere neues Pradikat maxseg:
∀L:Seq(Z).∀m:Z. L6=[] ⇒
maxseg(L,m) ⇔ m = MAX(⋃
Σqi=pL[i] |p ∈1..q | q ∈1..|L| )
2. Generalisiere: Einfuhrung eines Pradikats max aux:
∀L:Seq(Z).∀m:Z. L6=[] ⇒
maxseg(L,m) ⇔ ∃l:Z. max aux(L,m,l)
∀L:Seq(Z).∀m:Z. L6=[] ⇒
max aux(L,m,l) ⇔ m = MAX(⋃
Σqi=pL[i] |p ∈1..q | q ∈1..|L| )
∧ l = MAX(Σqi=1L[i] |q ∈1..|L| )
3. Transformation durch Anwendung von Lemmata
∀L:Seq(Z).∀m:Z. L6=[] ⇒ max aux(L,m,l)
⇔ |L|=1 ∧ m=L[1] ∧ l=L[1]
∨ |L|>1 ∧ ∃m’,l’:Z. l’ = MAX(Σqi=2L[i] | q ∈2..|L|
∧ m’ = MAX(⋃
Σqi=pL[i] |p ∈2..q | q ∈2..|L| )
∧ l=max(L[1],l’+L[1]) ∧ m=max(l,m’)
Entwurf zuverlassiger Software 186 Synthese durch Transformationen
Transformationen: Maximale Segmentsumme (2)
4. Umschreiben der Indizes relativ zu rest(L)
∀L:Seq(Z).∀m:Z. L 6=[] ⇒ max aux(L,m,l)
⇔ |L|=1 ∧ m=L[1] ∧ l=L[1]
∨ rest(L) 6=[]
∧ ∃m’,l’:Z. l’ = MAX(Σqi=1rest(L)[i] | q ∈1..|rest(L)|)
∧ m’= MAX(⋃
Σqi=prest(L)[i] |p ∈1..q | q ∈1..|rest(L)| )
∧ l=max(L[1],l’+L[1]) ∧ m=max(l,m’)
5. Einsetzen der Definition von max aux:
∀L:Seq(Z).∀m:Z. L 6=[] ⇒ max aux(L,m,l)
⇔ |L|=1 ∧ m=L[1] ∧ l=L[1]
∨ rest(L) 6=[] ∧ ∃m’,l’:Z. max aux(rest(L),m’,l’)
∧ l=max(L[1],l’+L[1]) ∧ m=max(l,m’)
6. PROLOG-artiges Programm
maxseg(L,m) :- max aux(L,l,m).
max aux([a],a,a).
max aux(a.L’,l,m):- max aux(L,m’,l’),max(a,l’+a,l),max(l,m’,m).
Entwurf zuverlassiger Software 187 Synthese durch Transformationen
Transformationen: Erzeugung funktionaler Programme
• Disjunktion 7−→ Fallunterscheidung
– Sind (D,R,I,O,body) und (D,R,I’,O’,body’) korrekt, dann auchFUNCTION f(x:D):R WHERE I(x) ∨I’(x) RETURNS y SUCH THAT O(x,y) ∨O’(x,y)
= if I(x) then body(x) else body’(x)
• Konjunktion 7−→ Einschrankung legaler Eingaben
• Existenzquantor 7−→ Generalisierung
– Sind (D,R,I,O,body) und (R,R’,J,O’,body’) korrekt, dann auchFUNCTION f(x:D):R’ WHERE I(x) ∧J(body(x))
RETURNS z SUCH THAT ∃y:R. O(x,y) ∧O’(y,z)
= body’(body(x))
• Rekursive Formel 7−→ Rekursion (Terminierungsbeweis notig!)
– fd:D6→D wohlfundierte ‘Reduktionsfunktion’ (keine absteigenden Ketten) und1. ∀x:D. I(x) ⇒ I(fd(x))
2. ∀x:D.∀y:R. I(x) ⇒ O(x,y) ⇔ ∃yr:R. O(fd(x),yr) ∧ OC(x,fd(x),yr,y)
3. FUNCTION fC(x,xr,yr:D×D×R):R WHERE I(x) RETURNS y SUCH THAT OC(x,xr,yr,y)
= body(x,xr,yr) ist korrekt
dann ist das folgende rekursive Programm korrekt
FUNCTION f(x:D):R WHERE I(x) RETURNS y SUCH THAT O(x,y) = body(x, fd(x), f(fd(x)))
Entwurf zuverlassiger Software 188 Synthese durch Transformationen
Programmerzeugung: Maximale Segmentsumme
Resultat der Transformationen
∀L:Seq(Z).∀m:Z. L 6=[] ⇒
maxseg(L,m) ⇔ ∃l:Z. max aux(L,m,l)
∀L:Seq(Z).∀m:Z. L 6=[] ⇒ max aux(L,m,l)
⇔ |L|=1 ∧ m=L[1] ∧ l=L[1]
∨ rest(L) 6=[] ∧ ∃m’,l’:Z. max aux(rest(L),m’,l’)
∧ l=max(L[1],l’+L[1]) ∧ m=max(l,m’)
Erzeugtes funktionales Programm
FUNCTION Maxseg(L:Seq(Z)):Z WHERE L6=[] RETURNS m SUCH THAT maxseg(L,m)
= snd( Max aux(L) )
FUNCTION Max aux(L:Seq(Z)):Z×Z WHERE L6=[]
RETURNS m,l SUCH THAT max aux(L,m,l)
= if |L|=1 then (L[1],L[1])
else let (m’,l’) = Max aux(rest(L)) in
let l=max(L[1],l’+L[1]) in
( max(l,m’), l)
Entwurf zuverlassiger Software 189 LOPS
LOPS – LOgische ProgrammSynthese
• Syntaktische Transformationen logischer Formeln
kontrolliert durch semantische Informationen
• Kombination einer kleinen Menge von Teilstrategien
– GUESS/DOMAIN: Raten einer Teillosung
– GET-REC: Rekursionseinfuhrung
– Vereinfachung
– Erzeugung von Unterproblemen
– Test auf Auswertbarkeit von Teilformeln
– ...
• Algorithmenkonstruktion:
– Umformung rekursiver Formeln in logische/funktionale Programme
Literatur:– Wolfgang Bibel: Syntax–directed, Semantics–supported Program Synthesis AIJ 14:243–261, 1980
Entwurf zuverlassiger Software 190 LOPS
LOPS: Maximum-Synthese (1)
Bestimme das Maximum m einer nichtleeren Menge S:Set(Z)
0. Definiere neues Pradikat max durch
∀S:Set(Z).∀m:Z. S6=∅ ⇒ max(S,m) ⇔ (m ∈S ∧ ∀x ∈S. x≤m)
Markiere S als Input-Variable und m als Output-Variable.
1. Die Formel ist nicht auswertbar
2. GUESS/DOMAIN:
– Rate eine Zahl g. Beschranke Auswahlmoglichkeiten auf Werte g ∈S
– Geratene Zahl ist direkte Losung oder Grundlage fur Problemreduktion
und Einfuhrung von Rekursion
Transformiere Ausgangsformel in
∀S:Set(Z).∀m:Z. S6=∅ ⇒
max(S,m) ⇔ ∃g:Z. g ∈S ∧ (m ∈S ∧ ∀x ∈S.x≤m ∧ g6=m ∨ g=m)
Entwurf zuverlassiger Software 191 LOPS
LOPS: Strategie GUESS/DOMAIN
Gezieltes Raten liefert verwertbare Information
Transformiere:
∀x:D.∀y:R. I(x) ⇒ P(x,y) ⇔ O(x,y)
in die Form
∀x:D.∀y:R. I(x) ⇒ P(x,y)
⇔ ∃g:G. DC(x,g) ∧ (O(x,y) ∧ t(g,y) ∨ ¬t(g,y))
Parameter der GUESS-Transformation
• G: Datentyp der “Guess-Variable” g. 7→ Wissensbank
In einfachen Fallen identisch mit R
• t: Tautologie-Relation zwischen y und g. 7→ Wissensbank
In einfachen Fallen die Gleichheit, sonst “g ist Teil von y”
• Bedingung an Losungen, von denen Teile geraten werden konnen
Pradikat displayable(y) = ∃g:G.t(g,y) 7→ Wissensbank
• DC: Bedingung an sinnvolle Ratewerte (Domain von g) 7→ Heuristik DOMAIN
Entwurf zuverlassiger Software 192 LOPS
LOPS: Heuristik DOMAIN
Beschranke Ratemoglichkeiten auf leicht zu bestimmende Werte
und versuche, die Moglichkeit falscher Rateschritte klein zu halten
• Spezifikation (D,G,I,DC) muß erfullbar sein.
• Darstellbare Anteile von Losungen mussen erreichbar sein
g:G |∃y:R. O(x,y) ∧t(g,y) ⊆ g:G | DC(x,g)
Formal: DC notwendig fur darstellbare Anteile von Losungen
∀x:D.∀g:G. I(x) ⇒ (∃y:R. O(x,y) ∧ t(g,y)) ⇒ DC(x,g)
Im einfachen Fall: DC “Echte Teilformel” von O
• Menge ungeeigneter Werte (g:G | DC(x,g) ∧¬t(g,y)) soll klein sein
• Effizienter Algorithmus zur Losung von (D,G,I,DC) soll existieren
⇒ Benutzerhilfe notig fur letzte beiden Kriterien
Entwurf zuverlassiger Software 193 LOPS
LOPS: Zerlegung in Teilprobleme
Zerlege Resultat von GUESS/DOMAIN in drei Teilprobleme
∀x:D.∀y:R. I(x) ⇒ P(x,y) ⇔ ∃g:G. DC(x,g) ∧ (O1(x,g,y) ∨O2(x,g,y))
∀x:D.∀g:G.∀y:R. I(x) ∧ DC(x,g) ⇒ O1(x,g,y) ⇔ O(x,y) ∧ t(g,y)
∀x:D.∀g:G.∀y:R. I(x) ∧ DC(x,g) ⇒ O2(x,g,y) ⇔ O(x,y) ∧ ¬t(g,y)
⇒ Losung der Unterprobleme bestimmt Gesamtlosung, wenn DC erfullbar
LOPS: Maximum-Synthese (2)
3....S 6=∅ ⇒ max(S,m) ⇔ ∃g:Z. g ∈S ∧ (m ∈S ∧ ∀x ∈S.x≤m ∧, g6=m ∨g=m) wird zerlegt in
∀S:Set(Z).∀m:Z. S6=∅ ⇒
max(S,m) ⇔ ∃g:Z. g ∈S ∧ (max1(S,g,m) ∨ max2(S,g,m))
∀S:Set(Z).∀g,m:Z. S6=∅ ∧ g ∈S ⇒
max1(S,g,m) ⇔ m ∈S ∧ ∀x ∈S. x≤m ∧ g6=m
∀S:Set(Z).∀g,m:Z. S6=∅ ∧ g ∈S ⇒
max2(S,g,m) ⇔ m ∈S ∧ ∀x ∈S. x≤m ∧ g=m
DC(g,S) = g ∈S ist erfullbar, Losung des dritten Teilproblems steht fest
Entwurf zuverlassiger Software 194 LOPS
LOPS: Maximum-Synthese (3)
4. GET-REC: Transformiere in rekursive Variante der Ausgangsformel
– Instantiiere Rekursionsschema fur endliche Mengen
“Versuche, P(S) durch P(S-g) auszudrucken” 7→ Terminierung garantiert
– Wende Lemmata der Wissensbank an
1. S6=∅ ⇔ S=g ∨ S-g 6= ∅
2. g ∈S ⇒ g6=m ∧ m ∈S ⇔ g6=m ∧ m ∈S-g
3. g ∈S ⇒ ∀x ∈S. x≤m ⇔ g≤m ∧ ∀x ∈S-g. x≤m
– Zerlege Vorbedingung in Basis- & Rekursionsfall
Resultat der Transformation
∀S:Set(Z).∀g,m:Z. S=g ∧ g ∈S ⇒
max1(S,g,m) ⇔ m ∈S ∧ ∀x ∈S. x≤m ∧ g6=m
∀S:Set(Z).∀g,m:Z. S-g 6=∅ ∧ g ∈S ⇒
max1(S,g,m) ⇔ m ∈S-g ∧ ∀x ∈S-g. x≤m ∧ g6=m ∧ g≤m
Entwurf zuverlassiger Software 195 LOPS
LOPS: Strategie GET-REC
Goal-oriented Equivalence Transformation
• Ziel: Rekursive Form
– Disjunktion in der Input-Bedingung
– Konjunktionen in der Output-Bedingung
– Außer O nur erfullbare Pradikate
• Methode: Suche nach geeigneten Lemmata
– Beziehung zwischen reduzierter und nichtreduzierter Form der Pradikate
• Hilfsmittel:
– Wohlfundiertes Rekursionsschema 7→ Wissensbank
– Suchheuristik
Entwurf zuverlassiger Software 196 LOPS
LOPS: Maximum-Synthese (4)
5. Simplifikation durch gerichtete Lemmata
∀S:Set(Z).∀m:Z. S 6=∅ ⇒
max(S,m) ⇔ ∃g:Z. g ∈S ∧ (max1(S,g,m) ∨ max2(S,g,m))
∀S:Set(Z).∀g,m:Z. S=g ⇒
max1(S,g,m) ⇔ false
∀S:Set(Z).∀g,m:Z. S-g 6=∅ ∧ g ∈S ⇒
max1(S,g,m) ⇔ max(S-g,m) ∧ g<m
∀S:Set(Z).∀g,m:Z. g ∈S ⇒
max2(S,g,m) ⇔ ∀x ∈S. x≤g ∧ g=m
6. Programmkonstruktion: Erzeugtes Logik Programm
max(S,M) :- member(G,S), max-aux(S,G,M).
max-aux(S,G,M) :- setminus(S,G,SminusG),
max(SminusG,M), less(G,M),!.
max-aux(S,M,M) :- setless(S,M).
Entwurf zuverlassiger Software 197 LOPS
LOPS: Konstruktion logischer Programme
• ∀ entfallt im Programmkopf
• ∃ entfallt im Programmkorper
• Disjunktionen werden ersetzt durch einen Aufruf.
– Der zugehorige Programmkopf wird entsprechend umbenannt
• Vorbedingungen entfallen
• Unerfullbare Teile entfallen
• Gleichheit wird verschoben in den Programmkopf
• Funktionsaufrufe werden ersetzt durch pradikative
Programme mit neuer Ausgabevariable
Entwurf zuverlassiger Software 198 LOPS
LOPS: Sonstige Strategien
• Allgemeine Techniken
– Normalisierung und Simplifikation (gerichtete Lemmata)
– Unterproblem-Erzeugung (fur komplexere Ausdrucke)
• Unterstutzung von GUESS/DOMAIN
– Preprocessing (Abspaltung von Outputs ohne darstellbare Anteile)
– GET-RNV: Reduziere die Zahl der Ausgabevariablen
– GET-SOC: Spalte Ausgabebedingungen
– CHVAR: Wahle bestgeeigneteste Ausgabevariable
– DEPEND: Bestimme Abhangigkeiten zwischen den Ausgabevariablen
• Unterstutzung von GET-REC
– GET-EP: Ersetzung durch auswertbare Pradikate
Entwurf zuverlassiger Software 199 LOPS
LOPS: Preprocessing fur GUESS
• Abspaltung von Eingaben, die kein GUESS erlauben
– Ausgabewerte ohne darstellbare Anteile (d.h. ¬∃g:G.t(g,y))
– zugehorige Eingaben haben einfache Losungen (aus y:R |¬displayable(y))
• Bestimme Pradikat prim mit
∀x:D. (∃y:R. I(x) ∧ O(x,y) ∧ ¬displayable(y)) ⇒ prim(x)
∀x:D. I(x) ∧ prim(x) ⇒ ∃y:R. O(x,y)
Herleitung: Vereinfachung von ∃y:R. I(x) ∧ O(x,y) ∧ ¬displayable(y)
• Transformation: Zerlege ∀x:D.∀y:R. I(x) ⇒ P(x,y) ⇔ O(x,y) in
∀x:D.∀y:R. I(x) ∧ prim(x) ⇒ P(x,y) ⇔ O(x,y)
∀x:D.∀y:R. I(x) ∧ ¬prim(x) ⇒ P(x,y) ⇔ O(x,y)
Entwurf zuverlassiger Software 200 LOPS
GET-RNV — Reduce Number of Output Variables
• Anwendbar bei Programmen mit mehreren Ausgabewerten
• Ziel: Veringere Anzahl der Ausgabevariablen
– Suche unmittelbare Abhangigkeiten zwischen Variablen
– Beschreibe Variable als Funktion der anderen
• ∀x:D.∀(y,y’):R×R’. I(x) ⇒ P(x,(y,y’)) ⇔ O(x,(y,y’))
wird transformiert in
∀x:D.∀(y,y’):R×R’. I(x) ⇒ P(x,(y,y’)) ⇔ P’(x,y) ∧ y’=f(x,y)
∀x:D.∀y:R. I(x) ⇒ P’(x,y) ⇔ O(x,y,f(x,y))
Beispiel: Bestimme das i-t-großte Element einer Menge S
∀S,i.∀S1,a,S2. i ∈1..|S| ⇒ FIND((S,i),(S1,a,S2))
⇔ S=S1∪a∪S2 ∧ ∀x ∈S1.x<a ∧ ∀x ∈S2.a<x ∧ |S1|=i-1
Drucke S2 durch S1 und a aus
∀S,i.∀S1,a,S2. i ∈1..|S| ⇒ FIND((S,i),(S1,a,S2))
⇔ FIND’((S,i),(S1,a)) ∧ S2= S\(S1+a)
∀S,i.∀S1,a. i ∈1..|S| ⇒ FIND’((S,i),(S1,a))
⇔ a ∈S ∧ S1⊆S-a ∧ ∀x ∈S1.x<a ∧ ∀x ∈ S\(S1+a) .a<x ∧ |S1|=i-1
Entwurf zuverlassiger Software 201 LOPS
GET-SOC — Separate Output Conditions
• Anwendbar bei Programmen mit mehreren Ausgabewerten
– wenn GET-RNV nicht zum Ziel fuhrt
• Zerlege Output Bedingungen in unabhangige Teile
∀x:D.∀(y,y’):R×R’. I(x) ⇒ P(x,(y,y’)) ⇔ O(x,(y,y’))
wird transformiert in
∀x:D.∀(y,y’):R×R’. I(x) ⇒ P(x,(y,y’)) ⇔ P1(x,y) ∧ P2(x,y’)
∀x:D.∀(y,y’):R×R’. I(x) ⇒ P1(x,y) ⇔ O1(x,y)
∀x:D.∀(y,y’):R×R’. I(x) ⇒ P2(x,y) ⇔ O2(x,y)
• Zerlegung geschieht auf rein syntaktischer Basis
– Aufsammeln von Konjunktionsgliedern, in denen nur y bzw. y’ vorkommt
Entwurf zuverlassiger Software 202 LOPS
CHVAR — Choose Output-Variable
• Anwendbar bei Programmen mit mehreren Ausgabewerten
– ∀x:D.∀y,y’:R×R’. I(x) ⇒ P(x,(y,y’)) ⇔ O(x,(y,y’))
– wenn GET-RNV und GET-SOC nicht zum Ziel fuhren
• Versuche hierarchische Losung:
– Berechnung des zweiten Ausgabewertes wird Teilproblem bei Berechnung des ersten
– Guessing zunachst auf ‘außerer’ Variable
– Guessing auf ‘innerer’ Variable wahrend Synthese der entstandenen Teilprobleme
• Lege heuristisch fest, welche Variable zuerst verwendet wird
– Wahle Guess-Schema fur einzelne Ausgabevariablen und fuhre DOMAIN aus
– Vergleiche | y:R | ∃g:G.DC(x,g) ∧t(g,y) |
mit | y’:R’ | ∃g’:G’.DC’(x,g’)∧t’(g’,y’) |
– Wahle Variable mit kleinerer Anzahl von Ratemoglichkeiten
Entwurf zuverlassiger Software 203 LOPS
DEPEND — Bestimme Abhangigkeiten der Ausgaben
• Anwendbar nach CHVAR
– Bestimme Abhangigkeit der Ausgabevariablen von außerster Guess-Variable (y)
– ahnlich wie GET-RNV aber erheblich aufwendiger
• Nach GUESS auf y suche maximale Bedingung O’(x,g,y,y’),
die in beiden Teilproblemen losbar ist
– Heuristik: großte Menge von Konjunktionsgliedern, in denen y’ vorkommt
• Synthetisiere separat (mit Eingabevariablen x,g,y!)
∀x:D.∀g:G.∀y:R.∀y’:R’.
I(x) ∧ DC(x,g) ⇒ P’(x,g,y,y’)⇔ O’(x,y,y’)
• Ersetze im ursprunglichen Problem y’ durch f’(x,g,y)
Entwurf zuverlassiger Software 204 LOPS
GET-EP — Rewrite into Evaluable Predicates
• Simplifikation: ersetze Konjunktionsglieder der Ausgabeformel
– suche Konjunktionsglieder, die nicht unmittelbar auswertbar sind
– ersetze durch aquivalente auswertbare Pradikate
• Ziel: vereinfachte Erzeugung von (Logik-)Programmen
– vereinfachter Test auf Auswertbarkeit
– effizientere Anordnung von Pradikaten im Programm
• Hilfreich, aber nicht unbedingt notwendig
Beispiel: Maximum-Simplifikation
∀S:Set(Z).∀g,m:Z. S6=∅ ∧ g ∈S ⇒
max2(S,g,m) ⇔ m ∈S ∧ ∀x ∈S. x≤m ∧ g=m
Ohne g=m ist ∀x ∈S. x≤m nicht auswertbar. Ersetze durch ∀x ∈S. x≤g
∀S:Set(Z).∀g,m:Z. S6=∅ ∧ g ∈S ⇒
max2(S,g,m) ⇔ ∀x ∈S. x≤g ∧ g=m
Entwurf zuverlassiger Software 205 LOPS
LOPS: Gesamtstrategie (1)
Gegeben x:D, y:R, I(x) und O(x,y)
1. Definiere Pradikat P durch ∀x:D.∀y:R. I(x) ⇒ P(x,y) ⇔ O(x,y)
– Markiere x als Eingabevariable
2. GUESS-Phase:
– Bei mehreren Ausgabevariablen versuche Problemreduktion mit GET-RNV,
GET-SOC oder CHVAR/DEPEND
(a) Wahle GUESS-Schema (R, G, displayable,t) aus der Wissensbank
(b) Enthalt R nichtdarstellbare Ausgaben, so spalte diese ab.
(c) Bestimme DC mit der Heuristik DOMAIN
(d) Transformiere die Ausgangsformel durch Hinzufugen der geratenen Information.
(e) Spalte Problem in Teilprobleme und behandle diese einzeln.
Markiere g als Eingabevariable der neuen Hilfspradikate.
Entwurf zuverlassiger Software 206 LOPS
LOPS: Gesamtstrategie (2)
3. Teste Auswertbarkeit und Widerspruchlichkeit heuristisch
– Heuristik: in wenigen Schritten nachweisbar
– einfaches Guessing 7→ trivial losbare Teilprobleme
– induktive Datenstrukturen 7→ widerspruchliche Teilprobleme
4. GET-REC-Phase
(a) Wahle Rekursionsschema (D,R,) aus der Wissensbank.
(b) Schreibe Formel um in rekursive Variante der Ausgangsformel:
∀x:D.∀y:R.∀g:G. Ibase(x,g) ∨I(xg) ⇒
P’(x,g,y) ⇔ ∃yr.O(xg,yr) ∧ Orec(x,g,yr,y)
(c) Spalte nichtrekursiven Losungen (Ibase) ab.
Ersetze Konjunktionsglieder aus O durch P.
5. Vereinfache Formeln soweit wie moglich und teste Auswertbarkeit
– Starte LOPS erneut, wenn Formel nicht auswertbar
6. Extrahiere aus der rekursiven Formel ein Programm
Entwurf zuverlassiger Software 207 LOPS
LOPS Strategie: Sortieralgorithmus
FUNCTION sort(L:Seq(Z)):Seq(Z) RETURNS S SUCH THAT rearranges(L,S) ∧ ordered(S)
1. Definiere: ∀L,S:Seq(Z). true ⇒ SORT(L,S) ⇔ rearranges(L,S) ∧ ordered(S)
2.(a) Wahle GUESS-Schema G≡Z, displayable(S)≡S6=[], t(g,S)≡g=first(S)
(b) ∃S:Seq(Z). SORT(L,S) ∧¬(S6=[]) ⇒ L=[]≡prim(L) B.2.26.1
(c) ∃S:Seq(Z). L 6=[] ∧SORT(L,S) ∧g=first(S) ⇒ g ∈L ∧∀x ∈L.x≥g B.2: 9.3/26.3/26.12/ordered
Losungsfunktion fur DC(L,g): λL. min(L)
(d) Teilprobleme:g ∈L ∧∀x ∈L.x≥g ⇒ SORT
1(L,g,S) ⇔ rearranges(L,S) ∧ ordered(S) ∧ g=first(S)
g ∈L ∧∀x ∈L.x≥g ⇒ SORT2(L,g,S) ⇔ rearranges(L,S) ∧ ordered(S) ∧ g6=first(S)
3. Teilproblem SORT2ist unerfullbar
4. (a) Rekursionsschema fur Seq(Z)×Z: Lg ≡ L-g
(b) g ∈L ∧∀x ∈L.x≥g ⇒ SORT1(L,g,S) ⇔ ∃S’:Seq(Z).SORT(L-g,S’) ∧ S=g.S’
Funktion fur Rekursionsanpassung: λL,g,S’. g.S’ B.2: 26.15/3.2/2.3/25.2/fold SORT
5. L = [] ⇒ SORT(L,S) ⇔ S=[] auswertbar
L6=[] ⇒ SORT(L,S) ⇔ ∃g:Z. g ∈L ∧∀x ∈L.x≥g ∧SORT1(L,g,S) auswertbar
g ∈L ∧∀x ∈L.x≥g ⇒ SORT1(L,g,S) ⇔ ∃S’:Seq(Z).SORT(L-g,S’) ∧ S=g.S’ auswertbar
6. Funktionale LosungFUNCTION sort(L:Seq(Z)):Seq(Z) RETURNS S SUCH THAT rearranges(L,S) ∧ ordered(S)
= if L=[] then [] else let g=min(L) in g.sort(L-g)
Entwurf zuverlassiger Software
Lektion 12
Synthese durch Algorithmenschemata
1. Grundprinzip
2. Theoretische Grundlagen
3. Syntheseverfahren und Verfeinerungen
Entwurf zuverlassiger Software 208 Algorithmentheorien
Syntheseparadigmen: Algorithmenschemata
Erzeuge Algorithmus in einem Schritt
Gegeben sei die Spezifikation:
FUNCTION f(x:D):R WHERE I(x) RETURNS y SUCH THAT O(x,y)
1. Wahle algorithmischen Klasse und (partielles) Schema
2. Verfeinere Schema auf das Problem
Vervollstandige unbesetzte Parameter
3. Instantiiere Algorithmenschema
Forschung:
– Analyse der Struktur einer Klasse von Algorithmen
– Komponenten und Axiome fur Korrektheit
– Techniken zur Verfeinerung von Standardlosungen
Entwurf zuverlassiger Software 209 Algorithmentheorien
Synthese mit Algorithmenschemata
• Historisch: High-Level Transformation– Erzeuge lauffahigen Algorithmus in einem Schritt – Optimiere nachtraglich
• Vorarbeiten: Strukturanalyse fur algorithmische Klasse– Identifizierung von Komponenten und Axiomen
– Korrektheitsbeweis fur abstraktes Algorithmenschema
– Erstellung von konkreten (partiellen) Standardlosungsstrukturen
+ Techniken zur Verfeinerung von Standardlosungen
• Syntheseprozeß:– Bestimmung der fehlenden Komponenten
– Nachweis der Axiome
– Instantiierung des Algorithmenschemas
• Forschung: Formalisierung als algebraische Theorien– 3 Ebenen: Allgemeines Konzept — algorithmische Theorien — konkrete Probleme
– Entwurf spezialisierter Strategien fur jede Algorithmenklasse
Entwurf zuverlassiger Software 210 Algorithmentheorien
Hierarchie algorithmischer Theorien
Allgemeine Problemstruktur
Generate & Test
Lokale Struktur
LokalsucheSimulated Annealing
Reduktionsstruktur
KomplementierungSiebe
∧ -Reduktion
statischProblemreduktion(Operator Match)
rekursivDivide & Conquer
∨ -Reduktion
statischBedingungen
Fallanalyse
rekursivGlobalsuche
BinarsucheBacktracking
Branch & Bound (A∗)
∧ - ∨ -ReduktionDynamische Programmierung
Branch & Bound (AO∗)Spielbaum-Suche
XXXXXXXXXXXXXXXXXXXXXX
PPPPPPPPPPPPPPPPP
PPPPPPPPPPPPPPPPP
@@
@@
@@
@@
@@
@
Entwurf zuverlassiger Software 211 Algorithmentheorien
Algorithmenschemata: Literatur
Douglas R. Smith and Michael R. Lowry
Algorithm Theories and Design Tactics,
Science of Computer Programming 14:305–321
Douglas R. Smith
KIDS — A Knowledge-Based Software Development system,
in: Michael R. Lowry and Robert D. McCartney, ed.
Automating Software Design, AAAI Press, 1991, p.483–514.
Douglas R. Smith
Top-Down Synthesis of Divide-and-Conquer Algorithms, AIJ 27:43–96, 1985
Douglas R. Smith
Structure and Design of Global Search Algorithms
Structure and Design of Problem Reduction Generators
Technical Report, Kestrel Institute
Michael R. Lowry
Structure and Design of Local Search Algorithms
Proceedings, AAAI Workshop on Software Design, p.88–94
Entwurf zuverlassiger Software 212 Algorithmentheorien
Sortierung: Divide & Conquer Algorithmus
• Problemspezifikation (SORT(L,S) = rearranges(L,S) ∧ ordered(S))
FUNCTION sort(L:Seq(Z)):Seq(Z) RETURNS S SUCH THAT SORT(L,S)
• Grundstruktur von Divide & Conquer AlgorithmenFUNCTION F(x:D):R WHERE I(x) RETURNS y SUCH THAT O(x,y)
= if primitive(x) then Directly-solve(x)
else (Compose G×F Decompose) (x)
• Komponenten eines Sortieralgorithmusprimitive :≡ λL. L=[]
Directly-solve :≡ λL. []
Decompose :≡ λL. ( L<L[|L|/2], L=L[|L|/2], L>L[|L|/2] )
L<a ≡ [ x|x ∈L ∧x<a ]
G :≡ sort× λS.S
Compose :≡ λS1,S
2,S
3. S
1S
2S
3)
• Instantiierter Divide & Conquer AlgorithmusFUNCTION sort(L:Seq(Z)):Seq(Z) RETURNS S SUCH THAT SORT(L,S)
= if L=[] then [] else let a = L[|L|/2]
in let L1= [ x|x ∈L ∧x<a ]
and L2= [ x|x ∈L ∧x=a ]
and L3= [ x|x ∈L ∧x>a ]
in sort(L1) L
2 sort(L
3)
Entwurf zuverlassiger Software 213 Algorithmentheorien
Algebraische Theorien – Grundbegriffe
• Formale Theorie: Tripel T = (S, Ω, Ax)
– S: Menge von Sortennamen (Namen fur Datentypen)
– Ω: Familie von Operationsnamen (zusammen mit Typisierung)
– Ax: Menge von Axiomen fur Datentypen und Operationen
• Struktur fur T :
– Menge von Datentypen und Operationen, typisiert gemaß Ω
• Modell fur T :
– Struktur T , die alle Axiome aus T erfullt
• Theorie T 1 erweitert T 2:
– Sortennamen, Operationsnamen und Axiome von T 2 existieren auch in T 1
Struktur T1 erweitert T2:
– Datentypen und Operationen von T2 existieren auch in T1
(gleiche Typisierung bezuglich T 2!)
Entwurf zuverlassiger Software 214 Algorithmentheorien
Algorithmenschemata als algebraische Theorien
• TSPEC: algebraische Theorie der Spezifikationen
– (D,R, I:D→B, O:D×R→B, ∅)
P Problemtheorie:
– P erweitert TSPEC (P enthalt Programmspezifikation)
• TPROG: algebraische Theorie der Programme
– ( D,R, I: D→B, O: D×R→B,body: D6→R,
∀x:D. I(x)⇒ O(x,body(x)) )
P Programmtheorie:
– P erweitert TPROG
• A Algorithmentheorie:
– Problemtheorie mit kanonischer Erweiterung zu Programmtheorie
– Es gibt abstraktes Programmschema BODY mit der Eigenschaft(specA,BODY(A)) korrekt fur jedes Modell A von A
“Fur jedes Modell A existiert Standardlosung der Spezifikation specA”
Entwurf zuverlassiger Software 215 Algorithmentheorien
Divide & Conquer Schema als Algorithmentheorie
SD&C ≡ D, R, D’, R’
ΩD&C ≡ I: D→B, O: D×R→ B, OD: D×D’×D→ B, I’: D’→B, O’: D’×R’→ B,
OC: R’×R×R→ B, : D×D→ B, Decompose: D→ D’×D, G: D’→R’,
Compose: R’×R→ R, Directly-solve:D→R, primitive:D→B
AxD&C ≡ FUNCTION Fp(x:D):R WHERE I(x) ∧ primitive(x) RETURNS y SUCH THAT O(x,y)= Directly-solve(x) korrekt,
OD(x,y’,y) ∧ O(y,z) ∧ O’(y’,z’) ∧ OC(z,z’,t) ⇒ O(x,t),
FUNCTION Fd(x:D):D’×D WHERE I(x) ∧ ¬primitive(x)
RETURNS y’,y SUCH THAT I’(y’) ∧I(y) ∧ xy ∧OD(x,y’,y) = Decompose(x) ‘’,
FUNCTION Fc(z,z’:R×R’):R RETURNS t SUCH THAT OC(z,z’,t) = Compose(z,z’) ‘’,
FUNCTION FG(y’:D’):R’ WHERE I’(y’) RETURNS z’ SUCH THAT O’(y’,z’) = G(y’) ‘’,
ist wohlfundierte Ordnung auf D
BODY(A) = FUNCTION F(x:D):R WHERE I(x) RETURNS y SUCH THAT O(x,y)
= if primitive(x) then Directly-solve(x)
else (Compose G×F Decompose) (x)
A = (D, R, D’, R’, I, O, OD, I’, O’, OC, , Decompose, G, Compose, Directly-solve, primitive)
BODY(A) ist korrekt, wenn A alle obigen Axiome erfullt
Entwurf zuverlassiger Software 216 Algorithmentheorien
Algorithmenschemata: Syntheseverfahren
Satz: Spezifikation spec = (D,R,I,O) ist erfullbar, wenn es eine Algorithmentheorie A
und ein Modell A fur A gibt, welches die Struktur Tspec = (D,R, I,O) erweitert
Methode:
– Wahle Algorithmentheorie A,
– erweitere Tspec zu Modell A von A
– Instantiiere BODY(A) und extrahiere Programmkomponenten
SyntheseSpezifikation
Tspec--
TSPEC*
Erweiterung:Komponentensuche
*
*Theorie-Erweiterung:
Komponenten+Axiome
A
Modell
A
-
-Erweiterung mit BODY(A)
Kanonische Theorie-Erweiterung: BODY + Korrektheitsaxiom P
PTPROG
Programmkonstruktion:Extraktion relevanter Komponenten
Programm
Tprog
Entwurf zuverlassiger Software 217 Algorithmentheorien
Algorithmenschemata: Verfeinertes Syntheseverfahren
spec reduzierbar auf spec′:– Eingabebedingung (nach Transformation) starker, Ausgabebedingung schwacher– ∀x:D. I(x) ⇒ ∃x’:D’. I’(x) ∧ ∀y’:R’. O(x’,y’) ⇒ ∃y:R.O(x,y)
Satz: spec= (D,R,I,O) ist erfullbar, wenn es eine Algorithmentheorie A und einModell A fur A gibt, so daß spec reduzierbar auf specA
⇓Methode: “Operator match”
– Wahle Algorithmentheorie A und allgemeines Modell A von A– Zeige: spec reduzierbar auf specA 7−→ Substitutionen σ und θ
– Spezialisiere body(A) zu λx. σ(x,body(A)(θ(x)))
D’,I’ R’,O’
D,I R,O
6
?
θ σspec spec’
-body’
-body(x) = σ(θ(x), body’(θ(x)))
Entwurf zuverlassiger Software 218 Algorithmentheorien
Verfeinertes Syntheseverfahren: mengenwertige Probleme
spec′ generalisiert spec:– Eingabebedingung (nach Transformation) und Ausgabebedingung schwacher– ∀x:D. I(x) ⇒ ∃x’:D’. I’(x) ∧ ∀y:R. O(x,y) ⇒ O’(x’,y)
Satz: FUNCTION F(x:D):Set(R) WHERE I(x) RETURNS z |O(x,z)ist erfullbar, wenn es eine Algorithmentheorie A und ein Modell A fur A gibt, sodaß gilt: specA generalisiert (D,R,I ,O)
⇓Methode:
– Wahle Algorithmentheorie A und allgemeines Modell A von A– Zeige: specA generalisiert (D,R,I ,O) 7−→ Substitution θ:D→DA
– Spezialisiere body(A) zu λx. y | y ∈body(A)(θ(x)) ∧ O(x,y) (Optimierte Verfahren fur spezielle Algorithmentheorien moglich)
D’,I’
R’,O’
D,I R,O
6
θ spec spec’
?
PPPPPPPPPPPPPPPPPPPPPPPPPPPPq
body’
-body(x)= y|y ∈body’(θ(x)) ∧O(x,y)
Entwurf zuverlassiger Software 219 Algorithmentheorien
Algorithmenschemata: Vorteile fur Syntheseverfahren
1. Effizientes Syntheseverfahren
– Theoretische Untersuchungen entlasten Syntheseprozeß zur Laufzeit7→ Beweislast verlagert in Entwurf und Beweis der Algorithmentheorien
– Verfeinerung vorgefertigter Teillosungen (Modelle) moglich7→ zielgerichtetes Vorgehen, Verifikation der Axiome entfallt
– Echte Kooperation zwischen Mensch und ComputerMensch: Entwurfsentscheidungen — Computer: formale Details
2. Erzeugung effizienter Algorithmen
– Vorgabe einer effizienten Grundstruktur durch Theoreme
– Individuelle Optimierung nachtraglich
3. Wissensbasiertes Vorgehen
– Erkenntnisse uber Algorithmen als Theoreme verwendbar
4. Formales theoretisches Fundament
– Leicht in das Konzept beweisbasierter Systeme integrierbar
Entwurf zuverlassiger Software
Lektion 13
Synthese von Globalsuchalgorithmen
1. Grundstruktur von Globalsuchalgorithmen
2. Axiome und Korrektheit
3. Entwicklung einer Synthesestrategie
– Verfeinerung vorgefertigter Globalsuchtheorien
– Integration von Filtern
Entwurf zuverlassiger Software 220 Globalsuchalgorithmen
Globalsuchalgorithmen: Grundidee
• Beispiel: Suche alle Indizes des Wertes k in Liste L
FUNCTION osearch(L:Seq(Z),k:Z):Set(N) WHERE L6=[] ∧ ordered(L)
RETURNS i | i ∈1..|L| ∧L[i]=k
• Binares Suchen und Aufsammeln von Losungen– Spalte Indexmenge 1..|L| in 1..m und m+1..|L|– Durchsuche linke und rechte Halfte nach gleichem Verfahren– Vereinige jeweilige Losungsmengen
• Vereinfachung des Verwaltungsaufwands– Verwalte Grenzen l und r der Indexmengen als Suchraumdeskriptoren– Sinnvoll nur wenn 1≤l≤r≤|L|
– Verwende Hilfsfunktion oaux(L,k,l,r) mit Initialaufruf oaux(L,k,1,|L|)
FUNCTION oaux(L:Seq(Z),k:Z,l:N,r:N):Set(N)
WHERE L6=[] ∧ordered(L) ∧1≤l≤r≤|L| RETURNS i | i ∈l..r ∧L[i]=k
⇒ Rekursives Durchlaufen des Suchraums
oaux(L,k,l,r) =
l falls l=r ∧L[l]=k
∅ falls l=r ∧L[l]6=koaux(L,k,l,m)∪ oaux(L,k,m+1,r) falls l<r; m=(l+r)/2
Entwurf zuverlassiger Software 221 Globalsuchalgorithmen
Globalsuchalgorithmen: einheitliche Darstellung
• Vereinheitlichung durch Mengendarstellung
oaux(L,k,l,r) = i | i ∈l..l ∧i=r ∧L[i]=k
∪⋃
oaux(L,k,n,m) | (n,m) ∈(l,(l+r)/2),((l+r)/2 + 1,r) | l<r
– Mengenschreibweise unabhangig von binarer Aufspaltung des Suchraums– (n,m) wird aus Aufspaltungsmenge ausgewahlt– Losungsmenge wird durch Vereinigung einer Losungsfamilie gebildet– Direkte Losung wird durch Extraktion aus l..l erzeugt
• Optimierung durch Einsatz von Filtern– Suche berucksichtigt nicht, daß Liste geordnet ist (⇒ linearer Algorithmus)– Suchraum n..m ohne Losung, falls L[n]>k oder L[m]>k– Erganze Filter L[n]≤k≤L[m] fur Aufspaltungsmenge (⇒ logarithmisch)
• Endgultige Form: effizienter, wohlstrukturierter AlgorithmusFUNCTION osearch(L:Seq(Z),k:Z):Set(N) WHERE L6=[] ∧ ordered(L)
RETURNS i | i ∈1..|L| ∧L[i]=k= if L[1]≤k≤L[|L|] then oaux(L,k,1,|L|) else ∅
FUNCTION oaux(L:Seq(Z),k:Z,l:N,r:N):Set(N)
WHERE L6=[] ∧ordered(L) ∧1≤l≤r≤|L| RETURNS i | i ∈l..r ∧L[i]=k = i | i ∈l..l ∧i=r ∧L[i]=k
∪⋃
oaux(L,k,n,m) | (n,m) ∈(l,(l+r)/2), ((l+r)/2 + 1,r) | l<r ∧L[n]≤k≤L[m]
Entwurf zuverlassiger Software 222 Globalsuchalgorithmen
Globalsuch-Algorithmen: Struktur und Komponenten
Bestimmung aller Losungen eines Problems
Grundstruktur: Manipulation von Kandidatenmengen
FUNCTION F(x:D):Set(R) WHERE I(x) RETURNS z | O(x,z)= if Φ(x,s0(x)) then Fgs(x,s0(x)) else ∅
FUNCTION Fgs(x,s:D×S):Set(R) WHERE I(x) ∧J(x,s) ∧Φ(x,s)RETURNS z | O(x,z) ∧sat(z,s)
= z | z ∈ext(s) ∧O(x,z) ∪⋃
Fgs(x,t) | t ∈split(x,s) ∧Φ(x,t)
• Deskriptoren s ∈ S fur Kandidatenmengen
J(x,s) : s sinnvoll fur x — sat(z,s) : z gehort zur “Menge” s
• Initialdeskriptor s0(x) ∈S – umfaßt alle Losungen
• Direkte Extraktion ext(s) ∈Set(R) von Losungskandidaten
• Suche: rekursive Aufspaltung split(x,s) ∈Set(S) von Deskriptoren
• notwendige Filter Φ(x,s) – Elimination unnotiger Deskriptoren
7→ Verallgemeinerung von Binarsuche, Backtracking, Branch-and-Bound
Vollstandig: jede berechenbare Funktion beschreibbar
Entwurf zuverlassiger Software 223 Globalsuchalgorithmen
Globalsuch-Algorithmen (Grundform): Korrektheit
FUNCTION F(x:D):Set(R) WHERE I(x) RETURNS z | O(x,z) = Fgs(x,s0(x))
FUNCTION Fgs(x,s:D×S):Set(R) WHERE I(x) ∧J(x,s) RETURNS z | O(x,z) ∧sat(z,s)
= z | z ∈ext(s) ∧O(x,z) ∪⋃
Fgs(x,t) | t ∈split(x,s)
ist korrekt, wenn 5 Axiome erfullt sind
1. Initialdeskriptor ist sinnvoll– I(x) ⇒ J(x,s
0(x))
2. Splitting sinnvoller Deskriptoren liefert sinnvolle Deskriptoren– I(x) ∧J(x,s) ⇒ ∀t ∈split(x,s).J(x,t)
3. Initialdeskriptor enthalt alle Losungen– I(x) ∧O(x,z) ⇒ sat(z,s
0(x))
4. Alle Losungen in endlich vielen Schritten extrahierbar– I(x) ∧J(x,s) ∧O(x,z) ⇒ sat(z,s) ⇔ ∃k:N.∃t ∈splitk(x,s). z ∈ext(t)
5. Splitting nur endlich oft durchfuhrbar (Wohlfundiertheit)– I(x) ∧J(x,s) ⇒ ∃k:N. splitk(x,s) =∅
G=((D,R,I,O),S,J,s0,sat,split,ext) wohlfundierte Globalsuchtheorie
Entwurf zuverlassiger Software 224 Globalsuchalgorithmen
Globalsuch-Algorithmen (Grundform): Korrektheitsbeweis
FUNCTION F(x:D):Set(R) WHERE I(x) RETURNS z | O(x,z) = Fgs(x,s0(x))
FUNCTION Fgs(x,s:D×S):Set(R) WHERE I(x) ∧J(x,s) RETURNS z | O(x,z) ∧sat(z,s)
= z | z ∈ext(s) ∧O(x,z) ∪⋃
Fgs(x,t) | t ∈split(x,s)
• Korrektheit von F folgt aus Korrektheit von Fgs mit Axiom 3 (& 1):
I(x) ∧J(x,s0(x)) ⇒ z | O(x,z) ∧sat(z,s0(x)) = z | O(x,z)
• Partielle Korrektheit von Fgs folgt aus Axiom 4 (& 2):
Def.: splitk(x,s) ≡ if k=0 then s else⋃
splitk−1(x,t) | t ∈split(x,s)
Satz: Halt Fgs(x,s) nach i Schritten an (spliti(x,s) = ∅), so ist das Resultat⋃
z | z ∈ext(t) ∧O(x,z) | t ∈⋃
splitj(x,s) | j ∈0..i-1 (Losungen, die extrahierbar sind aus Deskriptoren, die zu einem splitj(x,s) mit j<i gehoren)
Beweis durch Induktion uber i, Auffalten der Rekursion, Lemmata der Wissensbank
• Terminierung von Fgs folgt direkt aus Axiom 5
Entwurf zuverlassiger Software 225 Globalsuchalgorithmen
Globalsuchtheorie und Filter fur osearch
• Globalsuchtheorie gs osearch
D 7→ Seq(N)×N
R 7→ N
I 7→ λL,k. L6=[] ∧ordered(L)
O 7→ λL,k, i. i ∈1..|L| ∧L[i]=k
S 7→ Seq(N)×Seq(N)
J 7→ λL,k, l,r. 1≤l≤r≤|L|
s0 7→ λL,k. (1,|L|)
sat 7→ λi, l,r. i ∈l..r
split 7→ λL,k, l,r. if l<r then (l,(l+r)/2),((l+r)/2+ 1,r) else ∅
ext 7→ λl,r. if l=r then l else ∅
Alle 5 Axiome sind erfullt
• Filter Φ = λL,k,l,r. L[l]≤k≤L[r] ist ‘notwendig’– (∃i:N. i ∈l..r ∧i ∈1..|L| ∧L[i]=k) ⇒ L[l]≤k≤L[r]
gilt, wenn L6=[] ∧ordered(L)
Entwurf zuverlassiger Software 226 Globalsuchalgorithmen
Schematischer Globalsuchalgorithmus fur osearch
FUNCTION osearch(L:Seq(Z),k:Z):Set(N) WHERE L6=[] ∧ordered(L)
RETURNS i | i ∈1..|L| ∧L[i]=k= if L[1]≤k≤L[|L|] then oaux(L,k, 1,|L|) else ∅
FUNCTION oaux(L:Seq(Z),k:Z, l:N,r:N):Set(N)
WHERE L 6=[] ∧ordered(L) ∧1≤l≤r≤|L|
RETURNS i | i ∈1..|L| ∧L[i]=k ∧i ∈l..r = z | z ∈(if l=r then l else ∅) ∧ z ∈1..|L| ∧L[z]=k
∪⋃
oaux(L,k,n,m) |
(n,m) ∈(if l<r then (l,(l+r)/2), ((l+r)/2 + 1,r) else∅) ∧ L[n]≤k≤L[m]
Nach Optimierung durch SimplifikationenFUNCTION osearch(L:Seq(Z),k:Z):Set(N) WHERE L6=[] ∧ordered(L)
RETURNS i | i ∈1..|L| ∧L[i]=k= if L[1]≤k≤L[|L|] then oaux(L,k, 1,|L|) else ∅
FUNCTION oaux(L:Seq(Z),k:Z, l:N,r:N):Set(N)
WHERE L 6=[] ∧ordered(L) ∧1≤l≤r≤|L|
RETURNS i | i ∈1..|L| ∧L[i]=k ∧i ∈l..r = if l=r then if L[l]=k then l else ∅
else let m = (l+r)/2 in
(if L[l]≤k≤L[m] then oaux(L,k,l,m) else ∅)
∪ (if L[m+1]≤k≤L[r] then oaux(L,k,m+1,r) else ∅)
Entwurf zuverlassiger Software 227 Globalsuchalgorithmen
Synthese von Globalsuch-Algorithmen: Hilfsmittel
• Globalsuchtheorie G: allgemeine Suchstruktur fur R
– G=((D,R,I,O),S,J,s0,sat,split,ext) erfullt Axiome 1-4vorgefertigt in Wissensbank
• Filter Φ: verfeinert split-Operation– splitΦ(x,s) ≡ t | t ∈split(x,s) ∧Φ(x,t)
Wohlfundiertheit: splitΦ terminiert (= Axiom 5) vorgefertigt in Wissensbank
Notwendig: keine Losung wird eliminiert (7→ Axiom 4)– Φ(x,s) ⇐ ∃z:R. sat(z,s) ∧O(x,z), falls I(x) ∧J(x,s)
zur Laufzeit prufen, heuristischerganzen
Effizienzsteigerung durch starke notwendige Filter moglich
• Spezialisierungsmechanismus fur G und Φ
– Wahle G passend zum Ausgabebereich der Spezifikation spec = (D,R,I,O)
– Zeige: G generalisiert spec 7−→ Substitution θ:D→DG
– modifiziere G und Φ mit θ zu wohlfundierter Globalsuchtheorie fur spec
Entwurf zuverlassiger Software 228 Globalsuchalgorithmen
Globalsuchtheorie: Folgen L von Elementen einer endlichen Menge
S⊆α
Suche = Aufzahlung der Prafixe einer Folge
[]XXXXXXXXXXX
HHHHHH
x
1x
2x
3x4 x5 ...
@@@
AAA
@@@
AAA
@@@
AAA
@@@
AAA
x1x
1... x
2x
1... x
3x
1... x4x1
...
......
......
. . .
• Deskriptormengen: Folgen mit gemeinsamem Prafix V
• Splitting: Verlangern der Prafixsequenz
• Extraktion: Gesamte Prafixsequenz
gs seq set(α) ≡ D 7→ Set(α)
R 7→ Seq(α)
I 7→ λS. true
O 7→ λS, L. range(L)⊆S
S 7→ Seq(α)
J 7→ λS, V. range(V)⊆S
s0 7→ λS. []
sat 7→ λL, V. VvL
split 7→ λS, V. V·i|i ∈S
ext 7→ λV. V
Entwurf zuverlassiger Software 229 Globalsuchalgorithmen
Wohlfundiertheitsfilter fur gs seq set(α)
• Φ1(S,V) = |V|≤k
– Langenbegrenzung absolut
– Test einfach, Terminierung nach k Schritten, Baumgroße |S|k
• Φ2(S,V) = |V|≤k*|S|
– Langenbegrenzung relativ zur Große von S
– Test einfach, Terminierung nach k*|S| Schritten, Baumgroße |S|k∗|S|
• Φ3(S,V) = nodups(V)
– Folgen ohne doppelte Elemente
– Test aufwendiger, Terminierung nach |S| Schritten, Baumgroße |S| !
Entwurf zuverlassiger Software 230 Globalsuchalgorithmen
Spezialisierung von gs seq set(Z) und Φ3
Spezialisiere gs seq set(Z) und Φ3 auf das Costas-Arrays Problem
FUNCTION Costas (n:Z):Set(Seq(Z)) WHERE n≥1
RETURNS p | perm(p,1..n) ∧ ∀j ∈domain(p).nodups(dtrow(p,j))
1. Ausgabebereich R stimmt mit RG=Seq(Z) uberein
2. Eingabebereiche D=Z und DG=Set(Z) sind anzupassen
3. Keine Eingabebedingung zu prufen, da IG(S)=true.
4. Zeige ∀n:Z. n≥1 ⇒ ∃S:Set(Z).∀p:Seq(Z). O(n,p) ⇒ range(p)⊆S
– Heuristik: Suche Folgerungen von O(n,p), in denen range(p) vorkommt
– Auffalten von perm liefert: perm(p,1..n) ⇒ range(p)⊆ 1..n
– Wahle S:=1..n
5. Modifiziere gs seq set(Z) und Φ3 mit θ:=λn.1..n und (D,R,I,O)
Gθ = ((D,R,I,O), Seq(Z), λn,V.range(V)⊆1..n,λn.[], λL,V. VvL, λn,V.V·i|i ∈1..n, λV.V)
Φ3,θ(n,V) = Φ3(1..n,V) = nodups(V) notwendig fur Gθ!
Entwurf zuverlassiger Software 231 Globalsuchalgorithmen
Globalsuchalgorithmen: allgemeine Synthesesestrategie
Gegeben eine ProblemspezifikationFUNCTION F(x:D):Set(R) WHERE I(x) RETURNS y:R | O(x,y)
1. Wahle Globalsuchtheorie G mit Ausgabetyp R (Wissensbank)
2. Beweise ‘G generalisiert (D,R,I,O)’
Extrahiere Substitution θ aus dem Beweis und berechne Gθ
3. Wahle wf-Filter Φ fur G (Wissensbank)
Beweise ‘Φθ notwendig fur Gθ’
4. Bestimme zusatzlichen notwendigen Filter Ψ fur Gθ
– Eigenschaften von x und s, die leicht aus sat(z,s) ∧O(x,z) ableitbar sind
5. Instantiiere schematischen Globalsuchalgorithmus fur GΦ,θ,Ψ
FUNCTION F(x:D):Set(R) WHERE I(x) RETURNS z | O(x,z)
= if Φ(θ(x),s0(θ(x))) ∧Ψ(x,s
0(θ(x))) then Fgs(x,s0
(θ(x))) else ∅
FUNCTION Fgs(x,s:D×S):Set(R) WHERE I(x) ∧J(x,s) ∧Φ(θ(x),s) ∧Ψ(x,s)
RETURNS z | O(x,z) ∧sat(z,s)
= z | z ∈ext(s) ∧O(x,z) ∪⋃
Fgs(x,t) | t ∈split(θ(x),s) ∧Φ(θ(x),t) ∧Ψ(x,t)
Entwurf zuverlassiger Software 232 Globalsuchalgorithmen
Globalsuchalgorithmen: Costas Arrays Synthese
FUNCTION Costas (n:Z):Set( Seq(Z) ) WHERE n≥1
RETURNS p | perm(p,1..n) ∧ ∀j ∈domain(p).nodups(dtrow(p,j))
1. Wahle die Globalsuchtheorie G = gs seq set(Z)
2. Beweis fur ‘G generalisiert (D,R,I,O)’ liefert θ(n) := 1..n
3. Wahle wf-Filter Φ so, daß ‘Φθ notwendig fur Gθ’ beweisbar
perm(p,1..n) ∧ ∀j ∈domain(p).nodups(dtrow(p,j)) ∧ Vv p ⇒ Φ(1..n,V)
Leicht beweisbar nur fur Φ3(S,V) := nodups(V)
4. Aus perm(p,1..n) ∧ ∀j ∈domain(p).nodups(dtrow(p,j)) ∧ Vvpleite ab Ψ(n,V) := ∀i ∈domain(V).nodups(dtrow(V,j))
5. Instantiiere den Standard-Globalsuchalgorithmus
FUNCTION Costas (n:Z):Set( Seq(Z) ) WHERE n≥1
RETURNS p | perm(p,1..n) ∧ ∀j ∈domain(p).nodups(dtrow(p,j))= if nodups([]) ∧ ∀j ∈domain([]).nodups(dtrow([],j)) then Costasgs(n,[]) else ∅
FUNCTION Costasgs (n:Z,V:Seq(Z)):Set( Seq(Z) )
WHERE n≥1 ∧ range(V)⊆1..n ∧ nodups(V) ∧ ∀j ∈domain(V).nodups(dtrow(V,j))
RETURNS p | perm(p,1..n) ∧ Vvp ∧ ∀j ∈domain(p).nodups(dtrow(p,j))= p | p ∈V ∧ perm(p,1..n) ∧ ∀j ∈domain(p).nodups(dtrow(p,j))
∪⋃
Costasgs(n,W) | W ∈V·i|i ∈1..n ∧ nodups(W) ∧ ∀j ∈domain(W).nodups(dtrow(W,j))
Entwurf zuverlassiger Software 233 Globalsuchalgorithmen
Globalsuch-Strategie: Integration in Beweissysteme
• Formalisiere Grundkonzepte als Definitionen
– Globalsuchtheorie: Datenstruktur + Axiome
– Generalisierungseigenschaft
– Filter: Datenstruktur, Wohlfundiertheit, Notwendigkeit
– Verfeinerung und Spezialisierung
• Formalisiere vorgefertigte Objekte als Lemmata
– konkrete Globalsuchtheorien (mit Nachweis der Axiome)
– Wohlfundiertheitsfilter fur existierende Globalsuchtheorien (mit Nachweis)
• Beweise Theorem uber Globalsuchalgorithmen
– Erfullbarkeit folgt aus Existenz von G, θ, Φ und Ψ sowie Axiomen
• Schreibe Taktik zur Anwendung des Theorems
– Matching, Instantiierung, Suche in der Wissensbank
Entwurf zuverlassiger Software
Lektion 14
Synthese von Divide & Conquer Algorithmen
1. Struktur
2. Axiome und Korrektheit
3. Syntheseverfahren
– Strategie und Hilfsmittel
– Beispielsynthese: Sortieralgorithmen
Entwurf zuverlassiger Software 234 Divide & Conquer Algorithmen
Divide & Conquer Algorithmen: Grundidee
• ∧ -Reduktion: Aufteilen und Durchqueren– Divide: Zerlege Problem in kleinere Teilprobleme– Conquer: Lose Teilprobleme separat und setze Losungen zusammen
• Beispiel: Maximum einer nichtleeren ListeFUNCTION MAX(L:Seq(Z)):Z WHERE L6=[]RETURNS m SUCH THAT m ∈L ∧ ∀x ∈L. x≤m
= if |L|=1 then first(L)else let a,L’=L
in let m’=MAX(L’)in if a<m’ then m’ else a
– Direkte Losung first(L) fur primitive Eingaben (|L|=1)– Dekomposition mit Funktion FirstRest: L7→a,L’
– Simple Losung a=Id(a) fur a — Rekursive Losung m’=MAX(L’) fur L’– Komposition der Teillosungen a und m’ mit Funktion max
• Vereinheitlichung durch separierte DarstellungFUNCTION MAX(L:Seq(Z)):Z WHERE L6=[]RETURNS m SUCH THAT m ∈L ∧ ∀x ∈L. x≤m
= if |L|=1 then first(L)else (max (Id×MAX) FirstRest) (L)
Entwurf zuverlassiger Software 235 Divide & Conquer Algorithmen
Divide & Conquer Algorithmen: Allgemeine Struktur
Problemreduktion durch Eingabe-Dekomposition
FUNCTION F(x:D):R WHERE I(x) RETURNS y SUCH THAT O(x,y)
= if primitive(x) then Directly-solve(x)
else (Compose G×F Decompose)(x)
• Dekomposition Decompose(x) von Eingaben in Teilprobleme
• Rekursiver Aufruf F(y) — Hilfsfunktion G(y’)
– Zusammengesetzt zu G×F ≡ λy’,y.(G(y’),F(y))
• Bottom-up Komposition Compose(z,z’) von Teillosungen
– Notation: fg ≡ λx. f(g(x))
• Direkte Losung Directly-solve(x) fur ‘primitive’ Teilprobleme
• Kontrollpradikat primitive(x)
Entwurf zuverlassiger Software 236 Divide & Conquer Algorithmen
Divide & Conquer Algorithmen: Korrektheit
FUNCTION F(x:D):R WHERE I(x) RETURNS y SUCH THAT O(x,y)
= if primitive(x) then Directly-solve(x)
else (Compose G×F Decompose) (x)
ist korrekt, wenn 6 Axiome erfullt sind
1. Direkte Losung Directly-solve(x) erfullt O fur primitive Eingaben:
– FUNCTION Fp(x:D):R WHERE I(x) ∧ primitive(x) RETURNS y SUCH THAT O(x,y)
2. ‘Strong Problem Reduction Principle’:
– Ausgabebedingung O rekursiv zerlegbar in OD, O’ und OC
OD(x,y’,y) ∧ O’(y’,z’) ∧ O(y,z) ∧ OC(z’,z,t) ⇒ O(x,t)
3. Dekomposition Decompose(x) erfullt OD und ‘verkleinert’ Problem:– FUNCTION Fd(x:D):D’×D WHERE I(x) ∧ ¬primitive(x)
RETURNS y’,y SUCH THAT I’(y’) ∧I(y) ∧ xy ∧OD(x,y’,y)
4. Komposition Compose(z’,z) erfullt OC:
– FUNCTION Fc(z’,z:R’×R):R RETURNS t SUCH THAT OC(z’,z,t)
5. Hilfsfunktion G(y’) erfullt O’:
– FUNCTION FG(y’:D’):R’ WHERE I’(y’) RETURNS z’ SUCH THAT O’(y’,z’)
6. Verkleinerungsrelation ist wohlfundierte Ordnung auf D
Entwurf zuverlassiger Software 237 Divide & Conquer Algorithmen
Divide & Conquer Algorithmen: Korrektheitsbeweis
FUNCTION F(x:D):R WHERE I(x) RETURNS y SUCH THAT O(x,y)
= if primitive(x) then Directly-solve(x)
else (Compose G×F Decompose)(x)
• Partielle Korrektheit: strukturelle Induktion uber (D,)
– Primitive Eingaben:
– F(x) = Directly-solve(x) — Korrektheit folgt aus Axiom 1
– Nichtprimitive Eingaben:
– F(x) = (Compose G×F Decompose)(x)
– Decompose(x) liefert y’,y mit OD(x,y’,y) und xy Axiom 3
– G(y’) liefert z’ mit O’(y’,z’) Axiom 5
– F(y) liefert z mit O(y,z) Induktionsannahme
– Compose(z,z’) liefert t mit OC(z,z’,t) Axiom 4
– Fur t gilt O(x,t) und es ist t=F(x) Axiom 2
• Terminierung: Wohlfundiertheit von Axiom 6
Entwurf zuverlassiger Software 238 Divide & Conquer Algorithmen
Divide & Conquer Algorithmen: Synthesestrategie
Zerlege Problem in Spezifikationen fur Teilprobleme
Gegeben: FUNCTION F(x:D):R WHERE I(x) RETURNS y SUCH THAT O(x,y)
1. Wahle und Decompose aus Wissensbank 7→ OD,D’, Axiom 6
2. Konstruiere Hilfsfunktion G: 7→ O’,I’,R’, Axiom 5
– Heuristik: G:=F, falls D’=D, sonst G=Id
3. Verifiziere Decompose, generiere Vorbedingung: 7→ primitive, Axiom 3
– Heuristik: abgeleitete zusatzliche Vorbedingung fur OD ist ¬primitive(x)
4. Konstruiere Compose 7→ OC , Axiom 4,2
– Heuristik: Erzeuge OC mit Axiom 2; synthetisiere Compose gemaß Axiom 4
5. Konstruiere Directly-solve 7→ Axiom 1
– Heuristik: Suche nach vorgefertigten Losungen, sonst neue Synthese– Falls dies nicht moglich ist, konstruiere eingeschrankte Vorbedingung I
6. Instantiiere Divide & Conquer Schema
Alternativen:– Wahle Compose, konstruiere sukzessive G, , Decompose und Directly-solve
– Wahle Decompose und , konstruiere sukzessive Compose, G und Directly-solve
Entwurf zuverlassiger Software 239 Divide & Conquer Algorithmen
Divide & Conquer Strategie: Hilfsmittel
• Standard-Zerlegungen von D 7→ Decompose, OD, D’
– FirstRest, ListSplit auf Folgen (Seq(α))· ListSplit ≡ λL. ( [ L[i]|i ∈[1..|L|÷2] ], [ L[i]|i ∈[1+|L|÷2..|L|] ] )
mit OD ≡ λL,(L1,L2). L=L1L2, D’=Seq(α)
– ArbRest auf endlichen Mengen (Set(α))– Komponentenweise Dekomposition auf Produkten (und Mengen, Folgen, . . . )– Vorganger auf naturlichen Zahlen (N)
• Standard-Wohlordnungen auf D 7→
– Langen/Großenordnung auf Folgen und Mengen: λL,L’. |L|>|L’|
– Lexikographische Ordnung auf Produkten (und Mengen, Folgen, . . . )· λ(a1,b1),(a2,b2). a1>a2 ∨ (a1=a2 ∧ b1>b2)
– Zahlenordnung auf N, Absolutordnung auf Z
• Standard-Kompositionen auf R 7→ Compose, OC, R’
– cons, append auf Folgen– insert, union auf endlichen Mengen– Komponentenweise Komposition auf Produkten (und Mengen, Folgen, . . . )– Nachfolger auf naturlichen Zahlen
Entwurf zuverlassiger Software 240 Divide & Conquer Algorithmen
Divide & Conquer Strategie: Mechanismen
• Fixierung der Wahl von G– Falls D’=D, wahle G=F, R’=R, O’=O und I’=I
– Falls D’6=D, wahle G=Id, R’=D’, O’= λy’,z’.z’=y’ und I’= λy’.true
· Entscheidung analog, falls R’=R durch Wahl von Compose
• Inferenzmechanismus: Abgeleitete Vorbedingungen– Bestimme Voraussetzungen fur Gultigkeit einer Formel
= Verbleibende Vorbedingungen beim Versuch des Beweises
– Zielgerichteter Einsatz von Lemmata entsprechend vorkommender Begriffe
• Inferenzmechanismus: Fallanalyse– Erzeugung von Alternativen uber existierende Pradikate
– Auswertung der Einzelfalle
7→ Programmstucke mit Fallunterscheidungen
• Inferenzmechanismus: Operator match– Erzeugung von Programmstucken durch Anpassung an bekannte Losungen
Entwurf zuverlassiger Software 241 Divide & Conquer Algorithmen
Divide & Conquer Strategie: Sortieralgorithmus
FUNCTION sort(L:Seq(Z)):Seq(Z) RETURNS S SUCH THAT rearranges(L,S) ∧ ordered(S)
1. LL’ :≡ |L|>|L’| Decompose :≡ ListSplit
2. G :≡ sort
3. FUNCTION Fd(L:Seq(Z)):Seq(Z)×Seq(Z) WHERE ¬primitive(L)
RETURNS L1,L
2SUCH THAT LL
1∧ LL
2∧ L
1L
2=L
= ListSplit(L)
hat als Vorbedingung fur Korrektheit primitive(L) :≡ L=[]
4. LL1
∧ LL2
∧ L1L
2=L ∧ SORT(L
1,S
1) ∧SORT(L
2,S
2) ∧OC(S1
,S2,S) ⇒ SORT(L,S)
liefert als Spezifikation und Losung fur Compose
FUNCTION Fc(S1,S
2:Seq(Z)×Seq(Z)):Seq(Z) WHERE ordered(S
1) ∧ordered(S
2)
RETURNS S SUCH THAT ordered(S) ∧ rearranges(S,S1S
2)
= merge(S1,S
2) 7→ nachste Folie
5. Direkte Losung fur primitive Eingaben:
FUNCTION Fp(L:Seq(Z)):Seq(Z) WHERE L=[] RETURNS S SUCH THAT SORT(L,S) = []
6. Instantiierter Divide & Conquer Algorithmus
FUNCTION sort(L:Seq(Z)):Seq(Z) RETURNS S SUCH THAT rearranges(L,S) ∧ ordered(S)
= if L=[] then []
else let L1= [ L[i] | i ∈[1..|L|÷2] and L
2= [ L[i] | i ∈[1+|L|÷2..|L|]
in merge(sort(L1),sort(L
2))
Entwurf zuverlassiger Software 242 Divide & Conquer Algorithmen
Divide & Conquer Strategie: merge-Funktion
FUNCTION merge(S1,S
2:Seq(Z)×Seq(Z)):Seq(Z) WHERE ordered(S
1) ∧ordered(S
2)
RETURNS S SUCH THAT ordered(S) ∧ rearranges(S,S1S
2)
1. Wahle Listenerzeugungsfunktion cons als Compose-Operator
Spezifikation OC(a,S’,S) = S=a.S’, Domain D’ = Z
2. G kann nicht merge sein. Wahle G=Id, O’(a’,a) = a=a’.
3. Konstruiere auf Seq(Z)×Seq(Z):– (S1,S2)(S1,S2) = |S1|>|S1’| ∨ (|S1|=|S1’| ∧ |S2|>|S2’|)
– Langenordnung fur Listen + lexikographische Ordnung fur Produkte
4. Konstruiere Decompose mit Axiom 2 und 3OD(S1
,S2,a’,S
1’,S
2) ∧ a=a’ ∧ MERGE(S
1’,S
2’,S’) ∧ S=a.S’ ⇒ MERGE(S
1,S
2,S)
liefert als Spezifikation und Losung fur DecomposeFUNCTION fd(S1
,S2:Seq(Z)×Seq(Z)):Z×Seq(Z)×Seq(Z)
WHERE ordered(S1) ∧ ordered(S
2) ∧ |S
1|>0 ∧ |S
2|>0
RETURNS a’,S1’,S
2’ SUCH THAT rearranges(a.(S
1’S
2’), S
1S
2)
∧ ∀x ∈S1’S
2’. a≤x ∧ (S
1,S
2)(S
1’,S
2’)
= let x1.L
1=S
1and x
2.L
2=S
2in if x
1≤x
2then (x
1,L
1,S
2) else (x
2,S
1,L
2)
(Fallanalyse: a’ muß Minimum von first(S1) und first(S
2) sein)
Entwurf zuverlassiger Software 243 Divide & Conquer Algorithmen
Divide & Conquer Strategie: merge-Funktion
5. Vorbedingung fur Korrektheit von Decompose ist S16=[] ∧ S26=[]
– Liefert Spezifikation fur Directly-Solve
Direkte Losung fur primitive Eingaben:FUNCTION merge(S
1,S
2:Seq(Z)×Seq(Z)):Seq(Z)
WHERE ordered(S1) ∧ ordered(S
2) ∧ (S
1=[] ∨ S
2=[])
RETURNS S SUCH THAT ordered(S) ∧ rearranges(S, S1S
2)
= if S1=[] then S
2else S
1
6. Instantiierter Divide & Conquer AlgorithmusFUNCTION merge(S
1,S
2:Seq(Z)×Seq(Z)):Seq(Z)
WHERE ordered(S1) ∧ ordered(S
2)
RETURNS S SUCH THAT ordered(S) ∧ rearranges(S, S1S
2)
= if S1=[] then S
2
elseif S2=[] then S
1
else let x1.L
1=S
1and x
2.L
2=S
2
in if x1≤x
2then x
1.merge(L
1,S
2) else x
2.merge(S
1,L
2)
Entwurf zuverlassiger Software
Lektion 15
Problemreduktionsgeneratoren und Lokalsuchalgorithmen
1. Problemreduktionsgeneratoren
– Struktur und Axiome
– Syntheseverfahren
2. Lokalsuchalgorithmen
– Struktur und Korrektheitsbedingungen
– Syntheseverfahren
Entwurf zuverlassiger Software 244 Problemreduktionsgeneratoren
Problemreduktionsgeneratoren: Grundidee
• ∨ - ∧ -Reduktion auf mehrere Teilprobleme– Problem besitzt mehrere Losungen– Gesamtlosung ist Summe unabhangiger Einzellosungen ( ∨ -Reduktion)– Einzellosungen aus akzeptablen Teillosungen zusammengesetzt ( ∧ -Reduktion)– Verallgemeinerung von Dynamischem Programmieren, Spielbaumsuche, . . .
• Kombination von Globalsuche und Divide & Conquer– Unabhangige Divide & Conquer Algorithmen fur jede Einzellosung
· Dekompositionen und Kompositionen verschieden· Teilprobleme konnen einander uberlappen· Basisfall primitiver Eingaben ist primitives Divide & Conquer
– Losung durch Vereinigung aller Einzellosung berechnen
• Formale GrundstrukturFUNCTION F(x:D):Set(R) WHERE I(x) RETURNS z | O(x,z)
=⋃
(Composei (Fi1×..×Fik) Decomposei) (x) | i,k ∈N
– Decomposei: D → Di1×..×Dik – Composei: Ri1×..×Rik → R
– Fij lost (Dij,Rij,Iij,Oij)
– Strong Problem Reduction Principle muß gelten– Rekursive Aufrufe mussen wohlfundierter Ordnung genugen
Entwurf zuverlassiger Software 245 Problemreduktionsgeneratoren
Problemreduktionsgeneratoren: Komponenten und Axiome
FUNCTION F(x:D):Set(R) WHERE I(x) RETURNS z | O(x,z)
=⋃
(Composei (Fi1×..×Fik) Decomposei) (x) | i,k ∈ N
– Menge von Spezifikationen (Dj,Rj,Ij,Oj) mit Hauptspezifikation (D,R,I,O)
– Menge von Dekompositionsstrukturen ODi: D×Di1×..×Dik → B
· i1, ..ik: Menge von Indizes, abhangig von i
– Menge von Kompositionsstrukturen OCi: Ri1×..×Rik×R → B
– Wohlfundierte Ordnung auf D
1. Fur alle i: Decomposei erfullt ODiund ‘verkleinert’ Problem:
– FUNCTION Fdi(x:D):Set(Di1×..×Dik) WHERE I(x)
RETURNS y | ODi(x,y) ∧ xy ∧ Ii1(y) ∧ .. Iik(y)
· Notation: xy, falls xyij fur Dij=D (x ∈D, y ∈Di1×..×Dik)
2. Fur alle i: Composei erfullt OCi
– FUNCTION Fci(w:Ri1×..×Rik):Set(R) RETURNS z | OCi
(w,z)
3. Fur alle j: Funktion Fj erfullt (Dj,Rj,Ij,Oj):– FUNCTION Fj(yj:Dj):Set(Rj) WHERE Ij(yj) RETURNS wj|Oj(yj)
4. O rekursiv zerlegbar in ODi, Oi1×..×Oik, OCi
– O(x,z) ⇔ ∃i:N.∃y:Di1×..Dik.∃w:Ri1×..Rik. ODi(x,y) ∧ Oi1,..ik(y,w) ∧ OCi
(w,z)
· Oi1,..ik(y1,..yk, w1
,..wk) = Oi1(y1,w
1) ∧ .. ∧ Oi1(yk,wk)
Entwurf zuverlassiger Software 246 Problemreduktionsgeneratoren
Synthese von Problemreduktionsgeneratoren
• Aufspaltung des Reduktionsprizips in 2 Axiome
Starke Korrektheit bzgl. Komposition bzw. Dekomposition
∀i:N.∀x:D.∀y:Di1×..Dik.∀w:Ri1×..Rik.∀z:R. I(x) ∧ Ii1,..ik(y)
⇒ Oi1,..ik(y,w) ∧ OCi(w,z) ⇒ (ODi
(x,y) ⇔ O(x,z))
∀i:N.∀x:D.∀y:Di1×..Dik.∀w:Ri1×..Rik.∀z:R. I(x) ∧ Ii1,..ik(y)
⇒ Oi1,..ik(y,w) ∧ ODi(x,y) ⇒ (OCi
(w,z) ⇔ O(x,z))
Vollstandigkeit bzgl. Komposition
∀i:N.∀x:D.∀w:Ri1×..Rik.∀z:R. I(x)
⇒ O(x,z) ∧ OCi(w,z) ⇒ ∃y:Di1×..Dik. Ii1,..ik(y) ∧ Oi1,..ik(y,w)
• Strategie analog zu Divide & Conquer Verfahren– Wahle Composei aus Wissensbank– Konstruiere Hilfsfunktionen Fij (Id oder rekursiver Aufruf)– Konstruiere Dekompositionsoperaten mit Korrektheitsaxiom 1– Wahle aus der Wissensbank und verifiziere Decomposei
– Verifiziere Vollstandigkeitsaxiom– Instantiiere Algorithmus
Entwurf zuverlassiger Software 247 Lokalsuch-Algorithmen
Lokalsuch-Algorithmen: Grundidee
Losung von Optimierungsproblemen
• Optimierung = Minimierung von Kosten– Spezifikation des Problems besitzt mehrere leicht bestimmbare Losungen– Losungen konnen bewertet werden (Nutzen, Kosten, Dauer, . . . )– Gesucht: Losung mit optimaler Bewertung – o.B.d.A. minimale Kostenz.B. Travelling Salesman, (großte) Clique, Rucksackproblem, Scheduling– Optimierungsalgorithmus NP-vollstandig, suboptimale Losungen polynomial
• Losungsverfahren: Hillclimbing– Beginne mit irgendeiner Losung des Problems– Durchsuche Nachbarschaft der Losung nach besseren Losungen– Wiederhole Suche, bis keine bessere Losung in Nachbarschaft zu findenz.B. lineares Programmieren, Simplex-Algorithmus
• Nachbarschaftstruktur entscheidet Qualitat– Verfahren bestimmt lokale Optima– kleine Nachbarschaften ⇒ Verfahren endet nicht in globalem Optimum– grobe Nachbarschaften ⇒ Suche + Test auf lokales Optimum ineffizient⇒ Hauptproblem ist Bestimmung einer guten Nachbarschaftstruktur
Entwurf zuverlassiger Software 248 Lokalsuch-Algorithmen
Lokalsuch-Algorithmen: Struktur und Komponenten
FUNCTION Fopt(x:D):R WHERE I(x) RETURNS y
SUCH THAT O(x,y) ∧ ∀t:R. O(x,t) ⇒ cost(x,y)≤cost(x,t)
= FLS(x,F(x))
FUNCTION FLS(x:D,z:R):R WHERE I(x) ∧ O(x,y) RETURNS y
SUCH THAT O(x,y) ∧ ∀t ∈N(x,y). O(x,t) ⇒ cost(x,y)≤cost(x,t)
= if ∀t ∈N(x,z). O(x,t) ⇒ cost(x,z)≤cost(x,t)
then z
else FLS(x, arb(t | t ∈N(x,z) ∧ O(x,t)
∧ cost(x,z)>cost(x,t)) )
• Spezifikation D,R,I,O mit Initiallosung F(x)
• Kostenfunktion cost auf Raum R mit Ordnung ≤– Zusatzspezifikation des Optimierungsproblems
• Nachbarschaftsstruktur N:D×R→Set(R)– Suchraumbeschreibung fur lokale Variationen
Entwurf zuverlassiger Software 249 Lokalsuch-Algorithmen
Lokalsuch-Algorithmen: Korrektheit
FUNCTION Fopt(x:D):R WHERE I(x) RETURNS y
SUCH THAT O(x,y) ∧ ∀t:R. O(x,t) ⇒ cost(x,y)≤cost(x,t)
= FLS(x,F(x))
FUNCTION FLS(x:D,z:R):R WHERE I(x) ∧ O(x,y) RETURNS y
SUCH THAT O(x,y) ∧ ∀t ∈N(x,y). O(x,t) ⇒ cost(x,y)≤cost(x,t)
= if ∀t ∈N(x,z). O(x,t) ⇒ cost(x,z)≤cost(x,t)
then z else FLS(x, arb(t | t ∈N(x,z) ∧ O(x,t) ∧ cost(x,z)>cost(x,t)))
ist korrekt, wenn 4 Axiome erfullt sind
1. F(x) berechnet gultige Initiallosung fur O– FUNCTION f(x:D):R WHERE I(x) RETURNS y SUCH THAT O(x,y)
2. Reflexivitat der Nachbarschaftsstruktur– ∀x:D.∀y:R. I(x) ∧O(x,y) ⇒ y ∈N(x,y)
3. Exaktheit lokaler Optima ( 7→ Optimale Algorithmen)
– ∀x:D.∀y:R. I(x) ∧ O(x,y) ⇒ ∀t ∈N(x,y). O(x,t) ⇒ cost(x,y)≤cost(x,t)
⇒ ∀t:R. O(x,t) ⇒ cost(x,y)≤cost(x,t)
4. Erreichbarkeit gultiger Losungen (Fur suboptimale Algorithmen)
– ∀x:D.∀y,t:R. I(x) ∧ O(x,y) ∧ O(x,t) ⇒ ∃k:N.t ∈NkO(x,y)
– NkO(x,y) ≡ if k=0 then y else
⋃
Nk−1(x,t) | t ∈N(x,y) ∧ O(x,t)
Entwurf zuverlassiger Software 250 Lokalsuch-Algorithmen
Lokalsuchalgorithmen fur Sortierprobleme
• Sortierung als Ordnungsoptimierung– FUNCTION sort(L:Seq(Z)):Seq(Z)
RETURNS S SUCH THAT rearranges(L,S)
– Kostenfunktion: Anzahl der Fehlstellungen ‘S[i]>S[i+1]’
• Bubbelsort Algorithmus– Initiallosung S = L
– Modifikation durch Vertauschung benachbarter Komponenten von S
· Nachbarschaft: Listen die durch Tausch zweier Komponenten entstehen
· Restriktion auf benachbarte Komponenten
– Alle Nachbarn liefern mogliche Losungen (Feasibility Constraint)
– Nur Vertauschungen mit i<j ⇒ S[i]>S[j] bringen Verbesserungen
· S ist optimal, falls ∀i,j. i<j ⇒ S[i]≤S[j]
• Lokalsuche = Nachbarschaft + Suchfilter– Nachbarschaft: Anderungsaktion (Vertauschung) + Parameter (Indizes von S)
– Suchfilter: Feasibility Constraint, Optimality Constraint
Entwurf zuverlassiger Software 251 Lokalsuch-Algorithmen
Synthese von Lokalsuch-Algorithmen: Hilfsmittel
• Nachbarschaftsstruktur als Perturbation (Verwirbelung)– Inkrementelle Veranderung von Werten aus R
· Numerik: δ-Vektoren, Kombinatorik: Austausch von Komponenten– Nachbarschaft dargestellt als N(x,y) = Action(i,j,x,y)| i,j ∈π(x)
· Anderungsaktion Action(i,j,x,y) modifiziert Losungspunkt (x,y) ∈D×R
· Parameter i,j ∈π(x,y): minimale Bestandteile von Ein- oder Ausgabe
• Lokalsuchtheorie: allgemeine Suchstruktur fur R– L = (D,R,I,O,π, Action) erfullt Axiome 2–4– Vorgefertigte Nachbarschaftsstrukturen fur Grunddatentypen in Wissensbank
• Spezialisierungsmechanismen– Synthetisiere Losung F fur Spezifikation spec = (D,R,I,O)
– Wahle L passend zum Ausgabebereich R
– Zeige L generalisiert spec 7−→ Substitution θ:D→DL
– Modifiziere L zu Lokalsuchtheorie fur Spezifikation– Beschranke N im Hinblick auf optimale Losungen von spec
• Ggf. Verzicht auf Exaktheit– liefert effizienteren, aber suboptimalen Algorithmus
Entwurf zuverlassiger Software 252 Lokalsuch-Algorithmen
Standard-Lokalsuchtheorien
• LS seq re(α): Umordnung von Folgen– Suche = Permutation einzelner Elemente einer Folge– Anderungsparameter: Indizes der Eingabeliste L– Perturbation: Vertauschung zweier Elemente einer Ausgabeliste SLS seq re(α) ≡ D 7→ Seq(α)
R 7→ Seq(α)
I 7→ λL. true
O 7→ λL, S. rearranges(L,S)
π 7→ λL,S. (domain(S),domain(S))
Action 7→ λi,j,L,S. [ S(i↔j)(k) | k ∈domain(S)](i↔j)(k) = if k=i then j else if k=j then i else k
• LS subsets(α): Teilmengen fester Große– Suche = Austausch einzelner Elemente einer Menge– Anderungsparameter: Elemente der Ein- und Ausgabemenge– Perturbation: Austausch zweier Elemente in AusgabemengeLS subsets(α) ≡ D 7→ Set(α)×N
R 7→ Set(α)
I 7→ λS,m. m≤|S|
O 7→ λS,m, S’. S’⊆S ∧ |S’|=m
π 7→ λS,m,S’. (S\S’, S’)
Action 7→ λi,j,S,m,S’. S’ = (S∪i)-y
Entwurf zuverlassiger Software 253 Lokalsuch-Algorithmen
Lokalsuch-Algorithmen: Synthesestrategie
Gegeben: Spezifikation fur Optimierungsproblem
FUNCTION Fopt(x:D):R WHERE I(x) RETURNS y
SUCH THAT O(x,y) ∧ ∀t:R. O(x,t) ⇒ cost(x,y)≤cost(x,t)
1. Wahle Lokalsuchtheorie L mit Ausgabetyp R (Wissensbank)
2. Beweise ‘L generalisiert (D,R,I,O)’– Extrahiere Substitution θ und setze Lθ = (D,R,I,O,πθ,Actionθ)
3. Generiere Losungs-Filter FC fur Lθ (Feasibility Constraint)– Nicht akzeptable Losungen fur (D,R,I,O) konnen abgeschnitten werden
∀i,j,x,y. I(x) ∧O(x,y) ∧O(x,Action(i,j,θ(x),y)) ⇒ FC(i,j,x,y))– Entspricht notwendigen Filtern der Globalsuche
4. Generiere Optimalitats-Filter OC fur Lθ (Optimality Constraint)– Kostenungunstigere Punkte konnen eliminiert werden
∀i,j,x,y. I(x) ∧O(x,y) ∧O(x, Action(i,j,θ(x),y))
⇒ cost(x,y)≤cost(x,Action(i,j,θ(x),y)) ⇒ OC(i,j,x,y)
– ∀i,j ∈π(x,y). OC(i,j,x,y) notwendig fur lokale Optima
5. Synthetisiere Initiallosung f fur Spezifikation
FUNCTION F(x:D):R WHERE I(x) RETURNS y SUCH THAT O(x,y)
Entwurf zuverlassiger Software 254 Lokalsuch-Algorithmen
6. Generiere suboptimale Lokalsuch AlgorithmenFUNCTION Fopt(x:D):R WHERE I(x) RETURNS y
SUCH THAT O(x,y) ∧ ∀t ∈N(x,y). O(x,t) ⇒ cost(x,y)≤cost(x,t)= FLS(x,f(x))
FUNCTION F(x:D):R WHERE I(x) RETURNS y SUCH THAT O(x,y)= f(x)
FUNCTION FLS(x:D,z:R):R WHERE I(x) ∧ O(x,y) RETURNS ySUCH THAT O(x,y) ∧ ∀t ∈N(x,y). O(x,t) ⇒ cost(x,y)≤cost(x,t)
= if ∀i,j ∈π(θ(x),z). FC(i,j,x,z) ∧ O(x, Action(i,j,θ(x),y)⇒ OC(i,j,x,z) ∧ cost(x,z)≤cost(x, Action(i,j,θ(x),y)
then zelse FLS(x, arb( Action(i,j,θ(x),y)| i,j ∈π(θ(x),z)
∧ FC(i,j,x,z) ∧ O(x, Action(i,j,θ(x),y))∧ ¬OC(i,j,x,z) ∨ cost(x,z) > cost(x,Action(i,j,θ(x),y))) )
– Losungs und Optimalitatstests notwendig fur Korrektheit– Uberprufung nur fur Parameter, welche die Filter FC, OC passieren
· andthen/orelse Semantik von ∧ und ∨ in Programmen
7. Generiere Bedingungen fur Exaktheit (Global Optimality Constraint)∀x,y. [∀i,j.I(x) ∧O(x,y) ∧O(x, Action(i,j,θ(x),y))
⇒ cost(x,y)≤cost(x,Action(i,j,θ(x),y))]⇒ [∀t:R. O(x,t) ⇒ cost(x,y)≤cost(x,t)] ⇒ GOC(x,y)
– Optionaler Schritt – Erganzung des obigen Schemas
Entwurf zuverlassiger Software 255 Lokalsuch-Algorithmen
Lokalsuche: Anwendungsbeispiele
• Minimal Spanning Tree– Gegeben: Graph mit gewichteten Kanten (Zugriffszeiten, Abstande,. . . )– Gesucht: Baum, auf dem alle Knoten mit minimalen Kosten erreichbar– Initialwert: Erzeuge spannenden Baum– Perturbation: Erganze neue Kante, entferne eine andere Kante– Feasibility Constraint: Entfernte Kante muß redundant sein– Optimality Constraint: Hinzugefugte Kante ist teurer als bisheriger Weg
• Lineare Programmierung– Minimiere lineare Funktion f(x1,..xn)=Σcixi
unter linearen Restriktionen Aj[x1,..xn], j ∈1..m, m<n
– Standard Darstellung: Minimiere c ? x unter A ? x=b ∧ ∀i≤n.xi≥0
– Initiallosung: Setze xm+1,..xn := 0,Lose A1..m ? x1..m mit ∀i≤m.xi>0 durch Gauß-Verfahren
– Perturbation: Setze ein xi:=0, wahle neues xj 6=0
– Feasibility Constraint: Alte + neue x-Komponenten nach Losung positiv– Optimality Constraint: Relative Kosten steigen durch Veranderung
Entwurf zuverlassiger Software
Lektion 16
Korrektheitserhaltende Optimierung
1. Logische Vereinfachungen
– Mit und ohne Berucksichtigung von Kontext
2. Partielle Auswertung
3. Endliche Differenzierung
4. Fallanalyse
5. Datentyp-Verfeinerung
Entwurf zuverlassiger Software 256 Optimierungstechniken
Simplifikationen
Logische Vereinfachung von Teilausdrucken
Anwendung gerichteter Gleichungen– Term-Rewriting mit Lemmata der Wissensbank
– Auswahl anwendbarer Lemmata gemaß Haupt- und Nebenoperatoren
• CI-Simplifikation: (kontextunabhangig)– Nur der aktuelle Teilausdruck wird betrachtet
– Anwendung von Gleichungen ohne Vorbedingungen
– Ausfuhrung, solange anwendbare Gleichungen vorhanden
• CD-Simplifikation: (kontextabhangig)– Anwendung bedingter Gleichungen
– Kontext durch Syntaxbaum (Programmcode und Vorbedingung) bestimmt
– Hauptanwendung: Elimination redundanter Teilausdrucke
Benutzerinteraktion– Auswahl des zu vereinfachenden Teilausdrucks
– Art der vorgesehenen Vereinfachung (CI/CD)
– Begrenzung der Vor- und Ruckwartsinferenzen (optional)
Entwurf zuverlassiger Software 257 Optimierungstechniken
Costas-Arrays Optimierung: erster Algorithmus
FUNCTION Costas (n:Z):Set( Seq(Z) ) WHERE n≥1
RETURNS p | perm(p,1..n) ∧ ∀j ∈domain(p).nodups(dtrow(p,j))
= if nodups([]) ∧ ∀j ∈domain([]).nodups(dtrow([],j))
then Costasaux(n,[]) else ∅
FUNCTION Costasaux (n:Z,V:Seq(Z)):Set( Seq(Z) )
WHERE n≥1 ∧ range(V)⊆1..n ∧ nodups(V) ∧ ∀j ∈domain(V).nodups(dtrow(V,j))
RETURNS p | perm(p,1..n) ∧ Vvp ∧ ∀j ∈domain(p).nodups(dtrow(p,j))
= p | p ∈V ∧ perm(p,1..n) ∧ ∀j ∈domain(p).nodups(dtrow(p,j))
∪⋃
Costasaux(n,W) | W ∈V·i|i ∈1..n ∧ nodups(W)
∧ ∀j ∈domain(W).nodups(dtrow(W,j))
Entwurf zuverlassiger Software 258 Optimierungstechniken
Costas-Arrays Optimierung: CI-Simplifikationen
FUNCTION Costas (n:Z):Set( Seq(Z) ) WHERE n≥1
RETURNS p | perm(p,1..n) ∧ ∀j ∈domain(p).nodups(dtrow(p,j))
= Costasaux(n,[])
FUNCTION Costasaux (n:Z,V:Seq(Z)):Set( Seq(Z) )
WHERE n≥1 ∧ range(V)⊆1..n ∧ nodups(V) ∧ ∀j ∈domain(V).nodups(dtrow(V,j))
RETURNS p | perm(p,1..n) ∧ Vvp ∧ ∀j ∈domain(p).nodups(dtrow(p,j))
= (if perm(V,1..n) ∧ ∀j ∈domain(V).nodups(dtrow(V,j)) then V else ∅)
∪⋃
Costasaux(n,V·i) |i ∈1..n ∧ nodups(V·i)
∧ ∀j ∈domain(V·i).nodups(dtrow(V·i,j))
Entwurf zuverlassiger Software 259 Optimierungstechniken
Costas-Arrays Optimierung: CD-Simplifikationen
FUNCTION Costas (n:Z):Set( Seq(Z) ) WHERE n≥1
RETURNS p | perm(p,1..n) ∧ ∀j ∈domain(p).nodups(dtrow(p,j))
= Costasaux(n,[])
FUNCTION Costasaux (n:Z,V:Seq(Z)):Set( Seq(Z) )
WHERE n≥1 ∧ range(V)⊆1..n ∧ nodups(V) ∧ ∀j ∈domain(V).nodups(dtrow(V,j))
RETURNS p | perm(p,1..n) ∧ Vvp ∧ ∀j ∈domain(p).nodups(dtrow(p,j))
= (if 1..n⊆range(V) then V else ∅)
∪⋃
Costasaux(n,V·i) | i ∈1..n ∧ i 6∈V
∧ ∀j ∈domain(V). (V[|V|+1-j]-i) 6∈dtrow(V,j)
Entwurf zuverlassiger Software 260 Optimierungstechniken
Partielle Auswertung
Auswertung von Funktionen mit konstantem Argument
• Symbolische Auswertung zur Entwurfszeit
– Formal: Auffalten von Definitionen + Simplifikation
– Anwendbar, solange ein konstanter Teilausdruck vorhanden
Beispiel:
|[4;5] V| unfold concatenation
= |4. ([5] V)| unfold concatenation
= |4. (5. ([] V))| unfold concatenation
= |4. (5. V)| unfold length
= 1 + |5. V| unfold length
= 1 + 1 + |V| simplify
= 2 + |V|
• Benutzerinteraktion:
– Auswahl des auszuwertenden Teilausdruck und Optimierungstechnik
Entwurf zuverlassiger Software 261 Optimierungstechniken
Endliche Differenzierung
Inkrementelle Berechnung wiederkehrender Teilausdrucke
• Effizienter als standige Neuberechnung– Ersetze Teilausdruck in rekursivem Aufruf durch Variable
– Bestimme differentielle Veranderungen bei jedem Neuaufruf
– Formal: Abstraktion uber Teilausdruck E(x)
+ Simplifikation mit zusatzlicher Gleichung ‘E(x) = new’
• Abstraktion uber E(x) in f(x):– Bestimme neues f’, so daß f(x) = f’(x,E(x))
– Ersetze alle Aufrufe der Art f( g(x) ) durch f’( g(x), E(g(x)) )
• Simplifikation mit zusatzlicher Gleichung ‘E(x) = new’– Simplifiziere Ausdrucke der Form E(g(x)) in die Form g’(E(x))
– Ersetze alle Vorkommen von E(x) durch new
• Benutzerinteraktion:– Auswahl des zu ersetzenden Teilausdrucks E(x)
Entwurf zuverlassiger Software 262 Optimierungstechniken
Costas-Arrays Optimierung: Endliche Differenzierung
FUNCTION Costas (n:Z):Set( Seq(Z) ) WHERE n≥1
RETURNS p | perm(p,1..n) ∧ ∀j ∈domain(p).nodups(dtrow(p,j))
= Costasaux1(n,[],1..n)
FUNCTION Costasaux1 (n:Z,V:Seq(Z),Pool:Set(Z)):Set( Seq(Z) )
WHERE n≥1 ∧ range(V)⊆1..n ∧ nodups(V) ∧ ∀j ∈domain(V).nodups(dtrow(V,j))
∧ Pool = 1..n\range(V)
RETURNS p | perm(p,1..n) ∧ Vvp ∧ ∀j ∈domain(p).nodups(dtrow(p,j))
= (if empty?(Pool) then V else ∅)
∪⋃
Costasaux1(n,V·i,Pool−i) |i ∈Pool
∧ ∀j ∈domain(V). (V[ |V|+1 -j]-i) 6∈dtrow(V,j)
Entwurf zuverlassiger Software 263 Optimierungstechniken
Fallanalyse
• Separate Betrachtung von Einzelfallen
– Auswertung von Tests aus anderen Programmteilen
– Zweck: globale Vereinfachung durch lokale Einzelanalyse
– Formal: Erzeugung eines Kontexts + CD-Simplifikation
• Kontexterzeugung mit Pradikat P
– Ersetze Ausdruck E(x) durch if P(x) then E(x) else E(x)
– Vereinfache E(x) in beiden Kontexten
– Distributiere if P(x) uber Ausdrucke außerhalb von E(x)
• Benutzerinteraktion:
– Auswahl des zu ersetzenden Teilausdrucks E(x)
– Auswahl des Pradikats P
– Nachfolgende außere Simplifikationen
Entwurf zuverlassiger Software 264 Optimierungstechniken
Costas-Arrays Optimierung: Fallanalyse
FUNCTION Costas (n:Z):Set( Seq(Z) ) WHERE n≥1
RETURNS p | perm(p,1..n) ∧ ∀j ∈domain(p).nodups(dtrow(p,j))
= Costasaux2(n,[],1..n,1)
FUNCTION Costasaux2 (n:Z,V:Seq(Z), Pool:Set(Z),Vsize:Z):Set( Seq(Z) )
WHERE n≥1 ∧ range(V)⊆1..n ∧ nodups(V) ∧ ∀j ∈domain(V).nodups(dtrow(V,j))
∧ Pool = 1..n\range(V) ∧ Vsize = |V|+1
RETURNS p | perm(p,1..n) ∧ Vvp ∧ ∀j ∈domain(p).nodups(dtrow(p,j))
= if empty?(Pool)
then V
else⋃
Costasaux2(n,V·i,Pool−i,Vsize+1) |i ∈Pool
∧ ∀j ∈domain(V). (V[Vsize-j]-i) 6∈dtrow(V,j)
Entwurf zuverlassiger Software 265 Optimierungstechniken
Datentypverfeinerung
Konkrete Implementierungen fur abstrakte Konstrukte
• Realisiere abstrakte Definitionen von Datentypen– Bereitstellung einer Auswahl von Implementierungen fur jeden Typ
· effizient fur bestimmte Verwendungszwecke– Bereitstellung von Konversionsfunktionen
• Endliche Mengen– Listen: Standardimplementierung– Bitvektor: Mengen uber endlichem Domain– charakteristische Funktion (effiziente Elementrelation)
• Folgen– verkettete Liste: Standardimplementierung– umgekehrte Liste (gut fur append-Operation ·)
• Benutzerinteraktion– Auswahl einer Variablen fur Nichtstandard-Implementierungen– Auswahl einer vordefinierten Implementierung
• Weitere Optimierungsmoglichkeiten– Compilierung in konkrete Zielsprache (LISP, C++, ADA, . . . )– Sprachabhangige Optimierungen
Entwurf zuverlassiger Software
Lektion 17
Zusammenfassung und Ausblick
1. Zusammenfassung
– Unterstutzung beim Entwurf zuverlassiger Software
2. Ausblick: Aktuelle Entwicklungen
3. Forschungsthemen und Vertiefungsmoglichkeiten
Entwurf zuverlassiger Software 266 Zusammenfassung und Ausblick
Entwurf zuverlassiger Software: Zusammenfassung
• Objektmodellierung: Entwurf von Systemspezifikationen
– OMT als Methodik fur Entwurf von Klassen
· Operationen, Beziehungen, Attribute, Vor-/Nachbedingungen, Invarianten
– Methodische Unterstutzung, wenig Automatisierung
⇒ Kreativitat erforderlich
– Guter Bezug zur Anschauung (Diagramme)
– Resultierende Einzelspezifikationen sind klein
• Synthese: Entwurf von Einzelagorithmen
– Strategien zur Erzeugung effizienter Algorithmen aus Spezifikationen
– Hoher Abstraktionsgrad durch formale Logik
– Wenig anschaulich, aber gut automatisierbar und nachweisbar korrekt
⇒ Schnelle Realisierung des Systementwurfs
⇒ Benutzer kann sich auf Entwurfsarbeit konzentrieren
Entwurf zuverlassiger Software 267 Zusammenfassung und Ausblick
Programmsynthese: Ausblick
• Notwendig fur die Praxis der Programmierung
• Marktreife noch nicht erreicht
• Zukunftstrachtiges Forschungsgebiet
• Bedingungen an konkrete Systeme
– interne Verarbeitung formal korrekt
– externe Prasentation moglichst wenig formal
– graphische Unterstutzung fur Kontrolle einer Synthese
– große Wissensbanken mit effizienter Verwaltung
• Voraussetzungen fur die Entwicklung von Systemen
– Theoretische Grundlagen und praktische Programmierarbeiten
– Formale Denkweise, Kenntnis logischer Kalkule, Abstraktionsvermogen
– Kreativitat, Experimentierfreudigkeit, Ausdauer, Frustrationstoleranz
Entwurf zuverlassiger Software 268 Zusammenfassung und Ausblick
Aktuelle Forschungsthemen
• Aufbau und Strukturierung der Wissensbank– Formalisierung und Computerrealisierung verschiedener Anwendungsbereiche– Anwendung von Lemmata als Rewrite-Regeln (Teilterm-matching 2. Stufe)
– Effizienter Zugriff auf anwendbare Lemmata (Strukturierungsmethoden)
• Integration von Beweisverfahren– Aussagenlogik – Entscheidungsprozeduren (Davis-Putnam Verfahren?)
– Pradikatenlogik – Konnektionsmethode (7→ S.Schmitt / J.Otten / D.Korn)
– Induktionstechniken (Rippling,...)
– Anwendungsspezifische Verfahren
• Integration von Syntheseverfahren– Computerrealisierung von Algorithmetheorien als Theoreme– Spezialisierte Entwurfstaktiken mit Theoremeinbindung– Optimierungstechniken
• Benutzerinterface & Dokumentation
7→ Studien- & Diplomarbeiten
top related