Semantik Von Programmiersprachen

ISBN-13: 9783540151630 / Niemiecki / Miękka / 1989 / 211 str.

Elfriede Fehr

Opis

Dieses Buch vermittelt Techniken zur Formalisierung der Semantik (Bedeutungsinhalte) von Programmiersprachen. Zunachst werden unterschiedliche Formalisierungsansatze (die operationelle, denotationelle und axiomatische Semantik) vorgestellt und diskutiert. Anschliessend wird die mathematische Theorie der semantischen Bereiche entwickelt, die bei der zur Zeit wichtigsten, der denotationellen Methode, Anwendung findet. Danach wird schrittweise eine umfassende, PASCAL-orientierte Programmiersprache entwickelt und die Semantik der einzelnen Sprachkonstrukte denotationell spezifiziert. Die Fortsetzungssemantik (continuation semantics) wird dabei systematisch erklart und verwendet. Schliesslich wird auf die Anwendung dieser Techniken eingegangen, insbesondere im Rahmen des Compilerbaus und als Grundlage zur Entwicklung funktionaler Programmiersprachen. Das Wissen, das in diesem Buch vermittelt wird, ermoglicht es, selbstandig die Semantik neuer, unterschiedlicher Sprachkonstrukte formal zu definieren und damit umzugehen, und naturlich vorgegebene formale Beschreibungen zu verstehen. Dies ist besonders wichtig bei der Entwicklung neuer Sprachen, beim Beweisen von Programmeigenschaften und beim Compilerbau."

Spis treści

1 Einleitung.- 2 Verschiedene Methoden der formalen Semantikspezifikation.- 2.1 Die Beispielsprache WHILE.- 2.2 Informelle Beschreibung der Semantik von WHILE.- 2.2.1 Diskussion der informellen Semantik von WHILE.- 2.3 Operationelle Semantik der Sprache WHILE.- 2.3.1 Die WSKEA-Maschine.- 2.3.2 Diskussion der operationeilen Semantik von WHILE.- 2.3.3 Die Reduktionssemantik der Sprache WHILE.- 2.3.4 Äquivalenz von operationeller und Reduktionssemantik.- 2.4 Denotationelle Semantik der Sprache WHILE.- 2.4.1 Äquivalenz von operationeller und denotationeller Semantik.- 2.5 Axiomatische Semantik der Sprache WHILE.- 2.5.1 Beziehung der axiomatischen zur denotationellen und operationellen Semantik.- 3 Mathematische Grundlagen.- 3.1 Theorie der semantischen Bereiche.- 3.1.1 Elementare Bereiche.- 3.1.2 Kartesische Produkte und Folgen.- 3.1.3 Summen.- 3.1.4 Funktionen.- 3.1.5 Rekursiv definierte Bereiche.- 3.2 Der getypte ?-Kalkül als Metasprache.- 3.3 Lösung rekursiver Bereichsgleichungen.- 4 Detaillierte Behandlung der denotationellen Semantik.- 4.1 Spezielle Funktionen und Konventionen.- 4.1.1 Curry-Isomorphien.- 4.1.2 Die bedingte Verzweigung.- 4.1.3 Basisoperationen.- 4.1.4 Rekursion.- 4.1.5 Modifikation von Funktionen.- 4.1.6 Die verallgemeinerte Komposition.- 4.2 Denotationelle Semantik der Sprache WHILE unter Verwendung der neuen Notationen.- 4.3 Entwicklung der Standardsemantik unter besonderer Berücksichtigung der Fortsetzungssemantik.- 4.3.1 Fortsetzungen.- 4.3.2 Fortsetzungssemantik der Sprache WHILE.- 4.3.3 Typüberprüfung.- 4.3.4 Modifikation des Ausgabebereiches.- 4.3.5 Modifikation des Bereiches SPEICHER.- 4.3.6 Standardwertebereiche.- 4.3.7 Deklarationen.- 4.3.8 Standardfortsetzungsfunktionen.- 4.3.9 Fortsetzungstransformationen.- 4.3.10 Verallgemeinerung der Wertzuweisung.- 4.3.11 Standardsemantik von Prozeduren und Funktionen.- 4.4 Die Standardsemantik der Sprache PASCAL0.- 4.4.1 Syntax von PASCAL0.- 4.4.2 Semantik von PASCAL0.- 4.4.3 Bemerkungen zur Definition von PASCAL0.- 4.4.4 Berechnung der denotationellen Semantik eines Beispielprogramms.- 4.5 Weitere Sprachkonzepte, analysiert im Rahmen der Standardsemantik.- 4.5.1 Sprünge und Abbrüche.- 4.5.2 Verallgemeinerungen des Prozedur- und Funktionskonzeptes.- 4.5.3 Datenstrukturen.- 5 Funktionale Programmiersprachen.- 5.1 Die Programmiersprache LISP.- 5.1.1 Syntax von Kern-LISP.- 5.1.2 Statische Semantik von Kern-LISP.- 5.1.3 Operationelle Semantik von Kern-LISP.- 5.1.4 Inkonsistenzen von LISP.- 5.2 FP-Systeme.- 5.3 Programmieren mit rekursiven Gleichungssystemen.- 6 Anwendungen der denotationellen Semantik bei der Implementierung höherer Programmiersprachen.- 6.1 Systematische Codeerzeugung aus der Standardsemantik.- 6.2 Implementierung nach Übersetzung in kombinatorische Ausdrücke.- 6.3 Implementierung auf Reduktionsmaschinen.- 6.3.1 Die Reduktionsmaschine von Berkling und Kluge.- 6.3.2 Die Baumarchitektur von Mago.- 6.3.3 Die Graphreduktion nach Wadsworth.