Quelltext der Seite Axiomatische Semantik

Die '''axiomatische Semantik''' der [[Informatik]] beschreibt die [[Formale Semantik|Bedeutung]] von Programmen durch [[Schlussregel]]n, die es erlauben, von einer gewünschten Eigenschaft der Eingabe auf Eigenschaften der Ausgabe zu schließen. Dabei abstrahiert die axiomatische Semantik weiter als die [[denotationelle Semantik]]. Es werden keine konkreten Speicher transformiert, sondern nur logische Aussagen über Speicher, genauer gesagt über Werte von Programmvariablen in ihnen. Dabei entspricht die axiomatische Semantik der Sicht des Programmierers. Sie scheint im Gegensatz zur [[Operationelle Semantik|operationellen Semantik]] nur für [[Imperative Programmierung|imperative Sprachen]] geeignet zu sein.

Es existieren zwei Hauptausprägungen, der [[Hoare-Kalkül]] und der [[wp-Kalkül]].

== Literatur ==
* Hanne Riis Nielson, Flemming Nielson: ''Semantics With Applications. A Formal Introduction.'' John Wiley & Sons, Chichester 1992, ISBN 0-471-92980-8.

[[Kategorie:Theoretische Informatik]]