Semantik - Springer978-3-322-86823-7/1.pdfDie formale Semantik gehOrt zu den wichtigen Themen der...

14
Eike Best Semantik

Transcript of Semantik - Springer978-3-322-86823-7/1.pdfDie formale Semantik gehOrt zu den wichtigen Themen der...

Page 1: Semantik - Springer978-3-322-86823-7/1.pdfDie formale Semantik gehOrt zu den wichtigen Themen der Informatik. Ein wichtiges Thema der Informatik ist die formale Semantik. Anhand dieser

Eike Best

Semantik

Page 2: Semantik - Springer978-3-322-86823-7/1.pdfDie formale Semantik gehOrt zu den wichtigen Themen der Informatik. Ein wichtiges Thema der Informatik ist die formale Semantik. Anhand dieser

lehrbiicher Informotik

Aufbau unci Arbeitsweise von Rechenanlagen von Wolfgang Coy

Analysis Eine Einfuhrung fUr Mothemotiker und Informotiker von Gerold Schmieder

Numerik Eine Einfiihrung fUr Mothemoliker und Informaliker von Helmuth Spalh

Gnmdlogen des maKhinellen Beweisens von Dieter Hofbauer und Rolf-Dellef Kutsche

Fonnalisieren unci Beweisen Logik fUr Informoliker von Dirk Siefkes

Semon6k Theorie sequentieller und poralleler Programmierung von Eike Best

Verifikation und Validorion Software-Test fiir Studenten und Proktiker von Georg Erwin Thaller

Parullele Programmierung von Thomas Braunl Mehr ols nur Programmieren ... Eine EinfUhrung in die Informolik von Rainer Gmehlich und Heinrich Rusl

Algorithmen und Berechenbarkeit von Manfred Bretz

Konzeple und Praxis des Compilerbaus von Volker Penner

Modemes Software Engineering Eine EinfUhrung von Reiner Dumke

Interoktive Systeme Softwore-Entwicklung und Saftware-Erganomie von Christian Story

Management von Softwareprojekten Eine EinfUhrung von Fritz Peter Elzer

Vieweg

Page 3: Semantik - Springer978-3-322-86823-7/1.pdfDie formale Semantik gehOrt zu den wichtigen Themen der Informatik. Ein wichtiges Thema der Informatik ist die formale Semantik. Anhand dieser

Eike Best

Semantik

Theorie sequentieller und paralleler Programmierung

II v.eweg

Page 4: Semantik - Springer978-3-322-86823-7/1.pdfDie formale Semantik gehOrt zu den wichtigen Themen der Informatik. Ein wichtiges Thema der Informatik ist die formale Semantik. Anhand dieser

ISBN-I 3:978-3-322-86824-4 DOl : 10.1007/978-3-322-86823-7

Softcover reprint of the hardcover 1st edition 1995

e-ISBN- 13:978-3-322-86823-7

Das in diesem Buch enthaltene Pro gramm-Material ist mit keiner Verpflichtung oder Garantie irgendeiner Art verbunden. Der Autor und der Verlag iibernehmen infolgedessen keine Verantwor­tung und werden keine daraus folgende oder sonstige Haftung iibernehmen, die auf irgendeine Art aus der Benutzung dieses Programm-Materials oder Teilen davon entsteht.

Aile Rechte vorbehalten © Friedr. Vieweg & Sohn Verlagsgesellschaft mbH, BraunschweiglWiesbaden, 1995

Der Verlag Vieweg ist ein Unternehmen der Bertelsmann Fachinformation GmbH.

Das Werk einschlieBlich aller seiner Teile ist urheberrechtlich geschiitzt. Jede Verwertung auBerhalb der engen Grenzen des Urheberrechtsgesetzes ist ohne Zustimmung des Verlags unzuliissig und strafbar. Das gilt insbesondere flir Vervielfiiltigungen, Ubersetzungen, Mikroverfilmungen und die Einspei­cherung und Verarbeitung in elektronischen Systemen.

Druck und buchbinderische Verarbeitung: Hubert & Co., Gottingen Gedruckt auf siiurefreiem Papier

Page 5: Semantik - Springer978-3-322-86823-7/1.pdfDie formale Semantik gehOrt zu den wichtigen Themen der Informatik. Ein wichtiges Thema der Informatik ist die formale Semantik. Anhand dieser

Vorwort

Ich mochte mit zwei Behauptungen beginnen:

Die formale Semantik gehOrt zu den wichtigen Themen der Informatik. Ein wichtiges Thema der Informatik ist die formale Semantik.

Anhand dieser beiden Behauptungen mochte ich Ihnen, lieber Leser, den Gegenstand dieses Buches erkIaren: man sagt, daB die beiden Satze unterschiedliche Syntax, aber gleiche Semantik haben. Unter der Syntax eines Satzes versteht man seinen auBeren Aufbau, zum Beispiel als Folge Subjekt­Pradikat-Objekt. Vom rein satzbautechnischen Standpunkt aus besteht etwa zwischen den beiden Satzen:

Die formale Semantik ist ein Thema der Informatik. Das neue Buch begleitet eine Vorlesung des Studiengangs.

kein wesentlicher Unterschied. Der Inhalt, die Bedeutung oder eben die Semantik1 eines Satzes umfaBt die Bedeutung der Worter, aus denen er besteht. Sie ist jedoch mehr als nur deren Summe. In der Tat gehen zeitliche (z.B.: formal bedeutet heutzutage etwas anderes als vor 1000 Jahren), kontextuelle (z.B.: die Phrase Das neue Buch ist nur aus dem textuellen Zusammenhang heraus zu verstehen) und andere Aspekte, eventuell auch subjektive, in die Semantik eines Satzes ein. Die 'untersuchbare' Bedeutung ist daher stets eine Abstraktion vieler verschiedener Facetten ihrer Gesamtheit. Bei sehr genauer Untersuchung zeigen sich sogar zwischen den beiden Satzen zu Beginn dieser Uberlegungen unterschiedliche semantische Nuancen. Der erste legt starker als der zweite die Idee nahe, daB es eine wohldefinierte Menge von wichtigen Themen der Informatik gibt. Nur wenn Von diesem Unterschied abstrahiert wird, sind die Bedeutungen der beiden Satze gleich.

Die erwahnte Unterscheidung zwischen Syntax und Semantik tritt auch bei Programmiersprachen flir informationsverarbeitende Systeme - pragnanter als Computer bekannt - zutage. Zum Beispiel haben die beiden Programmstticke:

x := 0; (gelesen: Xneu wird zu 0)

x := x - x; (gelesen: Xneu wird zu Xalt minus Xalt)

die gleiche Semantik, aber unterschiedliche Syntax. Beide Zuweisungen bedeuten, daB der neue Wert der Variablen x gleich 0 sein solI, unabhangig von ihrem alten Wert. Mit einem ganz feinen Mikroskop konnen sogar zwischen dies en beiden Zuweisungen semantische Unterschiede entdeckt werden - namlich in der Art der Berechnung des Wertes 0, die bei beiden verschieden ist. Hier, wie auch schon oben, ist also die Abstraktionsebene wichtig, auf der man die semantischen Gegebenheiten betrachtet.

I Aus dem Brockhaus [62]: Semantik ist die Lehre von den Bedeutungen, von der Beziehung der Zeichen zum bezeichneten Gegenstand.

Page 6: Semantik - Springer978-3-322-86823-7/1.pdfDie formale Semantik gehOrt zu den wichtigen Themen der Informatik. Ein wichtiges Thema der Informatik ist die formale Semantik. Anhand dieser

vi Vorwort

1m Unterschied zu einer natiirlichen Sprache laBt sich bei einer Computersprache nicht nur die Syntax, sondern auch die Semantik streng mathematisch festlegen oder, wie man sagt,formalisie­ren, und zwar auf einem ganzen Spektrum von Abstraktionsstufen. Eine so1che Festlegung dient mehreren Zwecken:

• Eine unmittelbar einleuchtende Aufgabe ist es, sicherzustellen, daB das gleiche Compu­terprogramm nicht verschiedenen Interpretationen ausgesetzt werden kann, zum Beispiel durch zwei verschiedene Computer. In der 'Urzeit' der Computerprogrammierung konnte es durchaus vorkommen, daB ein und dasselbe Programm auf zwei verschiedenen Maschinen verschiedene Ergebnisse lieferte2 .

• Eine weitere - meiner Meinung nach die wichtigste - Aufgabe der formalen Semantik ist es, Korrektheitsbeweise von Programmen zu ermoglichen. Denn wenn die Semantik eines Programms prazise gegeben ist und wenn die Spezifikation des Programms als ein Objekt vergleichbarer Prazision vorliegt, dann kann die Korrektheit eines Programms in bezug auf seine Spezifikation in der Form eines mathematischen Satzes ausgesprochen werden. Die Richtigkeit eines so1chen Satzes kann entweder streng bewiesen werden, oder es kann seine Unrichtigkeit durch ein Gegenbeispiel gezeigt werden.

Ais ich vor vielen Jahren als studentische Hilfskraft an der Universitat Karlsruhe eine Stelle als Benutzerberater fiir die dort installierten Maschinen der Typen UNIVAC und Burroughs innehatte, lernte ich sehr schnell, daB die Benutzerfragen in zwei fast disjunkte Klassen zerfielen: syntaktische und semantische. Die Entdeckung syntaktischer Fehler ist bei guten Programmiersprachen wie dem damals benutzten Algol-GO [199], und in geringerem MaBe auch flir Fortran- und Cobol­

Programme iiberhaupt kein Problem. Die Entdeckung semantischer (oder, wie man auch oft sagt, logischer oder algorithmischer) Fehler ist flir den Benutzer zwar ungleich wichtiger, denn sein Programm beschreibt ja einen Algorithmus, der zu einem bestimmten Zweck eingesetzt werden solI; sie ist aber auch ungleich schwieriger, denn sie lauft auf die getrennte Beantwortung der beiden Fragen:

• Was soli das Programm leisten? • Was leistet das Programm?

hinaus und auf den Vergleich der beiden Antworten. GroBe und wichtige Teilgebiete der Informatik beschaftigen sich mit der Bereitstellung von Theorien und Methoden zur Beantwortung dieser Fragen: Spezifikation flir die erste Frage, Semantik flir die zweite Frage und Verifikation flir die Beantwortung der Frage, ob ein Programm oder ein System seine Spezifikation auch wirklich erfiillt. AIle drei Gebiete sind miteinander verbunden und erganzen sich gegenseitig.

Dieses Buch flihrt in das Gebiet der formalen Semantik ein und streift dabei auch die Gebiete der Spezifikation und der Verifikation, vor allem durch die Betrachtung von Beispielen und Fallstudien. Die Hauptkapitel3, 5,6,7 und 8 dieses Buches sind ungeHihrnach dem gleichen Muster aufgebaut:

wenig Syntax - viel Semantik - einige Beispiele.

Die Unterschiede (zum Beispiel in den Abstraktionsstufen) der Semantikdefinitionen werden immer durch qualifizierende Adjektiva unterschieden:

relationale Semantik - operation ale Semantik - axiomatische Semantik - etc.

Eine genauere Erklarung dieser Begriffe erfolgt spater.

2Den gleichen Effekt soli es auch heutzutage noch geben.

Page 7: Semantik - Springer978-3-322-86823-7/1.pdfDie formale Semantik gehOrt zu den wichtigen Themen der Informatik. Ein wichtiges Thema der Informatik ist die formale Semantik. Anhand dieser

Vorwort vii

Das Buch ist eine stark iiberarbeitete Version verschiedener Vorlesungsunterlagen. Als Skriptum liegt es den Vorlesungen Theorie der Programmierung I und II zugrunde, die seit dem Win­tersemester 1989190 regelmaBig an der Universitat Hildesheim gehalten werden. Die Vorlesung Theorie der Programmierung I umfaBt den Stoff der Kapitel 2, 3, 5 (soweit dieses Kapitel se­quentielle Programme betrifft) und 6. Die Vorlesung Theorie der Programmierung II umfaBt den Rest von Kapitel 5 sowie die Kapitel 7 und 8. Das Buch kann im fiinften und sechsten Semester zu Beginn des Hauptstudiums, aber auch im dritten und vierten Semester vor dem Vordiplom eingesetzt werden. Yom Leser werden Vorkenntnisse in nicht allzu groBem Umfang erwartet. Grundkenntnisse in diskreter Mathematik und in der Theorie formaler Sprachen sind zum Verstiindnis von groBem Vorteil. Programmierkenntnisse in einer imperativen Programmiersprache wie C [156] oder Pascal [260] sind hilfreich. Einige Lesehinweise fUr dieses Buch finden sich am Ende des Abschnitts 1.2 auf Seite 3.

Wahrend der Revision des Textes habe ich mich bemiiht, die Beweise verstiindlich darzustellen. In diesem Bemiihen bin ich oft, aber nicht immer, dem von Wim H. Feijen, Edsger W. Dijkstra und Carel S. Scholten - zum Beispiel in [107,237] - vorgeschlagenen Format gefolgt, namlich in einem Beweis die Deduktionen auf neuen Zeilen, abwechselnd mit den Begriindungen fUr ihre Giiltigkeit, aufzufUhren. Zum Beispiel ist:

Formelo ::::} ( Begriindung fiir die erste Implikation ) Formelt

::::} ( Begriindung fUr die zweite Implikation ) Formel2

::::} ( Begriindung fiir die n'te Implikation ) Formeln

das allgemeine Muster zur Darstellung einer Implikationskette der Liinge n. Genauso werden Aquivalenzketten oder (Un-)Gleichungsketten dargestellt. Das U mschreiben der Beweise war eine miihsame Arbeit, hat sich aber fUr mich personlich gelohnt. Generell habe ich beobachtet, daB sogenannte einfache Beweise, die friiher kurz aussahen,jetzt etwas liinger geworden sind, wahrend andere sogar kiirzer geworden sind.

Obwohl es auf Konferenzen und in Zeitschriften eine sehr rege Publikationstatigkeit gibt, ist die Anzahl der Lehrbiicher und Monographien auf dem Gebiet der Mathematik speziell paral­le1er Programme noch recht iiberschaubar (unter anderen sind [8, 18, 116] zu erwahnen). Dieses Buch unterscheidet sich von seinen verdienstvollen Vorgangem vielleicht in erster Linie dadurch, daB ich auf fast jeder Betrachtungsebene versucht habe, der vor allem aus der Petrinetztheorie stammenden Idee, die Daten (Zustande) und die Algorithmen (Aktionen) wohl zu unterscheiden und trotzdem gleichwertig zu behandeln, Ausdruck zu geben, selbst wenn die reine Petrinetztheorie in diesem Buch keine Hauptrolle spielt. Petris Auffassung von Aktionen als Zustandsanderungen und umgekehrt von Zustiinden als Ruhepunkten zwischen Aktionen [212] und die daraus folgende analoge Behandlung der beiden Konzepte habe ich stets als anschaulich und sinnvoll empfunden. Ich habe in diesem Buch an vielen Stellen versucht, diese Idee sinngemaB zu verwirklichen und auf realitatsgetreue Probleme anzuwenden. Ein anderer Gedanke aus der Petrinetztheorie findet in diesem Buch ebenfalls eine Anwendung: die Darstellung der Abliiufe eines parallelen Programms als Menge von Halbordnungen.

Page 8: Semantik - Springer978-3-322-86823-7/1.pdfDie formale Semantik gehOrt zu den wichtigen Themen der Informatik. Ein wichtiges Thema der Informatik ist die formale Semantik. Anhand dieser

viii Vorwort

Ich bin vielen Personen flir ihre Mithilfe am Zustandekommen dieses Buches zu Dank verpfiichtet. Claudia Toussaint hat flir einige der Ubungsaufgaben die Musterlosungen angefertigt. Javier Esparza hat einmal die Vorlesung iibernommen und nicht nur zur Erganzung, sondern auch zur besseren Organisation des Textes beigetragen. Hans-Giinther Linde-Goers, Holger Schirnick und Bernd Grahlmann haben Ubungsaufgaben und Musterlosungen beigesteuert. Karin Apitz hat die Ubungsaufgaben zu den Vorlesungen gesammelt und geordnet. Barbara Sprick hat einige Zeich­nungen angefertigt. Wolfgang Thomas hat mir freundlicherweise sehr detaillierte und hilfreiche Kommentare zu einer friiheren Version des Textes zur Verfugung gestellt. Manfred Broy hat wertvolle Hinweise zur GIattung des Materials gegeben. Fiir weitere ausfiihrliche Kommentare und erfolgreiche Fehlersuche bedanke ich mich vor allen bei JOrg Desel, der das Skriptum als Grundlage flir eine Vorlesung an der Humboldt-Universitat zu Berlin verwendet hat, und bei Javier Esparza, der oft freundlich genug war, kurzfristig als Korrekturleser zu he1fen, des weiteren bei Joachim Biskup, Hans-Herrmann Briiggemann, Peter Deussen, Hans Fleischhack, Alexander Lawrow, Agathe Merceron, Arend Rensink, Peter H. Starke, Glinther Stiege und Walter Vogler. Verschiedenen Generationen Hildesheimer und einem Jahrgang Berliner Studenten, besonders Stephan Melzer, Matthias Moeller, Sabine Klempt, Burkhard Bieber, Steffen Moller, Claus Reck und Andreas Benneke, bin ich fiir Kommentare und Fehlersuche dankbar. Ganz besonderen Dank schulde ich Thomas Thielke und Burkhard Graves flir eine grlindliche SchluBlektiire der Kapitel 1 bis 6. Carsten Bierans hat bei der Rechtschreibpriifung geholfen. Es ist vielleicht notig, zu erwlihnen, daB ich flir Fehler, falls solche trotz all dieser Hilfe noch im Text verborgen sind, ganz al1ein verantwortlich bin.

Dem Verlag Vieweg - in der Person von Reinald Klockenbusch - danke ich flir die Geduld mit meinen manchmal etwas optimistischen zeitlichen Vorstellungen und flir die generelle Unterstlitzung bei der Produktion des Textes. Meiner Familie: Andreas, Benjamin, Simon, Robert, David und Monika, danke ich flir die groBe Geduld und das mir entgegengebrachte Verstandnis. Meinem Vater Herbert Best und meinen Sohnen David und Robert danke ich flir hilfreiche und informative Gesprache iiber syntaktische Feinheiten und Fallen der deutschen Schriftsprache [110].

Wo im Text die Leserin und der Leser angesprochen werden, verwende ich immer die mannliche Form; die deutsche Sprache verhindert es leider, eine kurze libergreifende Form zu bilden. So mogen Leserinnen sich denn immer mitgemeint flihlen, wenn im folgenden (und vorher) vom Leser die Rede ist.

Eike Best Hildesheim,Oktober 1994

Dieses Buch wurde mit dem Programm Textures™ 1.6.2 der Firma Blue Sky Research gesetzt, einer Implementierung von Donald Knuths TEX [162] fur den Apple Macintosh. Benutzt wurden auch Leslie Lamports u\TPC [168], das Makropaket AMS-TEX der American Mathematical Society [7], PICTEX von Michael J. Wichura sowie einige Makropakete von DANTE, der deutschen TEX-Benutzergruppe [82]. Mehrere Programme impublic und shareware domain waren hilfreich, besonders LaGrafix von Brad Richards, Excalibur 1.5 von Robert Gottshall und Rick Zaccone, SearchFiles 1.3 von Robert Morris sowie LaterLaser 1.0b von Keith Stattenfield. Allen Genannten sei an dieser Stelle gedankt.

Page 9: Semantik - Springer978-3-322-86823-7/1.pdfDie formale Semantik gehOrt zu den wichtigen Themen der Informatik. Ein wichtiges Thema der Informatik ist die formale Semantik. Anhand dieser

Inhaltsverzeichnis

1 Einleitung...

1.1 Ubersicht.

1.2 Inhalt ...

1.3 Historisches zur Semantik sequentieller Programme .

1.4 Historisches zur Semantik paralle1er Programme .

1.5 Literaturangaben.................

2 Mathematische Grundlagen

2.1 Logik, Gleichheit und Mengen .

2.1.1 Logische Operatoren ..

2.1.2 Gleichheits- und Aquivalenzbegriffe .

2.1.3 Mengen . . . . . . . . . . . . .

1

1

3

5

10

12

13

14

14

14

15

2.2 Relationen, Funktionen und Operationen . 16

2.2.1 Relationen.......... 16

2.2.2 Funktionen und Operationen . 18

2.3 Halbordnungen............ 19

2.3.1 Grundbegriffe........ 20

2.3.2 Eigenschaften von Halbordnungen zur ProzeBbeschreibung 21

2.3.3 Bine Eigenschaft von Halbordnungen zur Terminierung 25

2.4 Verbande.............. 25

2.4.1 Grundlegende Definitionen

2.4.2 Verbandsoperationen und -funktionen

2.4.3 Uber die Existenz von Fixpunkten ..

2.4.4 Iterative Berechnung von Fixpunkten

26

27

29

30

Page 10: Semantik - Springer978-3-322-86823-7/1.pdfDie formale Semantik gehOrt zu den wichtigen Themen der Informatik. Ein wichtiges Thema der Informatik ist die formale Semantik. Anhand dieser

x Inhaltsverzeichnis

2.5 Boolesche Algebren, Teilmengen und Pradikate 31

2.6 Variablen, Zustande und Ausdriicke . . . . . 33

2.6.1 Variablendeklarationen und Zustande 33

2.6.2 Arithmetische und Boolesche Ausdriicke; Syntaxdefinitionen 35

2.6.3 Substitutionssatze..........

2.6.4 Felddeklarationen und Feldausdriicke

2.7 Graphen

2.8 Folgen

2.8.1 Grundlegende Definitionen

2.8.2 Prafixstruktur

2.9 Literaturangaben.

2.10 Ubungsaufgaben .

40

41

43

44

44

45

47

48

3 Semantik sequentieller Programme . . . . . . . .

3.1 Sequentielle nichtdeterministische Programme.

3.1.1 Syntax und Erlauterungen ...

51

52

52

54

54

56

3.2 Operationale und relationale Semantik .

3.2.1 Motivation und Grundbegriffe .

3.2.2 Induktive Definition der relationalen Semantik

3.2.3 Unendlich nichtdeterministische Programme 59

3.2.4 Angelischer, damonischer und erratischer Nichtdeterminismus 60

3.3 Beweisregeln.....

3.3 .1 Hoare-Tripel .

3.3.2 Hoare-Beweisregeln

3.3.3 Erlauterung der Regeln anhand von Beispielen

3.3.4 Schleifenregel und Invarianten (Beispiel)

3.3.5 Konsistenz und Vollstandigkeit .....

3.3 .6 Die Relativitat der Vollstandigkeitsaussage

3.3.7 Aquivalenz von relationaler und axiomatischer Semantik

3.4 Die w p-Semantik ......... .

3.4.1 Die semantische Funktion Wp

3.4.2 Das wp-Kalki.il ...... .

3.4.3 Aquivalenz zwischen wp-Kalki.il und wp-Funktion

62

62

62

64

66

68

72

73

74

75

76

80

Page 11: Semantik - Springer978-3-322-86823-7/1.pdfDie formale Semantik gehOrt zu den wichtigen Themen der Informatik. Ein wichtiges Thema der Informatik ist die formale Semantik. Anhand dieser

Inhaltsverzeichnis

3.4.4

3.4.5

3.4.6

3.4.7

Aquivalenz Von relationaler und wp-Semantik .

SpeziaWille: stetige und additive wp-Funktionen

Liveness und Safety, Invarianz und Terminierung

w p-Semantik endlich nichtdeterministischer Programme

3.5 Bemerkungen zum Entwurf VOn Programmen

3.5.1 Spezifikationen und Invarianten .

3.5.2 Loschen eines logischen Faktors .

3.5.3 Ersetzen einer Konstanten durch eine Variable .

3.5.4 VergroBern des Wertebereichs einer Variablen

3.5.5 Addieren eines logischen Summanden .

3.6 Literaturangaben

3.7 Ubungsaufgaben

4 Von sequentiellen zu parallelen Systemen . . . . . . .

4.1 Zur operationalen Semantik paralleler Programme.

4.1.1 Ein disjunkt-paralleles Modell . . . . . . .

4.1.2 Sequentielle, parallele und kausale Semantik

4.1.3 Ereignishalbordnungen und Halbworter ...

4.1.4 Korrektheit und Effizienz paralleler Programme

4.2 Atomare Aktionen und KontrollftuB . . . . . . . . . .

4.2.1 Fairness-Betrachtungen bei sequentiellen Programmen

4.2.2 Die UND-Regel . . . . . . . . . . ..

4.2.3 Eine Bemerkung zur Kompositionalitat

4.2.4 Deadlock-Betrachtungen.

4.3 KontrollftuB und DatenftuB .

4.4 Literaturangaben

4.5 Ubungsaufgaben

5 Kontrollprogramme und Petrinetze

5.1 Kontrollprogramme und ihr Verhalten

5.1.1 Sequentielle Kontrollprogramme

5.1.2 Parallele und Top-Level-Kontrollprogramme

5.1.3 Parallele Semantik von Kontrollprogrammen

Xl

85

89

93

99

100

100

104

104

106

106

108

109

113

113

113

116

120

122

124

125

126

128

129

130

133

134

135

135

136

142

145

Page 12: Semantik - Springer978-3-322-86823-7/1.pdfDie formale Semantik gehOrt zu den wichtigen Themen der Informatik. Ein wichtiges Thema der Informatik ist die formale Semantik. Anhand dieser

xii Inhaltsverzeichnis

5.2 Petrinetze und ihr Verhalten . . . .

5.2.1 Grundlegende Definitionen

5.2.2 S-Systeme und SND-Systeme

5.2.3 Invarianten in Petrinetzen . .

5.2.4 Kausale Semantik von Petrinetzen .

5.3 Netzsemantik von Top-Level-Kontrollprogrammen

5.3.1 Ubersetzung von Kontrollprogrammen in SND-Systeme

5.3.2

5.3.3

Semantikvergleich von Kontrollprogrammen und Petrinetzen

Wohlgeformtheit und Regularitat ..... .

5.4 Zur Benutzung von Kontrollprogrammen und Netzen

5.5 Literaturangaben

5.6 Ubungsaufgaben

6 Operationale Semantik und Fairness

6.1 Sequentielle Programme mit atomaren Aktionen .

6.2 Operationale Semantik ......... .

6.2.1 Beschreibung des Kontrollflusses

6.2.2 Beschreibung des Datenflusses .

6.2.3 Ausfiihrungsfolgen ...

6.2.4 Konsistenzbetrachtung.

6.3 Eine Hierarchie von Fairnessbegriffen

6.3.1 Vier Beispiele ...

6.3.2 Fairnessdefinitionen

6.3.3 Fairness und unbeschrankter Nichtdeterminismus

6.4 Literaturangaben

6.5 Ubungsaufgaben

7 Programme mit globalem Speicher

7.1 Syntax und Motivation .

7.2 Operationale Semantik .

7.3 Erganzende Bemerkungen

7.3.1 Relationale Semantik

7.3.2 Invarianten und stabile Pradikate .

146

147

150

152

155

159

159

162

166

168

171

172

175

175

177

177

179

180

182

185

185

187

188

193

193

195

196

199

202

202

204

Page 13: Semantik - Springer978-3-322-86823-7/1.pdfDie formale Semantik gehOrt zu den wichtigen Themen der Informatik. Ein wichtiges Thema der Informatik ist die formale Semantik. Anhand dieser

Inhaltsverzeichnis X1Il

7.3.3 Schachtelung von atomaren Aktionen und Paralleloperator 204

7.3.4 Kausale Semantik . . . 205

7.3.5 Fairness und Fortschritt 207

7.3.6 Lokale und globale Variablen, Leser- / Schreiber-Problem. 210

7.3.7 Implementierung atomarer Aktionen .

7.4 Algorithmen zum wechselseitigen AusschluB

7.4.1 Herleitung von Petersons Algorithmus .

7.4.2 Ein operationaler Beweis von Petersons Algorithmus

7.5 Das Owicki / Griessche Beweissystem .

213

215

215

218

220

7.5.1 Beispiele und Motivation ... 220

7.5.2 Sequentiell gliltige Annotationen 223

7.5.3 Parallel gliltige Annotationen 224

7.5.4 Der Konsistenzsatz. . . . . . 226

7.5.5 Ein Owicki / Gries-Beweis von Petersons Algorithmus 227

7.5.6 Systematische Einflihrung von Hilfsvariablen 229

7.5.7 Der Vollstandigkeitssatz . . . . . . . . . . . 234

7.5.8 Schachtelung des Paralleloperators, Terminierungsbeweise 237

7.6 Beispiele und Fallstudien

7.6.1 Ein Puffer-Programm

7.6.2

7.6.3

7.6.4

7.6.5

7.6.6

Ein paralleler Algorithmus zur Berechnung klirzester Wege

Ein Algorithmus zur Berechnung eines Eulerkreises .

Ein Petrinetzbeweis von Petersons Algorithmus . .

Ein partiell korrektes Fixpunkteinigungsprogramm

Ein paralleler Listenbereinigungsalgorithmus

7.7 Literaturangaben

7.8 illmngsaufgaben

8 Kommuuizierende Programme

8.1 Syntax und Beispiele ..

8.2 Operationale Semantik .

8.2.1 Namen atomarer Aktionen .

8.2.2 Kontrollprogramm und Ausflihrungen

8.3 Erganzende Bemerkungen . . . . . . . . . .

237

238

239

242

249

253

258

265

266

271

272

275

276

277

281

Page 14: Semantik - Springer978-3-322-86823-7/1.pdfDie formale Semantik gehOrt zu den wichtigen Themen der Informatik. Ein wichtiges Thema der Informatik ist die formale Semantik. Anhand dieser

xiv Inhaltsverzeichnis

8.3.1 Relationale Semantik und Konsistenz 281

8.3.2 Kausale Semantik .......... 282

8.3.3 Erweiterte Kommunikationsaktionen 282

8.3.4 Andere Erweiterungen . 285

8.4 Ein Mengenpartitionsprogramm 286

8.5 Ein Beweissystem ....... 290

8.5.1 Lokale, Kommunikations- und Terminierungsaktionen 290

8.5.2 Sequentiell giiltige Annotationen 291

8.5.3 Parallel gtiltige Annotationen .. 292

8.5.4 Eine Anwendung des Beweissystems 293

8.5.5 Der Konsistenzsatz. . . 295

8.5.6 Der Vollstlindigkeitssatz 297

8.5.7 Bemerkungen zu den Vollstlindigkeitsslitzen . 299

8.6 Beispiele und Fallstudien ...... 300

8.6.1 Ein Koordinationsprogramm . 301

8.6.2 Berechnung des groBten gemeinsamen Teilers . 303

8.6.3 Ein verteilter Terminierungsalgorithmus . 306

8.7 Literaturangaben 310

8.8 Ubungsaufgaben 311

A Beweise und Losungen ............... 313

A.1 Beweise der Slitze von Kapitel 2 und Kapitel 4 . 313

A.2 Losungen ausgewlihlter Aufgaben 326

A.3 Literaturangaben ......... 344

Bibliographie . . . . . 345

Index der Definitionen 363