Übungsaufgaben zur Wiederholung

Aufgabe 1

Formalisieren Sie das Konzept einer Gruppe (G,*,e,inv) in PVS und beweisen Sie:

inv(x*y) = inv(y) * inv(x)

Aufgabe 2

Chris Okasaki beschreibt eine funktionale Implementierung von Rot-Schwarz-Bäumen. In rb_task.pvs finden Sie eine Kodierung der Einfügeoperation in PVS. Zeigen Sie, dass Einfügen folgende Eigenschaft von Rot-Schwarz-Bäumen erhält: Auf jedem Pfad befinden sich gleich viele schwarze Knoten.

Aufgabe 3

Beweisen Sie in Coq:

forall n:nat, n = 0 \/ exists m:nat, n = S m
forall n:nat, 2 * n = n + n

Aufgabe 4

Wir betrachten eine rudimentäre Programmiersprache ADD mit folgender Befehlsgrammatik: 
  n  ::=  natürliche Zahl
  c  ::=  x = n
       |  x = y + z
       |  c ; c'
Dabei sind x,y,z Variablen aus einer Variablenmenge V. Ein Zustand ist eine Abbildung V -> nat von Variablen auf Werte.
  1. Definieren Sie einen induktiven Typen für ADD-Befehle in Coq.
  2. Definieren Sie rekursive eine Funktion exec c s, die Befehle c in einem Zustand s auswertet und den veränderten Zustand zurückgibt.
  3. Beweisen Sie Monotonie für ADD: Wenn s ≤ s', dann exec c s ≤ exec c s'. Dabei ist s ≤ s' falls s x ≤ s' x für alle Variablen x:V.
  4. Definieren Sie induktiv eine Relation: R x c gdw. Variable x kommt in Befehl c vor.