Praktische Semantik von Programmiersprachen - Exam

Aufgabe 1)

Du hast ein fiktives ProgrammiersPrachen-Framework entworfen, welches aus den folgenden Bestandteilen besteht: Syntax, denotationale Semantik, operationale Semantik, axiomatische Semantik, Fixpunkt-Theorie und semantische Äquivalenz. Die Syntax der Programmiersprache wird durch eine abstrakte Grammatik definiert, und die Bedeutung der Programme wird unter Verwendung der mathematischen Definitionen bestimmt.

a)

Implementiere einen einfachen Interpreter für die Programmiersprache . Dies sollte unter Verwendung der operationalen Semantik erfolgen, um die Ausführungen von Programmschritten durch Zustandsübergänge zu beschreiben. Gegeben sei das folgende Programm in der Sprache:

'let x = 5 in let y = x + 7 in return y'

Beschreibe den Zustandsübergang für jede Zeile des Programms, und zeige Schritt für Schritt, wie der Interpreter zu seinem Endzustand gelangt.

Lösung:

Um einen einfachen Interpreter für die gegebene Programmiersprache zu implementieren, verwenden wir die operationale Semantik, um die Ausführung einzelner Programmschritte durch Zustandsübergänge zu beschreiben. Betrachten wir das folgende Programm:

'let x = 5 in let y = x + 7 in return y'

Wir gehen Schritt für Schritt vor:

• Startzustand: Der Anfangszustand, den wir haben, ist eine leere Umgebung (environment), die keine Variablenzuweisungen enthält.
• Schritt 1: 'let x = 5': Zuweisen des Wertes 5 zur Variablen x.Zustand: {x: 5}
• Schritt 2: 'let y = x + 7': Berechnen des Ausdrucks x + 7 unter Verwendung des aktuellen Zustands.Da x = 5, wird der Ausdruck zu 5 + 7, was 12 ergibt. Dann wird y der Wert 12 zugewiesen.Zustand: {x: 5, y: 12}
• Schritt 3: 'return y': Geben des Werts der Variablen y zurück.Da y = 12, ist das Endergebnis 12.

Der Interpreter führt die Zustandsübergänge wie oben beschrieben aus und erreicht den Endzustand, in dem y den Wert 12 hat, und gibt diesen Wert als Ergebnis zurück.

Im folgenden Abschnitt wird ein einfacher Python-Interpreter-Code bereitgestellt, der diese Schritte simuliert:

def interpreter(program):    env = {}    lines = program.split(' in ')    for line in lines:        if line.startswith('let '):            var_expr = line[4:].split(' = ')            var = var_expr[0].strip()            expr = var_expr[1].strip()            if '+' in expr:                parts = expr.split(' + ')                val = int(env[parts[0].strip()]) + int(parts[1].strip())            else:                val = int(expr)            env[var] = val        elif line.startswith('return '):            return env[line[7:].strip()]    return None# Beispielverwendungprogram = 'let x = 5 in let y = x + 7 in return y'ergebnis = interpreter(program)print(f'Das Ergebnis des Programms ist: {ergebnis}')

Die Ausgabe des Programms sollte sein:

Das Ergebnis des Programms ist: 12

b)

Formuliere die denotationale Semantik für eine einfache mathematische Funktion in der Programmiersprache, z.B. die Funktion 'f(x) = x^2 + 3x + 2'. Definiere die Bedeutung dieser Funktion als ein mathematisches Objekt und demonstriere, wie der Wert der Funktion für einen gegebenen Eingabewert (z.B. x = 4) berechnet wird. Verwende dabei die Fixpunkt-Theorie, um zu zeigen, wie rekursive Definitionen und Schleifen interpretiert werden könnten.

Lösung:

Um die denotationale Semantik für eine einfache mathematische Funktion zu formulieren, betrachten wir die Funktion:

f(x) = x^2 + 3x + 2

Die denotationale Semantik zielt darauf ab, die Bedeutung dieses Ausdrucks als mathematisches Objekt zu definieren. Wir definieren die Semantik in mehreren Schritten:

• Definition der Funktion: Wir definieren die Funktion f als eine mathematische Abbildung, die einen Eingabewert x nimmt und den Wert von x^2 + 3x + 2 berechnet.Die Funktion f kann mathematisch wie folgt ausgedrückt werden:

• f(x) = x^2 + 3x + 2

Berechnung des Funktionswerts: Um den Wert der Funktion für einen gegebenen Eingabewert, z.B. x = 4, zu berechnen, setzen wir den Wert von x in die Funktion ein:

• f(4) = 4^2 + 3*4 + 2

Die Berechnung erfolgt schrittweise:

• f(4) = 16 + 12 + 2
• f(4) = 30

Der Wert der Funktion für x = 4 ist also 30.

Verwendung der Fixpunkt-Theorie: Um rekursive Definitionen und Schleifen zu interpretieren, verwenden wir die Fixpunkt-Theorie. Diese Theorie erlaubt es uns, den Fixpunkt einer Funktion zu finden, d.h. einen Wert, der unverändert bleibt, wenn die Funktion darauf angewendet wird.

Betrachten wir eine rekursive Funktion g(n), die die Fakultät von n berechnet:

g(n) = if n == 0 then 1 else n * g(n - 1)

Um dies mithilfe der Fixpunkt-Theorie zu interpretieren, definieren wir eine Funktion F, die eine Funktion h auf einen neuen Wert abbildet:

F(h) = λn. if n == 0 then 1 else n * h(n - 1)

Ein Fixpunkt dieser Funktion F ist eine Funktion g, die die Eigenschaft g = F(g) erfüllt. Der Fixpunkt g ist die gesuchte Fakultätsfunktion.

Einfach ausgedrückt: g bleibt unverändert, wenn F darauf angewendet wird, was bedeutet, dass g(n) der berechnete Wert der Fakultät von n ist.

Zusammenfassend ist die denotationale Semantik ein wertvolles Werkzeug zur Definition und Berechnung der Bedeutung von Funktionen in Programmiersprachen. Die Fixpunkt-Theorie bietet eine mächtige Methode zur Behandlung rekursiver Definitionen und Schleifen.

Aufgabe 2)

Big-Step und Small-Step Semantik

Big-Step und Small-Step Semantik sind zwei formale Methoden zur Beschreibung der Auswertung von Programmen. Die Big-Step Semantik (auch natürliche Semantik genannt) beschreibt, wie ein Ausdruck direkt zu seinem Endwert führt. Dies wird oft durch die Notation \(\frac{e \rightarrow v}{E \rightarrow V}\) dargestellt und eignet sich für die Beschreibung des gesamten Evaluierungsvorgangs auf einer höheren Ebene. Auf der anderen Seite beschreibt die Small-Step Semantik (auch strukturelle oder operationelle Semantik genannt) die Auswertung in kleinen Schritten. Diese wird durch die Notation \(\frac{e \rightarrow e'}{E \rightarrow E'}\) dargestellt und eignet sich für die Darstellung von Zwischenschritten und der präzisen Kontrolle des Auswertungsvorgangs.

• Big-Step Semantik: Definiert die direkte Auswertung zum Endwert.
• Small-Step Semantik: Definiert die schrittweise Auswertung von Zwischenschritten bis zum Endwert.

a)

Betrachte die folgende Ausdruck in einer einfachen Programmiersprache:

 a := 1 + 2 * 3; 

Beschreibe die Auswertung dieses Ausdrucks einmal mit der Big-Step Semantik und einmal mit der Small-Step Semantik.

Lösung:

Big-Step und Small-Step Semantik

Aufgabe: Betrachte den folgenden Ausdruck in einer einfachen Programmiersprache:

 a := 1 + 2 * 3; 

Beschreibe die Auswertung dieses Ausdrucks einmal mit der Big-Step Semantik und einmal mit der Small-Step Semantik.

• Big-Step Semantik: Definiert die direkte Auswertung zum Endwert.
• Small-Step Semantik: Definiert die schrittweise Auswertung von Zwischenschritten bis zum Endwert.

Big-Step Semantik

Bei der Big-Step Semantik wird der Ausdruck direkt zu seinem Endwert ausgewertet. Wir schauen uns den gesamten Evaluierungsvorgang auf einer höheren Ebene an.

1. Der gesamte Ausdruck \texttt{1 + 2 * 3} wird direkt ausgewertet.

• 2 * 3: Zuerst wird die Multiplikation durchgeführt: \texttt{2 * 3 = 6}
• 1 + 6: Dann wird die Addition durchgeführt: \texttt{1 + 6 = 7}

2. Der Ausdruck \texttt{a := 1 + 2 * 3} wird zu \texttt{a := 7}.

In dieser Darstellung haben wir den gesamten Ausdruck in einem Schritt ausgewertet, wobei wir zuerst die innere Multiplikation berechnet und dann die äußere Addition durchgeführt haben.

Small-Step Semantik

Bei der Small-Step Semantik wird der Ausdruck schrittweise ausgewertet. Wir zeigen jede kleine Auswertung, um die Zwischenschritte und die präzise Kontrolle des Auswertungsvorgangs zu veranschaulichen.

1. Startzustand: \texttt{a := 1 + 2 * 3}

2. Erste Auswertung: \texttt{1 + 2 * 3} --> \texttt{1 + 6}

• Hier wird das erste Paar im Ausdruck ausgewertet: \texttt{2 * 3}
• Daraus ergibt sich: \texttt{2 * 3 = 6}

3. Zweite Auswertung: \texttt{1 + 6} --> \texttt{7}

• Jetzt wird der verbleibende Ausdruck ausgewertet: \texttt{1 + 6}
• Daraus ergibt sich: \texttt{1 + 6 = 7}

4. Ergebnis: \texttt{a := 7}

In dieser Darstellung wird jeder kleine Schritt einzeln gezeigt, um die genaue Reihenfolge der Auswertungen zu verdeutlichen.

b)

Gegeben sei die folgende Big-Step Regel:

 \[\frac{a \rightarrow 1 \text{ und } b \rightarrow 2}{a + b \rightarrow 3}\]

Implementiere die entsprechende Small-Step Regel für denselben Ausdruck a + b, wobei a nach 1 und b nach 2 ausgewertet wird.

Lösung:

Big-Step und Small-Step Semantik

Big-Step und Small-Step Semantik sind zwei formale Methoden zur Beschreibung der Auswertung von Programmen. Die Big-Step Semantik (auch natürliche Semantik genannt) beschreibt, wie ein Ausdruck direkt zu seinem Endwert führt. Dies wird oft durch die Notation \(\frac{e \rightarrow v}{E \rightarrow V}\) dargestellt und eignet sich für die Beschreibung des gesamten Evaluierungsvorgangs auf einer höheren Ebene. Auf der anderen Seite beschreibt die Small-Step Semantik (auch strukturelle oder operationelle Semantik genannt) die Auswertung in kleinen Schritten. Diese wird durch die Notation \(\frac{e \rightarrow e'}{E \rightarrow E'}\) dargestellt und eignet sich für die Darstellung von Zwischenschritten und der präzisen Kontrolle des Auswertungsvorgangs.

• Big-Step Semantik: Definiert die direkte Auswertung zum Endwert.
• Small-Step Semantik: Definiert die schrittweise Auswertung von Zwischenschritten bis zum Endwert.

Aufgabe: Gegeben sei die folgende Big-Step Regel:

\[\frac{a \rightarrow 1 \text{ und } b \rightarrow 2}{a + b \rightarrow 3}\]

Implementiere die entsprechende Small-Step Regel für denselben Ausdruck a + b, wobei a nach 1 und b nach 2 ausgewertet wird.

Small-Step Semantik

Die Small-Step Semantik beschreibt die Auswertung in kleinen Schritten, wobei jeder Schritt eine einzelne Transformation des Ausdrucks ist. Für den Ausdruck a + b haben wir folgende Schritte:

• Startzustand: a + b
• Erster Schritt: a + b -> 1 + bWeil a zu 1 ausgewertet wird.
• Zweiter Schritt: 1 + b -> 1 + 2Weil b zu 2 ausgewertet wird.
• Dritter Schritt: 1 + 2 -> 3Weil der Ausdruck jetzt vollständig ausgewertet werden kann.

Zusammengefasst wird die Small-Step Semantik für den Ausdruck a + b, wobei a nach 1 und b nach 2 ausgewertet wird, wie folgt notiert:

\[\frac{a \rightarrow 1}{a + b \rightarrow 1 + b}\]\[\frac{b \rightarrow 2}{1 + b \rightarrow 1 + 2}\]\[1 + 2 \rightarrow 3\]

Diese Notation beschreibt die schrittweise Transformation des Ausdrucks, bis die endgültige Auswertung erreicht ist.

c)

Zeige, dass die Big-Step und Small-Step Semantik für den Ausdruck a := 2 + 2 zum selben Endwert führen. Verwende dabei beide Semantiken um den vollständigen Auswertungsvorgang darzustellen.

Lösung:

Big-Step und Small-Step Semantik

Big-Step und Small-Step Semantik sind zwei formale Methoden zur Beschreibung der Auswertung von Programmen. Die Big-Step Semantik (auch natürliche Semantik genannt) beschreibt, wie ein Ausdruck direkt zu seinem Endwert führt. Dies wird oft durch die Notation \(\frac{e \rightarrow v}{E \rightarrow V}\) dargestellt und eignet sich für die Beschreibung des gesamten Evaluierungsvorgangs auf einer höheren Ebene. Auf der anderen Seite beschreibt die Small-Step Semantik (auch strukturelle oder operationelle Semantik genannt) die Auswertung in kleinen Schritten. Diese wird durch die Notation \(\frac{e \rightarrow e'}{E \rightarrow E'}\) dargestellt und eignet sich für die Darstellung von Zwischenschritten und der präzisen Kontrolle des Auswertungsvorgangs.

• Big-Step Semantik: Definiert die direkte Auswertung zum Endwert.
• Small-Step Semantik: Definiert die schrittweise Auswertung von Zwischenschritten bis zum Endwert.

Aufgabe: Zeige, dass die Big-Step und Small-Step Semantik für den Ausdruck a := 2 + 2 zum selben Endwert führen. Verwende dabei beide Semantiken, um den vollständigen Auswertungsvorgang darzustellen.

Big-Step Semantik

Bei der Big-Step Semantik wird der Ausdruck direkt zu seinem Endwert ausgewertet. Wir betrachten den gesamten Evaluierungsvorgang auf einer höheren Ebene:

• Der Ausdruck 2 + 2 wird direkt ausgewertet:
• 2 + 2: Die Addition ergibt 4.
• Der gesamte Ausdruck a := 2 + 2 wird zu a := 4.

Formal dargestellt:

\[\frac{2 \rightarrow 2 \text{ und } 2 \rightarrow 2}{2 + 2 \rightarrow 4}\]

Zusammengefasst: a := 2 + 2 \rightarrow a := 4.

Small-Step Semantik

Bei der Small-Step Semantik wird der Ausdruck schrittweise ausgewertet. Wir zeigen jede kleine Auswertung, um die Zwischenschritte und die präzise Kontrolle des Auswertungsvorgangs zu veranschaulichen.

1. Startzustand: a := 2 + 2

2. Erster Schritt: 2 + 2 \rightarrow 4

• Hier wird der Ausdruck ausgewertet.

3. Ergebnis: a := 4

Formal dargestellt:

\[\frac{2 \rightarrow 2}{2 + 2 \rightarrow 4}\]

Zusammengefasst: a := 2 + 2 \rightarrow a := 4.

Dies zeigt, dass sowohl die Big-Step als auch die Small-Step Semantik für den Ausdruck a := 2 + 2 zum selben Endwert a := 4 führen.

d)

Betrachte den Ausdruck a := 1; b := a + 1. Zeige, wie die Small-Step Semantik präzises Wissen über den Zustand zwischen den Schritten der Auswertung liefert. Vergleiche dies mit der Big-Step Semantik und diskutiere die Vor- und Nachteile beider Ansätze.

Lösung:

Big-Step und Small-Step Semantik

Big-Step und Small-Step Semantik sind zwei formale Methoden zur Beschreibung der Auswertung von Programmen. Die Big-Step Semantik (auch natürliche Semantik genannt) beschreibt, wie ein Ausdruck direkt zu seinem Endwert führt. Dies wird oft durch die Notation \(\frac{e \rightarrow v}{E \rightarrow V}\) dargestellt und eignet sich für die Beschreibung des gesamten Evaluierungsvorgangs auf einer höheren Ebene. Auf der anderen Seite beschreibt die Small-Step Semantik (auch strukturelle oder operationelle Semantik genannt) die Auswertung in kleinen Schritten. Diese wird durch die Notation \(\frac{e \rightarrow e'}{E \rightarrow E'}\) dargestellt und eignet sich für die Darstellung von Zwischenschritten und der präzisen Kontrolle des Auswertungsvorgangs.

• Big-Step Semantik: Definiert die direkte Auswertung zum Endwert.
• Small-Step Semantik: Definiert die schrittweise Auswertung von Zwischenschritten bis zum Endwert.

Aufgabe:

Betrachte den Ausdruck a := 1; b := a + 1. Zeige, wie die Small-Step Semantik präzises Wissen über den Zustand zwischen den Schritten der Auswertung liefert. Vergleiche dies mit der Big-Step Semantik und diskutiere die Vor- und Nachteile beider Ansätze.

Small-Step Semantik

Die Small-Step Semantik beschreibt die Auswertung in kleinen Schritten und erlaubt somit eine präzise Kontrolle über den Zustand des Programms zwischen den Schritten. Betrachten wir den Ausdruck a := 1; b := a + 1 Schritt für Schritt:

• Startzustand: a := 1; b := a + 1
• Erster Schritt: a := 1; b := a + 1 \rightarrow (a = 1); b := a + 1Hier wird a := 1 ausgewertet und a wird auf 1 gesetzt.
• Zweiter Schritt: (a = 1); b := a + 1 \rightarrow (a = 1); b := 1 + 1Hier wird der Ausdruck a durch 1 ersetzt.
• Dritter Schritt: (a = 1); b := 1 + 1 \rightarrow (a = 1); b := 2Hier wird der Ausdruck 1 + 1 ausgewertet.

Auf diese Weise verfolgt die Small-Step Semantik den Zustand des Programms in jedem Zwischenschritt.

Big-Step Semantik

Die Big-Step Semantik beschreibt die direkte Auswertung zum Endwert, ohne die Zwischenschritte explizit darzustellen. Betrachten wir den Ausdruck a := 1; b := a + 1:

• Startzustand: a := 1; b := a + 1
• Auswertung: Der gesamte Ausdruck wird direkt ausgewertet:
• a := 1 setzt a auf 1.
• Für b := a + 1 wird a durch 1 ersetzt und 1 + 1 wird direkt zu 2 ausgewertet.
• Endzustand: a = 1 und b = 2.

Formal dargestellt:

\[\frac{a := 1 \rightarrow a = 1 \text{ und } a + 1 \rightarrow 2}{a := 1; b := a + 1 \rightarrow (a = 1, b = 2)}\]

Vergleich und Diskussion

• Small-Step Semantik:
  • Vorteile:
    • Ermöglicht eine präzise Kontrolle und Verfolgung der Zwischenschritte.
    • Geeignet für die Analyse und Fehlersuche, da jeder Teilschritt sichtbar ist.
  • Nachteile:
    • Kann bei komplexen Programmen unübersichtlich werden, da viele kleine Schritte verfolgt werden müssen.
• Big-Step Semantik:
  • Vorteile:
    • Bietet eine übersichtliche und fokussierte Darstellung des Endergebnisses.
    • Geeignet für die schnelle Überprüfung der korrekten Auswertung.
  • Nachteile:
    • Verbirgt die Zwischenschritte und bietet weniger Unterstützung für die detaillierte Analyse und Fehlersuche.

Zusammengefasst haben beide Semantiken ihre spezifischen Vorteile und Anwendungsfälle. Die Wahl zwischen Big-Step und Small-Step Semantik hängt von den Anforderungen an die Präzision der Analyse und die Übersichtlichkeit der Darstellung ab.

Aufgabe 3)

In der denotationalen Semantik ist die Fixpunkt-Theorie eine Methode zur Definition und Analyse von semantischen Interpretationen durch Fixpunkte von Funktionen in vollständigen Verbänden. Dieses Konzept ist zentral, um die Bedeutung rekursiver Definitionen richtig zu erfassen. Ein vollständiger Verband ist eine Struktur, in der jedes nicht-leere Teilsystem eine untere Schranke und ein Supremum hat.

Zu den wichtigen Aspekten der Fixpunkt-Theorie gehören unter anderem:

• Der vollständige Verband: Eine Struktur, in der jedes nicht-leere Teilsystem eine untere Schranke und ein Supremum hat.
• Fixpunkt-Gleichung: Für eine Funktion f gilt x = f(x), wobei x ein Fixpunkt ist.
• Kleiner Fixpunktsatz von Kleene: Dieser besagt, dass monotone Funktionen auf vollständigen Verbänden ihren kleinsten Fixpunkt haben, gegeben durch \(\bigsqcup_{n \geq 0} f^n(\bot)\).
• Anwendung: Die Fixpunkt-Theorie wird verwendet, um die Bedeutung rekursiver Programme zu bestimmen und deren korrekte Interpretation im Modell eines Programms zu ermöglichen.

a)

Gegeben sei ein vollständiger Verband (L, ≤) und eine monotone Funktion f: L → L. Zeige anhand des kleinen Fixpunktsatzes von Kleene, dass diese Funktion ihren kleinsten Fixpunkt hat. Berechne explizit den kleinsten Fixpunkt für die Funktion f(x) = x + 1, wobei die Grundmenge L = ℕ ∪ {∞} ist und ∞ + 1 = ∞ gilt.

Lösung:

Um den kleinen Fixpunktsatz von Kleene anzuwenden und zu zeigen, dass eine monotone Funktion f: L → L ihren kleinsten Fixpunkt hat, gehen wir schrittweise vor. Außerdem berechnen wir den kleinsten Fixpunkt der Funktion f(x) = x + 1 in der Menge L = ℕ ∪ {∞}.

• Definiere den vollständigen Verband (L, ≤):
  • Die Menge L = ℕ ∪ {∞} repräsentiert die natürlichen Zahlen ergänzt um ein zusätzliches Element ∞.
  • Die Ordnungsrelation ≤ ist die übliche Ordnungsrelation auf den natürlichen Zahlen, erweitert durch die Bedingung, dass jede natürliche Zahl kleiner als ∞ ist, d.h., für alle x ∈ ℕ gilt x ≤ ∞.

• Zeige, dass f(x) = x + 1 eine monotone Funktion ist: Eine Funktion f: L → L ist monoton, wenn für alle x ≤ y gilt f(x) ≤ f(y). Da für die Funktion f(x) = x + 1 gilt:
  • Wenn x ≤ y, dann ist x + 1 ≤ y + 1.
  • Da ∞ hierbei ein spezielles Verhalten hat, gilt ebenfalls ∞ + 1 = ∞, was immer noch ≥ x + 1 für alle x ∈ ℕ ist.
  Dies zeigt, dass f monoton ist.

• Finde den kleinsten Fixpunkt gemäß des kleinen Fixpunktsatzes von Kleene:Der kleine Fixpunktsatz von Kleene besagt, dass jede monotone Funktion auf einem vollständigen Verband ihren kleinsten Fixpunkt hat, und dieser ist gegeben durch:
  • \[\bigsqcup_{n \geq 0} f^n(\bot)\]
  Da der minimale Wert in L (⊥) = 0 ist, berechnen wir die Iterationen von f:
  • f^0(0) = 0
  • f^1(0) = f(0) = 0 + 1 = 1
  • f^2(0) = f(f(0)) = f(1) = 1 + 1 = 2
  • Allgemein gilt f^n(0) = n für jede natürliche Zahl n.
  Da f immer um 1 inkrementiert und ∞ + 1 = ∞ ist, gibt es keinen natürlichen Fixpunkt außer ∞. Folglich ist der kleinste Fixpunkt der Funktion f(x) = x + 1 in L definiert als ∞:

• Folgerung: Der kleinste Fixpunkt von f(x) = x + 1 in der Menge L = ℕ ∪ {∞} ist ∞, da jede natürliche Zahl durch fortgesetztes Anwenden von f zu ∞ führen wird.

• Zusammenfassend:
  • Die Funktion f(x) = x + 1 ist monoton und hat, gemäß des kleinen Fixpunktsatzes von Kleene, ihren kleinsten Fixpunkt in der Menge L = ℕ ∪ {∞}.
  • Dieser kleinste Fixpunkt ist ∞

b)

Betrachte die rekursive Funktion g(n) = n * g(n-1) mit der Basisbedingung g(0) = 1. Verwende die Fixpunkt-Theorie, um den Fixpunkt dieser Funktion zu bestimmen. Beweise, dass der kleinste Fixpunkt g(n) die Fakultät n! ist.

Lösung:

Um den Fixpunkt der rekursiven Funktion g(n) = n * g(n-1) mit der Basisbedingung g(0) = 1 unter Anwendung der Fixpunkt-Theorie zu bestimmen, gehen wir wie folgt vor:

• Definiere die rekursive Funktion und die Basisbedingung:
  • Die Funktion g ist rekursiv definiert als:
  • g(0) = 1
  • g(n) = n * g(n-1) für n > 0

• Formuliere g als einen Fixpunkt einer Funktion f: Wir können g als den Fixpunkt einer Funktion f betrachten, die auf Funktionen selbst operiert. Sei F die Funktion, die eine Funktion h auf eine neue Funktion F(h) abbildet, wobei:
• F(h)(0) = 1
• F(h)(n) = n * h(n-1) für n > 0
Das bedeutet, dass g der Fixpunkt von F ist, wenn F(g) = g gilt.

• Zeige, dass g(n) die Fakultät n! ist: Wir beweisen dies durch vollständige Induktion:
• Induktionsanfang: Für n = 0 gilt:
• g(0) = 1
• Dies entspricht der Definition von 0!, da 0! = 1.
• Induktionsvoraussetzung: Angenommen, g(k) = k! gilt für ein beliebiges aber festes k ≥ 0.
• Induktionsschritt: Es ist zu zeigen, dass g(k+1) = (k+1)! gilt.
• Nach Definition von g haben wir:
• g(k+1) = (k+1) * g(k)
• Nach Induktionsvoraussetzung setzen wir g(k) = k! ein:
• g(k+1) = (k+1) * k!
• Dies entspricht der Definition von (k+1)!, da (k+1)! = (k+1) * k!.
• Damit haben wir gezeigt, dass g(n) = n! für alle natürlichen Zahlen n gilt.

• Zusammenfassung:
  • Die rekursive Definition der Funktion g(n) = n * g(n-1) mit der Basisbedingung g(0) = 1 entspricht der Fakultät n!.
  • Wir haben bewiesen, dass der kleinste Fixpunkt dieser Funktion durch die Fakultät n! gegeben ist.
  • Das bedeutet, dass g(n) die Fakultät n! ist.

Aufgabe 4)

Kontext: Angenommen, Du hast ein einfaches Programm mit einer Schleife und möchtest mit Hilfe der Hoare-Logik die partielle Korrektheit des Programms nachweisen. Das folgende Programm berechnet die Summe der ersten n natürlichen Zahlen. Vorbedingung ist, dass n eine nicht-negative ganze Zahl ist.

  sum := 0; i := 1; while (i <= n) do  sum := sum + i; i := i + 1 

Die Nachbedingung ist, dass sum den Wert \(\frac{n(n+1)}{2}\) enthält.Verwende Hoare-Logik, um die Korrektheit dieses Programms nachzuweisen.

a)

Identifiziere geeignete Schleifeninvarianten für die angegebenen Schleifenbedingung und erkläre, warum diese Invarianten korrekt sind.

Lösung:

Schleifeninvariante:Um die Korrektheit des Programms mit Hilfe der Hoare-Logik nachzuweisen, müssen wir eine geeignete Schleifeninvariante finden. Eine Schleifeninvariante ist eine Bedingung, die zu Beginn und am Ende jeder Iteration der Schleife wahr ist, und die helfen kann, die Korrektheit des Programms zu beweisen.Schauen wir uns das Programm und die Vor- und Nachbedingungen an:

 sum := 0; i := 1; while (i <= n) do  sum := sum + i;  i := i + 1

Die Vorbedingung ist, dass n eine nicht-negative ganze Zahl (n ≥ 0) ist.Die Nachbedingung ist, dass sum den Wert \(\frac{n(n+1)}{2}\) enthält.Eine geeignete Schleifeninvariante für diesen Fall könnte wie folgt aussehen:

• Schleifeninvariante: sum ist die Summe der ersten i-1 natürlichen Zahlen, also gilt: sum = \(\frac{(i-1)i}{2}\).

Diese Invariante ist korrekt, weil:

• Anfangszustand: Bevor die Schleife beginnt, haben wir sum := 0 und i := 1. Zu diesem Zeitpunkt ist sum = \frac{(1-1)1}{2} = 0, was mit der Invariante übereinstimmt.
• Schleifenbedingung: Während der Schleife wird sum := sum + i und i := i + 1 ausgeführt. Nach der Ausführung von sum := sum + i wird sum die Summe der ersten i natürlichen Zahlen sein. Dann erhöhen wir i um 1, sodass die Invariante sum = \frac{(i-1)i}{2} für den nächsten Durchlauf wieder gilt.
• Endzustand: Wenn die Schleife beendet ist, ist i gleich n+1. Zu diesem Zeitpunkt haben wir sum als die Summe der ersten n natürlichen Zahlen, also: sum = \frac{(n)(n+1)}{2}, was der Nachbedingung entspricht.

Zusammenfassend können wir sehen, dass die Schleifeninvariante sum = \frac{(i-1)i}{2} während jeder Iteration der Schleife korrekt ist und am Ende der Schleife die gewünschte Nachbedingung erfüllt ist.

b)

Beweise formal unter Verwendung der Hoare-Logik, dass das gegebene Programm korrekt ist, indem Du das entsprechende Hoare-Tripel für das Programm aufstellst und die Korrektheit durch Anwendung der Inferenzregeln und Axiome zeigst. Dabei musst Du insbesondere nachweisen, dass die identifizierte Schleifeninvariante die gesamte Schleife erfüllt.

Lösung:

Formaler Beweis der Korrektheit des Programms unter Verwendung der Hoare-Logik:Um die partielle Korrektheit des Programms zu beweisen, verwenden wir Hoare-Tripel und zeigen, dass die Schleifeninvariante während der gesamten Schleifenlaufzeit erfüllt ist. Wir haben bereits eine geeignete Schleifeninvariante identifiziert:

• Schleifeninvariante: sum ist die Summe der ersten i-1 natürlichen Zahlen, also gilt: \(\text{sum} = \frac{(i-1)i}{2}\).

Nun stellen wir das Hoare-Tripel für das Programm auf:

 {P} sum := 0; i := 1; while (i <= n) do  sum := sum + i; i := i + 1 {Q} 

• Vorbedingung (P): \(n \geq 0\)
• Nachbedingung (Q): \(\text{sum} = \frac{n(n+1)}{2}\)

Zuerst betrachten wir die Vorbereitungssequenz vor der Schleife:

 {P} sum := 0; i := 1 {I} 

Hier ist

• Invariante (I): \(\text{sum} = \frac{(i-1)i}{2}\)

Wir überprüfen, ob {P} die Invariante (I) zu Beginn erfüllt:

• Nach \(\text{sum := 0}\) und \(\text{i := 1}\) haben wir \(\text{sum} = \frac{(1-1)1}{2} = 0\), was wahr ist.

Nun betrachten wir die Schleifenbedingung:

 {I \text{ and } i \leq n}   sum := sum + i; i := i + 1   {I} 

Wir müssen zeigen, dass die Invariante nach jeder Iteration erhalten bleibt.

• Vor der Iteration: \(I: \text{sum} = \frac{(i-1)i}{2}\)
• Schleifenbedingung: \(i \leq n\)

Nach der Iteration:

• \(\text{sum} := \text{sum} + i\)
• \(\text{sum} = \frac{(i-1)i}{2} + i = \frac{(i-1)i + 2i}{2} = \frac{i^2 - i + 2i}{2} = \frac{i^2 + i}{2} = \frac{i(i+1)}{2}\)
• \(\text{i := i + 1}\)

Wir müssen überprüfen:

• \(\text{sum} = \frac{i(i+1)}{2}\) muss nach der Iteration wahr sein.

Da die Gleichung \(\frac{(i-1)i}{2} + i\) nach der Erhöhung von \(\text{i}\) zur nächsten Invariante führt, bleibt die Invariante \(\text{sum} = \frac{(i-1)i}{2}\) gültig.Nun betrachten wir den Endzustand, wenn die Schleifenbedingung \(i > n\) wird:

• Wenn \(i = n+1\), dann \(\text{sum} = \frac{(n+1 - 1)(n+1)}{2} = \frac{n(n+1)}{2}\), was der Nachbedingung entspricht.

Damit haben wir den Beweis der Korrektheit des Programms erbracht.