Semantics and program verification

MaRDI QIDQ2761214zbMATH OpenFDO

Authors Christoph Walther

Publication date 18 December 2001

Published in Teubner-Texte zur Informatik (Search for Journal in Brave)

zbMATH Keywords

functional languagessemantics verification

Mathematics Subject Classification ID

Introductory exposition (textbooks, tutorial papers, etc.) pertaining to computer science (68-01) Functional programming and lambda calculus (68N18) Semantics in the theory of computing (68Q55)

Review text

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.

Recommendations

• scientific article; zbMATH DE number 546874
• Theory of program structures: schemes, semantics, verification. 2nd printing
• Programmverifikation
• scientific article; zbMATH DE number 50008
• scientific article; zbMATH DE number 548908

Cited in

(5)

• Mechanized semantics
• scientific article; zbMATH DE number 3866548 (Why is no real title available?)
• scientific article; zbMATH DE number 3980456 (Why is no real title available?)
• scientific article; zbMATH DE number 546874 (Why is no real title available?)
• Program semantics and verification technique for AI-centred programs

This page was built for publication: Semantics and program verification

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2761214)