Entwurf zuverl assiger Software - Universität Potsdam · Lehrziele und geplanter Aufbau der...

Entwurf zuverlassiger Software

Sommersemester 1996

Christoph KreitzFG Intellektik, TH Darmstadt, Telephon (06151) 16-2863

[email protected]

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


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


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.


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:


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.


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 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


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


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


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 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


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)


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


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.)


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


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


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ß


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


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


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


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


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()


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


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


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


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


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


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


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


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


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;


nationalitat: STRING;

vater, mutter: PERSON

end -- class PERSON

• Zyklische Objektstrukturen sind erlaubt


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


Definition von Routinen

class PERSON feature

name, vornamen, nationalitat: STRING;


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


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


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


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


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;


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


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


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;


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


Generische Klassendefinition

class LIST[X]

creation new

feature

empty: BOOLEAN is -- Ist die Liste leer ?

do...end;


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]]


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)


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


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)


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


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


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


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.


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]


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


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]


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


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


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


Vererbung als Diagramm

'

&

$

%PERSON

'

&

$

%

*

ENTLEIHER

'

&

$

%

HHHHHHHHHHY

ARBEITNEHMER

ENTLEIHER und ARBEITNEHMER erben von PERSON


Polymorphismus

Fahigkeit, verschiedene Formen anzunehmen

benutzerliste-

QQ

QQ

QQ

QQ

QQ

QQ

QQ

QQ

QQk

AA

AA

AA

AA

AA

AAK

3

Professorenobjekt Studentenobjekt Mitarbeiterobjekt Professorenobjekt

Keine Konvertierung notig


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.


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.


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


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


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.


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;


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!


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.


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


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;


do Result := Festgehalt nach monatsstunden end

end -- class HILFSKRAFT


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.


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.


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.


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


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]


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


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


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


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


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


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


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


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


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


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


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)


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)


Leistungen von ENTLEIHER


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))


Leistungen der Erben von ENTLEIHER


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


Leistungen von BUCH DB


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


Leistungen von BUCH


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...


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


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


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


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


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


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

drucken

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


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

'

&

$


Paris

'

&

$

%(Land)

Deutschland

'

&

$


Berlin

'

&

$

%


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


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


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


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


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


Generalisierungshierarchie in OMT

OMT Bild 3.24 Seite 41 150%


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


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


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


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


Aggregation vs. Generalisierung

OMT Bild 4.2 Seite 59 200%

Aggregation: ‘UND’ Beziehung zwischen verschiedenen Instanzen

Generalisierung: ‘ODER’ Beziehung zwischen Klassen (gleiche Instanzen)


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


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


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


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?)


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


Zustandsdiagramm

Bild 5.10, S.94 120%


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


Datenflußdiagramm

Bild 6.9, S.134 120%

+ Vorgriff auf Folie OMT Methodik aus Lektion 7


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


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


Leitbeispiel: Verwaltung von Geldautomaten

Fig 8.3, S151 – 140%


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 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


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


ATM Netzwerk: mogliche und sinnvolle Objektklassen

Fig 8.5/6 200% – LIVE farbig umrahmen, Farben unten vorbereiten

— Irrelevant — Redundant — Undeutlich

— Implementierungsnah – Attribute


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


ATM Netzwerk: mogliche Beziehungen

Fig 8.9 160%, dann markiere was gestrichen/verandert wird


ATM Netzwerk: Erstentwurf eines Objektmodells

Fig 8.11 160%,


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?


ATM Netzwerk: Objektmodell mit Attributen

Fig 8.12 140%,


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


ATM Netzwerk: Objektmodell mit Generalisierung

Fig 8.13 125%,


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?)


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


ATM Netzwerk: Objektmodell nach Revision

Fig 8.14 140%, Farbig gestalten fur Module


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


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


ATM Netzwerk: Event-Trace

Fig 8.18 100%,


ATM Netzwerk: Ereignisflußdiagramm

Fig 8.19 160%,


ATM Netzwerk: Zustandsdiagramm der Klasse ATM

Fig 8.20 110%,


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


ATM Netzwerk: Datenflußdiagram und

Prozeßverfeinerung

Fig 8.24/25 125%,


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


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


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


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


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


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


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


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


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


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)


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))


Costas-Arrays (3): lauffahiger Algorithmus


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))


COSTAS-ARRAYS (4a): CI-Simplifikationen



= Costasaux(n,[])




= (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))


Costas-Arrays (4b): CD-Simplifikationen



= Costasaux(n,[])




= (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)


Costas-Arrays (4c): Finite Differencing



= Costasaux1(n,[],1..n)

FUNCTION Costasaux1 (n:Z,V:Seq(Z),Pool:Set(Z))


∧ Pool = 1..n\range(V)


= (if empty?(Pool) then V else ∅)

∪⋃

Costasaux1(n,V·i,Pool−i) |i ∈Pool



Costas-Arrays (4d): Case Analysis



= Costasaux2(n,[],1..n,1)

FUNCTION Costasaux2 (n:Z,V:Seq(Z), Pool:Set(Z),Vsize:Z)


∧ Pool = 1..n\range(V) ∧ Vsize = |V|+1


= 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)


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


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


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


Syntheseparadigmen: Synthese durch Transformation



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


Syntheseparadigmen: Algorithmenschemata

Erzeuge Algorithmus in einem Schritt



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


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


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 –


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



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


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


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)


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


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


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?


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


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!)


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)


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


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


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


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


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


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)


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))


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)


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)


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


3: M = maxseq(x.l)

| ` max(L+a1,a

1) = maxbeg(a

1.(x.l))

| by lemma M3\... v


3: M = maxseq(x.l)

` max(M, max(L+a1,a

1)) = maxseq(a

1.(x.l))

by ... lemma M3 ... lemma M4


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.


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


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



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


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.


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


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’)


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|=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).


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)))


Programmerzeugung: Maximale Segmentsumme

Resultat der Transformationen

∀L:Seq(Z).∀m:Z. L 6=[] ⇒

maxseg(L,m) ⇔ ∃l:Z. 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


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)


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


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


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


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



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


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



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).


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


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


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)


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


GET-SOC — Separate Output Conditions


– 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


CHVAR — Choose Output-Variable


– ∀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


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)


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


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.


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


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)


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



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


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


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

@@

@@

@@

@@

@@

@


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


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)


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!)


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”


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)



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


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


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)))


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)


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


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


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]


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


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


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


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)


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 ∅)


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


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


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| !


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θ!


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)


Globalsuchalgorithmen: Costas Arrays Synthese

FUNCTION Costas (n:Z):Set( Seq(Z) ) WHERE n≥1


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


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) )


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))


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


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)


Divide & Conquer Algorithmen: Allgemeine Struktur

Problemreduktion durch Eingabe-Dekomposition

FUNCTION F(x:D):R WHERE I(x) RETURNS y SUCH THAT O(x,y)


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)


Divide & Conquer Algorithmen: Korrektheit





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


Divide & Conquer Algorithmen: Korrektheitsbeweis



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


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


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


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


Divide & Conquer Strategie: Sortieralgorithmus


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


= 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))


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)


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)


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)


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)


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


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)


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


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


Lokalsuch-Algorithmen: Korrektheit



= 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)))


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)


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


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


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


Lokalsuch-Algorithmen: Synthesestrategie

Gegeben: Spezifikation fur Optimierungsproblem



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



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


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


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)


Costas-Arrays Optimierung: erster Algorithmus



= if nodups([]) ∧ ∀j ∈domain([]).nodups(dtrow([],j))

then Costasaux(n,[]) else ∅

FUNCTION Costasaux (n:Z,V:Seq(Z)):Set( Seq(Z) )


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))


Costas-Arrays Optimierung: CI-Simplifikationen



= Costasaux(n,[])




= (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))


Costas-Arrays Optimierung: CD-Simplifikationen



= Costasaux(n,[])




= (if 1..n⊆range(V) then V else ∅)

∪⋃

Costasaux(n,V·i) | i ∈1..n ∧ i 6∈V



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


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)


Costas-Arrays Optimierung: Endliche Differenzierung



= Costasaux1(n,[],1..n)

FUNCTION Costasaux1 (n:Z,V:Seq(Z),Pool:Set(Z)):Set( Seq(Z) )


∧ Pool = 1..n\range(V)


= (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)


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


Costas-Arrays Optimierung: Fallanalyse



= Costasaux2(n,[],1..n,1)

FUNCTION Costasaux2 (n:Z,V:Seq(Z), Pool:Set(Z),Vsize:Z):Set( Seq(Z) )


∧ Pool = 1..n\range(V) ∧ Vsize = |V|+1


= 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)


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


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


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


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

Entwurf zuverl assiger Software - Universität Potsdam · Lehrziele und geplanter Aufbau der...

Documents

Transcript of Entwurf zuverl assiger Software - Universität Potsdam · Lehrziele und geplanter Aufbau der...