Semantik

Dieses Lehrbuch richtet sich an Studenten und ambitionierte Praktiker, die sich für die Theorie der Programmierung bzw. die Semantik von Programmiersprachen interessieren und dabei auch neuere Konzepte kennenlernen wollen.Der Datenfluß einer imperativen und nichtdeterministischen Programmiersprache und der Kontrollfluß einer variablenfreien Sprache werden zunächst getrennt beschrieben und dann zu einer einheitlichen Semantik für parallele Programme zusammengefügt. Besonderes Augenmerk liegt auf dem Studium der mathematischen Beziehungen zwischen verschiedenen semantischen Ansätzen. Das Buch ist vollständig mit leicht verständlichen Beweisen und praktische relevanten Beispielen versehen und enthält neben größeren Fallstudien auch Übungsaufgaben mit Musterlösungen sowie eine breite Literaturauswahl.

Autorentext

Prof. Dr. Eike Best lehrt Theoretische Informatik an der Universität Hildesheim. Er hat in Karlsruhe studiert, in Newcastle (England) promoviert und sich in Bonn für Informatik habilitiert. Seine Forschungsinteressen konzentrieren sich auf das Gebiet Semantik und Verifikation paralleler und verteilter Systeme.

Inhalt
1 Einleitung.- 1.1 Übersicht.- 1.2 Inhalt.- 1.3 Historisches zur Semantik sequentieller Programme.- 1.4 Historisches zur Semantik paralleler Programme.- 1.5 Literaturangaben.- 2 Mathematische Grundlagen.- 2.1 Logik, Gleichheit und Mengen.- 2.2 Relationen, Funktionen und Operationen.- 2.3 Halbordnungen.- 2.4 Verbände.- 2.5 Boolesche Algebren, Teilmengen und Prädikate.- 2.6 Variablen, Zustände und Ausdrücke.- 2.7 Graphen.- 2.8 Folgen.- 2.9 Literaturangaben.- 2.10 Übungsaufgaben.- 3 Semantik sequentieller Programme.- 3.1 Sequentielle nichtdeterministische Programme.- 3.2 Operationale und relationale Semantik.- 3.3 Beweisregeln.- 3.4 Die wp -Semantik.- 3.5 Bemerkungen zum Entwurf von Programmen.- 3.6 Literaturangaben.- 3.7 Übungsaufgaben.- 4 Von sequentiellen zu parallelen Systemen.- 4.1 Zur operationalen Semantik paralleler Programme.- 4.2 Atomare Aktionen und Kontrollfluß.- 4.3 Kontrollfluß und Datenfluß.- 4.4 Literaturangaben.- 4.5 Übungsaufgaben.- 5 Kontrollprogramme und Petrinetze.- 5.1 Kontrollprogramme und ihr Verhalten.- 5.2 Petrinetze und ihr Verhalten.- 5.3 Netzsemantik von Top-Level-Kontrollprogrammen.- 5.4 Zur Benutzung von Kontrollprogrammen und Netzen.- 5.5 Literaturangaben.- 5.6 Übungsaufgaben.- 6 Operationale Semantik und Fairness.- 6.1 Sequentielle Programme mit atomaren Aktionen.- 6.2 Operationale Semantik.- 6.3 Eine Hierarchie von Fairnessbegriffen.- 6.4 Literaturangaben.- 6.5 Übungsaufgaben.- 7 Programme mit globalem Speicher.- 7.1 Syntax und Motivation.- 7.2 Operationale Semantik.- 7.3 Ergänzende Bemerkungen.- 7.4 Algorithmen zum wechselseitigen Ausschluß.- 7.5 Das Owicki / Griessche Beweissystem.- 7.6 Beispiele und Fallstudien.- 7.7 Literaturangaben.- 7.8 Übungsaufgaben.- 8 Kommunizierende Programme.- 8.1 Syntax und Beispiele.- 8.2Operationale Semantik.- 8.3 Ergänzende Bemerkungen.- 8.4 Ein Mengenpartitionsprogramm.- 8.5 Ein Beweissystem.- 8.6 Beispiele und Fallstudien.- 8.7 Literaturangaben.- 8.8 Übungsaufgaben.- A Beweise und Lösungen.- Bibliographie.- Index der Definitionen.