Semantik (Informatik) - Semantics (computer science)

In der Programmiersprache Theorie , Semantik ist das Feld mit der strengen mathematischen Untersuchung der Bedeutung des betreffenden Programmiersprachen . Dazu wertet es die Bedeutung von syntaktisch gültigen Strings aus, die von einer bestimmten Programmiersprache definiert werden, und zeigt die damit verbundene Berechnung. In einem solchen Fall, in dem die Auswertung von syntaktisch ungültigen Zeichenfolgen wäre, wäre das Ergebnis keine Berechnung. Semantik beschreibt die Prozesse, denen ein Computer bei der Ausführung eines Programms in dieser spezifischen Sprache folgt. Dies kann gezeigt werden, indem die Beziehung zwischen Eingabe und Ausgabe eines Programms beschrieben wird, oder eine Erklärung, wie das Programm auf einer bestimmten Plattform ausgeführt wird, wodurch ein Berechnungsmodell erstellt wird .

Überblick

Das Gebiet der formalen Semantik umfasst alle der folgenden Bereiche:

  • Die Definition semantischer Modelle
  • Die Beziehungen zwischen verschiedenen semantischen Modellen
  • Die Beziehungen zwischen verschiedenen Bedeutungszugängen
  • Die Beziehung zwischen Berechnung und den zugrunde liegenden mathematischen Strukturen aus Bereichen wie Logik , Mengenlehre , Modelltheorie , Kategorientheorie usw.

Es hat enge Verbindungen zu anderen Bereichen der Informatik wie Programmiersprachendesign , Typentheorie , Compiler und Interpreter , Programmverifikation und Modellprüfung .

Ansätze

Es gibt viele Ansätze zur formalen Semantik; diese gehören zu drei großen Klassen:

  • Denotationssemantik , wobei jede Phrase in der Sprache als Denotation interpretiert wird, dh als begriffliche Bedeutung, die abstrakt gedacht werden kann. Solche Bezeichnungen sind oft mathematische Objekte, die einen mathematischen Raum bewohnen, aber dies ist keine Voraussetzung. Aus praktischer Notwendigkeit werden Denotationen in irgendeiner Form mathematischer Notation beschrieben, die wiederum als denotationale Metasprache formalisiert werden kann. Zum Beispielübersetzt diedenotationale Semantik funktionaler Sprachen die Sprache oft in die Domänentheorie . Denotationale semantische Beschreibungen können auch als kompositorische Übersetzungen von einer Programmiersprache in die denotationale Metasprache dienen und als Grundlage für den Entwurf von Compilern verwendet werden .
  • Operative Semantik , wobei die Ausführung der Sprache direkt (und nicht durch Übersetzung) beschrieben wird. Operative Semantik entspricht lose der Interpretation , obwohl die "Implementierungssprache" des Interpreten im Allgemeinen ein mathematischer Formalismus ist. Die Betriebssemantik kann eine abstrakte Maschine (wie die SECD-Maschine ) definieren und Phrasen Bedeutung verleihen, indem sie die Übergänge beschreibt, die sie bei Zuständen der Maschine induzieren. Alternativ kann, wie beim reinen Lambda-Kalkül , die operationale Semantik über syntaktische Transformationen auf Phrasen der Sprache selbst definiert werden;
  • Axiomatische Semantik , bei der man Phrasen Bedeutung verleiht, indem man diefür siegeltenden Axiome beschreibt. Die axiomatische Semantik macht keinen Unterschied zwischen der Bedeutung einer Phrase und den logischen Formeln, die sie beschreiben; seine Bedeutung ist genau das, was man in irgendeiner Logik daran beweisen kann. Das kanonische Beispiel der axiomatischen Semantik ist die Hoare-Logik .

Abgesehen von der Wahl zwischen denotationalen, operationalen oder axiomatischen Ansätzen ergeben sich die meisten Variationen in formalen semantischen Systemen aus der Wahl des unterstützenden mathematischen Formalismus.

Variationen

Einige Variationen der formalen Semantik umfassen die folgenden:

Beziehungen beschreiben

Aus verschiedenen Gründen kann man die Beziehungen zwischen verschiedenen formalen Semantiken beschreiben. Beispielsweise:

  • Zu beweisen, dass eine bestimmte operationale Semantik für eine Sprache die logischen Formeln einer axiomatischen Semantik für diese Sprache erfüllt. Ein solcher Beweis zeigt, dass es "stichhaltig" ist, über eine bestimmte (operative) Interpretationsstrategie mit einem bestimmten (axiomatischen) Beweissystem zu argumentieren .
  • Um zu beweisen, dass die operationelle Semantik einer High-Level-Maschine durch eine Simulation mit der Semantik einer Low-Level -Maschine in Beziehung steht , wobei die Low-Level-abstrakte Maschine mehr primitive Operationen enthält als die High-Level-abstrakte Maschinendefinition einer gegebenen Sprache. Ein solcher Beweis zeigt, dass die Low-Level-Maschine die High-Level-Maschine "treu umsetzt".

Es ist auch möglich, multiple Semantiken durch Abstraktionen über die Theorie der abstrakten Interpretation in Beziehung zu setzen .

Geschichte

Robert W. Floyd wird zugeschrieben, das Gebiet der Programmiersprachensemantik in Floyd (1967) begründet zu haben .

Siehe auch

Verweise

Weiterlesen

Lehrbücher
Vorlesungsnotizen

Externe Links