Formale Semantik
Die formale Semantik ist ein Teilgebiet der theoretischen Informatik, das sich mit dem Nachweis der Korrektheit von Computerprogrammen beschäftigt (Verifikation). Anders als die linguistische Semantik, die ein Teil der Sprachwissenschaft ist, arbeitet die formale Semantik mit vollständig mathematischen Methoden, um die Bedeutung von Computerprogrammen und Spezifikationen zu formalisieren. Sie ist eng verwandt mit der Berechenbarkeitstheorie, die sich damit beschäftigt, welche Probleme mit Computerprogrammen überhaupt gelöst werden können.
Die formale Semantik hat zum Ziel, die Bedeutung von Computerprogrammen in einer formalen Sprache auszudrücken — sie soll also die Semantik eines Computerprogramms syntaktisch ausdrücken, so dass sich über das Anwenden von Ableitungsregeln (Kalkülen) Aussagen über das Programm beweisen lassen.
In der formalen Semantik finden folgende Kalküle Verwendung:
- denotationale Semantik: Konstruktion der Semantik mittels mathematischer Räume aus der Bereichstheorie; die Semantik eines Programms ist eine Funktion.
- axiomatische Semantik: Beschreibung der Semantik durch ihre logischen Eigenschaften, wobei i.a. nur einige Eigenschaften betrachtet werden.
- operationale Semantik: durch eine Relation werden die möglichen Ausführungsschritte als Paare (Programm, Zustand) beschrieben.
Siehe auch
Literatur
- Joseph E. Stoy: Denotational Semantics: The Scott-Strachey Approach to Programming Language Semantics. MIT Press, Cambridge, Massachusetts, 1977.
- Jan van Leeuwen: Handbook of Theoretical Computer Science, Volume B. Elsevier / MIT Press, 1990.
Weblinks
- http://www.csse.monash.edu.au/~lloyd/tilde/Semantics/
- http://www.risc.uni-linz.ac.at/people/schreine/courses/densem/densem.html
- http://www.cl.cam.ac.uk/Teaching/Lectures/dens/