Axiomatische Semantik
Die axiomatische Semantik der Informatik beschreibt die Bedeutung von Programmen durch Schlussregeln, 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 operationellen Semantik nur für 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 1992
This article is issued from Wikipedia. The text is licensed under Creative Commons - Attribution - Sharealike. The authors of the article are listed here. Additional terms may apply for the media files, click on images to show image meta data.