Formale Semantikdefinition

Übersicht: Formale Semantikdefinition

• Warum Formale Semantikdefinition?
• Drei Hauptansätze

Eine formale und sehr präzise Beschreibung der Bedeutung von Programmen ist eine unerlässliche Voraussetzung für viele Dinge, die Programmiersprachen und Programmierung betreffen, so insbesondere für

• die Definition von Programmiersprachen für den Benutzer (beispielsweise mittels eines Sprachberichtes), um ihm Sicherheit bei der Erstellung von Programmen zu geben
• die Implementierung von Programmiersprachen durch einen Übersetzer oder einen Interpreter, um die Portabilität von Programmen zu gewährleisten
• das formale Arbeiten mit Programmen, etwa bei der Verifikation (hier versucht man nachträglich zu beweisen, dass ein Programm eine gegebene Aufgabestellung erfüllt) oder bei der formalen Herleitung (hier entwickelt man zielgerichtet und meist regelgesteuert ein Programm ausgehend von einer gegebenen Aufgabestellung)

• Operationelle Semantik
  Diese Art der Semantikdefinition entspricht hauptsächlich der Sicht des Implementierers. Sie beschreibt die Auswertung eines Programms als Folge elementarer Berechnungsschritte auf einer konkreten oder abstrakten Maschine. Die operationelle Semantik beschreibt also im Detail sämtliche Zwischenzustände bei der Abarbeitung des Programms; sie ist deshalb vorzuziehen, wenn die Semantik einer Programmiersprache in Hinblick auf eine korrekte Implementierung formalisiert werden soll. In einem gewissen Sinne ist auch jeder Übersetzer und jeder Interpreter eine operationelle Semantikspezifikation.
• Denotationelle Semantik
  Diese Art der Semantikdefinition entspricht hauptsächlich der Sicht des Sprachdesigners. Sie beschreibt die Ein/Ausgabefunktion für syntaktische Konstrukte induktiv über den Aufbau der Syntax. Die Grundidee ist dabei, elementare syntaktische Elemente in allgemeiner(Mathematik) Sprache zu beschreiben und damit induktiv die Bedeutung zusammengesetzter Elemente zu erklären. Die denotationelle Semantik ist gut zum Beweis von Programmeigenschaften geeignet.
• Axiomatische Semantik
  Diese Art der Semantikdefinition entspricht hauptsächlich der Sicht des Programmierers. Sie beschreibt logische Eigenschaften eines Programms. Die Axiomatische Semantik ist gut zum Beweis der Korrektheit der Programme geeignet.