Praktische Semantik von Programmiersprachen - Cheatsheet

Small-Step- und Big-Step-Semantik

Definition:

Small-Step- und Big-Step-Semantik sind zwei Ansätze zur formalen Beschreibung der Ausführung von Programmen.

Details:

• Small-Step-Semantik: Definiert die Programmausführung als eine Folge kleiner Berechnungsschritte.
• Nutzt Übergangsrelationen: \(e \rightarrow e'\) bedeutet Ausdruck \(e\) reduziert sich zu \(e'\).
• Big-Step-Semantik: Beschreibt die Ausführung eines gesamten Programms in einem großen Schritt.
• Nutzt Bewertungsrelationen: \(e \Downarrow v\) bedeutet Ausdruck \(e\) wird ausgewertet zu Wert \(v\).
• Small-Step hat den Vorteil, Zwischenschritte zu zeigen; Big-Step ist oft intuitiver für die Gesamtauswertung.
• Beide Semantiken werden verwendet, um verschiedene Aspekte der Programmausführung zu analysieren und zu beweisen.

Deterministische vs. nicht-deterministische Semantik

Definition:

Deterministische Semantik: Gibt für jede Eingabe genau ein definiertes Ergebnis zurück. Nicht-deterministische Semantik: Kann für dieselbe Eingabe verschiedene mögliche Ergebnisse haben.

Details:

• Deterministische Semantik:
• Eindeutiges Verhalten
• Vorhersehbare Ausführung
• Reproduzierbare Ergebnisse
• Nicht-deterministische Semantik:
• Mehrere mögliche Verhaltensweisen
• Unvorhersehbare Ausführung
• Potentiell verschiedene Ergebnisse bei gleicher Eingabe

Lambda-Kalkül

Definition:

Formales System zur Untersuchung von Funktionen und deren Anwendungen.

Details:

• Kernbestandteil der funktionalen Programmierung
• Abstraktion von Funktionen: \(\lambda x. x+1\)
• Applikation von Funktionen: \( (\lambda x. x+1)\ 2 = 3 \)
• Reduktionen: \( \beta \text{-Reduktion}, \eta \text{-Reduktion} \)
• Freie und gebundene Variablen

Hoare-Logik

Definition:

Hoare-Logik ist ein formales System zur Spezifikation und Überprüfung der Korrektheit von Computerprogrammen basierend auf Vor- und Nachbedingungen.

Details:

• Hoare-Dreier: \[ \{P\} \;C\; \{Q\} \] - \(P\): Vorbedingung - \(Q\): Nachbedingung - \(C\): Programm
• Partielle Korrektheit: Wenn \(P\) wahr und \(C\) terminierend, dann \(Q\) wahr
• Totale Korrektheit: Partielle Korrektheit und \(C\) terminiert
• Regeln: Sequenz, Auswahl, Schleifen, etc.

Typsicherheitsbeweise

Definition:

Typsicherheitsbeweise belegen, dass ein Programm zur Laufzeit keine Typfehler erzeugt.

Details:

• Wesentliche Eigenschaft: Zeigt Formalitätsgrad einer Programmiersprache.
• Besteht aus: Typregeln und Beweisführung.
• Typregeln: Formale Regeln zur Überprüfung der Typkonsistenz.
• Beweisführung: Formalisierung und Nachweis, dass alle gültigen Programme typensicher sind.
• Typkonsistenz: Jeder Ausdruck im Programm hat einen korrekten Typ.
• Führt zu sicherer Programmausführung ohne Typfehlerrisiko.
• Beweis durch strukturelle Induktion: Oft genutzt, um Typsicherheitsbeweise zu führen.
• Wichtige Theoreme: Progression und Konservierung.
• Progression: Ein typisiertes Programm kann entweder einen Wert produzieren oder einen weiteren Berechnungsschritt durchführen.
• Konservierung: Wenn ein Ausdruck einen weiteren Berechnungsschritt durchführen kann, bleibt der Typ des Ausdrucks erhalten.
• Formale Darstellung: \[ \text{Wenn } \Gamma \vdash e : \tau \text{ und } e \rightarrow e' \text{ dann } \Gamma \vdash e' : \tau \]

Typinferenzalgorithmen

Definition:

Automatische Ermittlung der Typen von Ausdrücken in Programmiersprachen ohne explizite Typangaben.

Details:

• Wichtig für die statische Typprüfung
• Verwendet Typumgebungen zur Assoziation von Variablen und Typen
• Algorithmus-Beispiele: Hindley-Milner, Algorithm W
• Erfordert Unifikation zur Lösung von Typgleichungen
• Ergebnisse: Typsignaturen für alle Ausdrücke

Syntaxanalyse und Parsererzeugung

Definition:

Syntaxanalyse bezieht sich auf die Analyse der grammatikalischen Struktur von Quellcode, während Parsererzeugung den Prozess der Erstellung eines Parsers zur Analyse dieser Struktur beschreibt.

Details:

• Ziel: Überprüfung und Strukturierung des Quellcodes entsprechend einer formalen Grammatik.
• Parser-Typen: Top-Down (z.B., rekursiver Abstieg) und Bottom-Up (z.B., Shift-Reduce).
• Werkzeuge: Lex und Yacc (oder Flex und Bison), ANTLR.
• Kontextfreie Grammatiken (CFG): Häufig verwendet. Ein CFG ist definiert durch \(G = (N, \Sigma, P, S)\), wobei \(N\) Nichtterminale, \(\Sigma\) Terminale, \(P\) Produktionsregeln und \(S\) das Startsymbol sind.
• Parsebäume: Geeignet zur Darstellung der hierarchischen Struktur eines Programms.
• Ambiguität: Wenn eine Grammatik mehrere Parsebäume für einen String hat, ist sie mehrdeutig.
• LL(1) und LR(1) Grammatiken: Spezielle Formen zur Vermeidung von Mehrdeutigkeiten.

Interpreter- und Compilerbau

Definition:

Verständnis und Implementierung der Übersetzungsprozesse von Programmiersprachen in Maschinenbefehle; Fokus auf Unterscheidung zwischen Interpretern und Compilern.

Details:

• Interpreter: Führt Quellcode Zeile für Zeile aus; keine Zwischenspeicherung in Maschinencode.
• Compiler: Übersetzt gesamten Quellcode in Maschinencode vor der Ausführung.
• Phasen eines Compilers: Lexikalische Analyse (\textit{Tokenisierung}), Syntaxanalyse (\textit{Parsing}), Semantische Analyse, Optimierung, Codegenerierung.
• Interpreterbau: Implementierung eines Interpreters oft einfacher als bei einem Compiler; nützlich für dynamische Sprachen.
• JIT-Compiler (Just-In-Time): Kombination aus Compilation und Interpretation; zur Laufzeit kompiliert.