Semantics and program verification (Q2761214)

Dieses Buch behandelt Grundkonzepte der Programmiersprachensemantik anhand einer einfachen funktionalen Programmiersprache. Darauf aufbauend werden die Aufgaben und Probleme bei Nachweis von totaler und partieller Korrektheit einfacher funktionaler Programme behandelt. Insbesondere wird der Bezug zwischen Programmiersprachensemantik und formaler Logik illustriert. Prinzipielle Grenzen der ``automatischen'' Verifikation werden untersucht und die praktische Relevanz dieser Grenzen wird diskutiert.NEWLINENEWLINENEWLINEDas Buch ist in drei Kapitel aufgeteilt: Die formalen Grundlagen behandeln Syntax und Semantik der Prädikatenlogik, fundierte Mengen und konfluente Relationen. Die funktionale Programmiersprache FP ist Gegenstand des zweiten Kapitels, ihre operationale und ihre denotationale Semantik werden erklärt und als äquivalent bewiesen. Das Kapitel wird ergänzt durch Datenstrukturen, alternative Parameterübergaben und die Elimination gegenseitiger Rekursion. Das dritte Kapitel widmet sich schließlich Terminierungsbeweisen sowie der Spezifikation und Beweisverfahren für partielle Korrektheit.NEWLINENEWLINENEWLINEGrundlage des Buches war eine gleichnamige Vorlesung, und umgekehrt ist es als Basis für eine Vorlesung verwendbar. Der Text ist sehr formal und kompakt geschrieben, enthält aber viele Beispiele und einige Übungsaufgaben.NEWLINENEWLINENEWLINEAndere Ansätze zur Programmiersprachensemantik und zur Programmverifikation werden nicht erwähnt; insbesondere werden ausschließlich funktionale Programmiersprachen betrachtet.