Praktische Semantik von Programmiersprachen - Exam

Aufgabe 1)

Gegeben seien die folgenden Funktionen und mathematischen Ausdrücke zur Verdeutlichung der Small-Step- und Big-Step-Semantik. Die Small-Step-Semantik zerlegt die Ausführung eines Programms in viele kleine Schritte, während die Big-Step-Semantik die Ausführung als einen großen Schritt beschreibt. Angenommen wir haben die Sprache mit folgenden Ausdrücken:

• Expressionen: Konstanten, Variable und einfache arithmetische Operationen wie Addition oder Multiplikation.
• Zuweisungen: x := e - ordnet einer Variablen x den Wert des Ausdrucks e zu.
• Sequenzen: S1; S2 - führt zuerst S1, dann S2 aus.

• Small-Step-Relationen:

    e1 + e2 -> v1 + e2, wenn e1 -> v1   v1 + e2 -> v1 + v2, wenn e2 -> v2   v1 + v2 -> v3, wobei v3 = v1 + v2

• Big-Step-Relationen:

    e1 + e2 ↓ v1 + v2, wobei v1 und v2 die ausgewerteten Werte von e1 und e2 sind

a)

1. Betrachte die folgende arithmetische Operation in der Sprache:

3 + (2 * 4)

Lösung:

Um die arithmetische Operation 3 + (2 * 4) mithilfe der Small-Step-Semantik schrittweise auszuwerten, folgen wir den definierten Übergangsrelationen. Wir zerlegen den Ausdruck in viele kleine Schritte, bis wir den endgültigen Wert erhalten. Hier sind die Schritte:

• Ausgangsausdruck:

  3 + (2 * 4)

• Wir müssen zuerst die Multiplikation auswerten, da dies eine innere Berechnung ist:

  2 * 4 -> 8

• Der Ausdruck wird dann zu:

  3 + 8

• Nun werten wir die Addition aus:

  3 + 8 -> 11

• Endgültiger Wert:

  11

Die Übergangsrelationen sind wie folgt:

• (3 + (2 * 4)) -> (3 + 8)

• (3 + 8) -> 11

Zusammengefasst haben wir durch die Small-Step-Semantik die Auswertung von 3 + (2 * 4) schrittweise dokumentiert und den Endwert 11 erhalten.

b)

2. Verwende nun die Big-Step-Semantik, um denselben Ausdruck 3 + (2 * 4) zu evaluieren. Zeige die einzelnen Schritte mit Hilfe der Bewertungsrelationen und dokumentiere das Endergebnis. Erkläre, wie sich dieser Ansatz von der Small-Step-Semantik unterscheidet und warum er möglicherweise intuitiver sein kann.

Lösung:

Um den Ausdruck 3 + (2 * 4) mithilfe der Big-Step-Semantik zu evaluieren, betrachten wir die Bewertung des gesamten Ausdrucks in einem großen Schritt. Die Bewertungsrelationen sind hierbei entscheidend. Gehen wir die Schritte durch:

• Ausgangsausdruck: 3 + (2 * 4)
• Hierbei müssen wir zuerst die inneren Ausdrücke 3 und 2 * 4 bewerten.
• Die Konstanten 3 sind bereits vollständig bewertet:

  3 ↓ 3

• Wir bewerten die Multiplikation:

  2 * 4 ↓ 8

• Der ursprüngliche Ausdruck wird dann zu: 3 + 8
• Wir bewerten die Addition:

  3 + 8 ↓ 11

• Endergebnis:

  11

Zusammengefasst:

• Bewertung einzelner Terme:

  3 ↓ 3

  und

  2 * 4 ↓ 8

• Zusammensetzung:

  3 + (2 * 4) ↓ 11

Erklärung des Ansatzes und Unterschied zur Small-Step-Semantik:

• Die Small-Step-Semantik zerlegt die Auswertung in viele kleine Schritte und berücksichtigt dabei kontinuierlich die Übergangsrelationen des Systems. Sie eignet sich gut für die Darstellung der exakten Ausführungsreihenfolge in einer imperativen Sprache.
• Die Big-Step-Semantik beschreibt die Auswertung eines Ausdrucks in einem großen Schritt, indem sie die Endbewertung der inneren Ausdrücke kombiniert. Sie bietet eine klarere und umfassendere Sicht auf die gesamte Bewertung, was oft intuitiver und übersichtlicher ist, insbesondere bei einfachen arithmetischen Ausdrücken.

Aufgabe 2)

In einem Programmierkontext können wir zwischen deterministischer und nicht-deterministischer Semantik unterscheiden. Die deterministische Semantik liefert für jede bestimmte Eingabe exakt ein definiertes Ergebnis, während die nicht-deterministische Semantik für dieselbe Eingabe unterschiedliche mögliche Ergebnisse liefern kann. Diese Konzepte haben erhebliche Auswirkungen auf das Verhalten von Programmen und deren Vorhersagbarkeit.

a)

Schreibe eine Funktion in Python, die deterministische Semantik aufweist und das Maximum einer Liste von Zahlen findet. Erkläre, warum diese Funktion deterministisch ist.

 def find_max(numbers):     if not numbers:         return None     max_number = numbers[0]     for num in numbers:         if num > max_number:             max_number = num     return max_number 

Lösung:

Um eine Funktion in Python zu schreiben, die deterministische Semantik aufweist und das Maximum einer Liste von Zahlen findet, können wir die folgende Funktion implementieren:

def find_max(numbers):    if not numbers:        return None    max_number = numbers[0]    for num in numbers:        if num > max_number:            max_number = num    return max_number

Warum diese Funktion deterministisch ist:

• Deterministischer Algorithmus: Die Funktion find_max folgt einem deterministischen Algorithmus. Dies bedeutet, dass sie den gleichen Ablauf und die gleichen Operationen in derselben Reihenfolge ausführt, unabhängig davon, wie oft sie aufgerufen wird.
• Eindeutige Ergebnisse: Für eine gegebene Eingabeliste von Zahlen liefert die Funktion immer denselben Ausgangswert (das Maximum der Liste). Es gibt keine Zufallselemente oder unvorhersehbare Bedingungen im Code.
• Keine seitlichen Effekte: Die Funktion verändert keine externen Zustände oder Variablen. Sie arbeitet nur mit den ihr übergebenen Argumenten und gibt ein klares Ergebnis zurück, ohne äußere Einflüsse beachten zu müssen.
• Endliche Schleife: Die Schleife in der Funktion läuft über alle Elemente der Liste und beendet sich nach einer bestimmten Anzahl von Durchläufen (nämlich der Länge der Liste). Es gibt keine Möglichkeit, dass die Schleife unendlich läuft oder eine variable Anzahl von Durchläufen hat.

Zusammenfassend lässt sich sagen, dass die Funktion find_max für jede gegebene Eingabe von Zahlen immer ein vorhersehbares und eindeutiges Ergebnis liefert, weshalb sie als deterministisch bezeichnet werden kann.

b)

Angenommen, Du hast eine nicht-deterministische Funktion, die eine Zahl zwischen 1 und 10 zurückgibt. Beschreibe zwei potenzielle Szenarien, wie solch eine Funktion in einem Algorithmus verwendet werden könnte und welche Auswirkungen die nicht-deterministische Semantik auf das Gesamtsystem hätte.

Lösung:

Eine nicht-deterministische Funktion, die eine Zahl zwischen 1 und 10 zurückgibt, könnte unterschiedliche Auswirkungen auf ein System haben, abhängig davon, wie sie verwendet wird. Hier sind zwei potenzielle Szenarien:

• Szenario 1: Zufällige Auswahl in einem SpielAngenommen, die nicht-deterministische Funktion wird verwendet, um eine zufällige Zahl zu generieren, die bestimmt, wie viele Schritte ein Spieler in einem Brettspiel vorwärts ziehen kann. Jedes Mal, wenn der Spieler an der Reihe ist, wird eine Zahl zwischen 1 und 10 ausgewählt.In diesem Fall:
• Vielfalt im Spiel: Die nicht-deterministische Funktion sorgt für Abwechslung und Unvorhersehbarkeit, was das Spiel interessanter und spannender macht.
• Unvorhersehbarer Verlauf: Der Fortschritt der Spieler ist nicht vorhersehbar, was bedeutet, dass keine zwei Spielrunden identisch verlaufen. Dies erhöht den Wiederspielwert.
• Szenario 2: Verwendung in einem SicherheitskontextAngenommen, die nicht-deterministische Funktion wird verwendet, um eine zufällige Verzögerung in einem sicherheitskritischen System einzubauen, um Timing-Angriffe (wie Seitenkanalangriffe) zu verhindern. Die Funktion wird aufgerufen, um eine Zahl zwischen 1 und 10 zu generieren, die dann als Verzögerung in Millisekunden hinzugefügt wird, bevor eine sicherheitsrelevante Aktion ausgeführt wird.In diesem Fall:
• Sicherheitsverbesserung: Die nicht-deterministische Verzögerung macht es für Angreifer schwieriger, genaue Timing-Informationen zu sammeln, da die Zeit, die die Aktion benötigt, jedes Mal variiert. Dies kann helfen, Timing-Angriffe zu verhindern.
• Unvorhersehbare Leistung: Die Gesamtleistung des Systems kann variieren, da einige Aktionen aufgrund der zufälligen Verzögerungen länger dauern können. Dies kann zu unvorhersehbarem Verhalten führen und die durchschnittliche Reaktionszeit des Systems erhöhen.

Auswirkungen der nicht-deterministischen Semantik auf das Gesamtsystem:

• Vorteile: Nicht-deterministische Funktionen können in vielen Szenarien nützlich sein, indem sie Vielfalt, Unvorhersehbarkeit und erhöhte Sicherheit bieten.
• Nachteile: Nicht-deterministische Funktionen können es schwieriger machen, das Verhalten eines Systems vorherzusagen und zu testen. Sie können auch zu inkonsistenten Ergebnissen führen, was besonders in sicherheitskritischen oder leistungsabhängigen Anwendungen problematisch sein kann.

Insgesamt muss die Verwendung von nicht-deterministischen Funktionen sorgfältig abgewogen werden, um sicherzustellen, dass die Vorteile die potenziellen Nachteile überwiegen.

Aufgabe 3)

Gegeben sei das Lambda-Kalkül, ein formales System zur Untersuchung von Funktionen und deren Anwendungen. Dabei sind Kernbestandteile der funktionalen Programmierung wie die Abstraktion von Funktionen, z.B. \(\lambda x. x+1\), sowie die Applikation von Funktionen, z.B. \((\lambda x. x+1)2 = 3\). Ebenfalls betrachtet werden die Reduktionen \(\beta\text{-Reduktion}\) und \(\eta\text{-Reduktion}\), sowie die Konzepte freier und gebundener Variablen.

a)

a) Reduktionen im Lambda-Kalkül:Sei folgende Lambda-Ausdruck gegeben: \((\lambda f.\, (\lambda x.\, f\, (x\, x))\,(\lambda x.\, f\, (x\, x)))\, (\lambda y.\, y + 1)\).

• Berechne die vollständige \beta-Reduktion. Zeige alle Zwischenschritte.
• Bestimme den finalen Wert des Ausdrucks.

Lösung:

Aufgabe a) Reduktionen im Lambda-Kalkül:

Gegeben sei der Lambda-Ausdruck:

(\lambda f. (\lambda x. f (x x)) (\lambda x. f (x x))) (\lambda y. y + 1)

Wir berechnen nun die vollständige \(\beta\)-Reduktion Schritt für Schritt und bestimmen den finalen Wert des Ausdrucks.

• Schritt 1: Wenden wir die äußere Funktion auf (\lambda y. y + 1) an:

(\lambda f. (\lambda x. f (x x)) (\lambda x. f (x x))) (\lambda y. y + 1)\rightarrow \lambda x. (\lambda y. y + 1) (x x)) (\lambda x. (\lambda y. y + 1) (x x))

(\lambda x. (\lambda y. y + 1) (x x)) (\lambda x. (\lambda y. y + 1) (x x))\rightarrow (\lambda y. y + 1) ((\lambda x. (\lambda y. y + 1) (x x)) (\lambda x. (\lambda y. y + 1) (x x)))

(\lambda y. y + 1) ((\lambda x. (\lambda y. y + 1) (x x)) (\lambda x. (\lambda y. y + 1) (x x)))

(\lambda x. (\lambda y. y + 1) (x x)) (\lambda x. (\lambda y. y + 1) (x x)) \rightarrow (\lambda y. y + 1)

Finaler Wert des Ausdrucks: (\lambda y. y + 1)

• Der finale Wert ist also eine Funktion, die ihren Eingabewert um 1 erhöht. Der komplette Ausdruck wurde in eine Funktion reduziert, die wie folgt aussieht: (\lambda y. y + 1)

b)

b) Freie und gebundene Variablen:Betrachte den Lambda-Ausdruck \(\lambda x.\, (x\, y)\, (\lambda y.\, x\, z)\).

• Identifiziere alle freien und gebundenen Variablen im Ausdruck.
• Gib die Menge der freien Variablen an und erkläre dein Vorgehen.

Lösung:

Aufgabe b) Freie und gebundene Variablen:

Betrachte den Lambda-Ausdruck:

\(\lambda x. (x\, y) (\lambda y. x\, z)\)

Wir identifizieren nun alle freien und gebundenen Variablen im Ausdruck und geben die Menge der freien Variablen an.

• Freie Variablen: Variablen, die nicht innerhalb einer Lambda-Abstraktion eingeführt werden, d.h. sie haben keine \(\backslash\)-Bindung zu ihrer linken Seite.
• Gebundene Variablen: Variablen, die innerhalb einer Lambda-Abstraktion eingeführt werden, d.h. sie haben eine \(\backslash\)-Bindung zu ihrer linken Seite.

Analysieren wir den Ausdruck Schritt für Schritt:

• Der äußerste Lambda-Ausdruck:

\(\lambda x. (x\, y) (\lambda y. x\, z)\)Hier wird die Variable x gebunden.

(x\, y)

(\lambda y. x\, z)

Im Gesamtausdruck sind folgende Variablen:

• Gebundene Variablen: x, y (innerhalb der zweiten Abstraktion)
• Freie Variablen: y, z

Die Menge der freien Variablen ist:

{y, z}

Vorgehen:

• Identifiziere alle Lambda-Abstraktionen und notiere die gebundenen Variablen.
• Analysiere den restlichen Ausdruck und identifiziere die Variablen, die nicht innerhalb einer Lambda-Abstraktion gebunden sind.
• Die übrigen, nicht gebundenen Variablen sind die freien Variablen.

Aufgabe 4)

Betrachten wir ein einfaches Programm zur Berechnung des Maximums von zwei Variablen. Das Programm liest zwei Ganzzahlen a und b ein und schreibt das Maximum der beiden in max.

if (a >= b) {    max = a;} else {    max = b;}

a)

Verwende die Methode der Hoare-Logik, um die totale Korrektheit dieses Programms zu beweisen. Gib eine Vorbedingung P, eine Nachbedingung Q und die entsprechenden Hoare-Dreier für die Sequenzen an.

Lösung:

Um die totale Korrektheit des gegebenen Programms mittels Hoare-Logik zu beweisen, müssen wir geeignete Vor- und Nachbedingungen definieren und die jeweiligen Hoare-Dreier formulieren.

• Vorbedingung (P): Die Vorbedingung beschreibt den Zustand vor der Ausführung des Programms. Da das Programm zwei Ganzzahlen a und b einliest und das Maximum dieser beiden berechnet, können wir folgende Vorbedingung formulieren:

P: wahr
• Diese Vorbedingung ist immer wahr, da keine speziellen Annahmen über a und b gemacht werden müssen.

• Nachbedingung (Q): Die Nachbedingung beschreibt den Zustand nach der Ausführung des Programms. Das Programm soll sicherstellen, dass max das Maximum von a und b enthält. Die Nachbedingung lautet daher:
• Q: max = max(a, b)

• Hoare-Dreier: Für die beiden möglichen Sequenzen im Programm müssen wir die entsprechenden Hoare-Dreier formulieren.

• 1. Bedingung 'if (a >= b)':
{P ∧ (a >= b)} max = a {Q}{wahr ∧ (a >= b)} max = a {max = max(a, b)}

• 2. Bedingung 'else':
{P ∧ (a < b)} max = b {Q}{wahr ∧ (a < b)} max = b {max = max(a, b)}

• Da 'wahr ∧ (a >= b)' und 'wahr ∧ (a < b)' immer gültig sind, ergeben sich folgende Hoare-Dreier für die gesamte Sequenz:

{wahr} if (a >= b) { max = a; } else { max = b; } {max = max(a, b)}

Damit haben wir bewiesen, dass das gegebene Programm korrekt arbeitet und nach der Ausführung die erwartete Nachbedingung erfüllt.

b)

Erweitere das Programm so, dass das Maximum von drei Variablen a, b und c bestimmt wird. Schreibe das erweiterte Programm auf und zeige mittels Hoare-Logik, dass dieses Programm korrekt ist. Gib wieder die Vorbedingung P, die Nachbedingung Q und die entsprechenden Hoare-Dreier an.

Lösung:

Um das gegebene Programm zu erweitern, damit es das Maximum von drei Variablen a, b und c bestimmt, muss der Code modifiziert werden. Hier ist das erweiterte Programm:

if (a >= b) {    if (a >= c) {        max = a;    } else {        max = c;    }} else {    if (b >= c) {        max = b;    } else {        max = c;    }}

Als nächstes demonstrieren wir mittels Hoare-Logik, dass dieses Programm korrekt ist.

• Vorbedingung (P): Da keine speziellen Annahmen über a, b und c gemacht werden müssen, lautet die Vorbedingung:

P: wahr

• Nachbedingung (Q): Das Programm soll sicherstellen, dass max das Maximum der Werte a, b und c enthält:
Q: max = max(a, b, c)

• Hoare-Dreier: Wir müssen die Hoare-Dreier für die verschiedenen Sequenzen im Programm formulieren:

• 1. Bedingung 'if (a >= b)':
{P ∧ (a >= b)}if (a >= c) { max = a; } else { max = c; }{Q}{wahr ∧ (a >= b)}if (a >= c) { max = a; } else { max = c; }{max = max(a, b, c)}
• 1.1. Bedingung 'if (a >= c)':
{P ∧ (a >= b) ∧ (a >= c)}max = a{Q}{wahr ∧ (a >= b) ∧ (a >= c)}max = a{max = max(a, b, c)}
• 1.2. Bedingung 'else (a < c)':
{P ∧ (a >= b) ∧ (a < c)}max = c{Q}{wahr ∧ (a >= b) ∧ (a < c)}max = c{max = max(a, b, c)}
• 2. Bedingung 'else (a < b)':
{P ∧ (a < b)}if (b >= c) { max = b; } else { max = c; }{Q}{wahr ∧ (a < b)}if (b >= c) { max = b; } else { max = c; }{max = max(a, b, c)}
• 2.1. Bedingung 'if (b >= c)':
{P ∧ (a < b) ∧ (b >= c)}max = b{Q}{wahr ∧ (a < b) ∧ (b >= c)}max = b{max = max(a, b, c)}
• 2.2. Bedingung 'else (b < c)':
{P ∧ (a < b) ∧ (b < c)}max = c{Q}{wahr ∧ (a < b) ∧ (b < c)}max = c{max = max(a, b, c)}

Da 'wahr ∧ (a >= b)' und 'wahr ∧ (a < b)' sowie die weiteren Bedingungen immer gültig sind, ergeben sich folgende Hoare-Dreier für die gesamte Sequenz:

{wahr}if (a >= b) { if (a >= c) { max = a; } else { max = c; } } else { if (b >= c) { max = b; } else { max = c; } }{max = max(a, b, c)}

Damit haben wir bewiesen, dass das erweiterte Programm korrekt arbeitet und nach der Ausführung die erwartete Nachbedingung erfüllt.