Angewandte Softwareverifikation mit einem interaktiven Theorembeweiser Version 28. März 2011

Endliche Mengen: Externe Charakterisierung

Eine algebraische Spezifikation für endliche Mengen enthält eine Konstante nil : set und eine Operation add : set × A ⟶ set für die die folgenden Axiome gelten:

∀s ∈ set, a ∈ A . add(add(s, a), a) = add(s, a)
∀s ∈ set, a, b ∈ A . add(add(s, a), b) = add(add(s, b), a)

Ein Modell dieser Spezifikation besteht aus einer Grundmenge X (der Menge aller endlichen Mengen) und entsprechenden Operationen nil_{X} und add_{X}, die die Axiome erfüllen.

Eine Funktion f : X ⟶ Y zwischen den Grundmengen zweier Modelle heißt Mengenhomomorphismus, falls

f(nil_{X}) = nil_{Y}
∀s ∈ X, a ∈ A . f(add(s, a)) = add(fs, a)

Ein Modell X ist initial, wenn es genau einen Mengenhomomorphismus zu jedem anderen Modell gibt (insbesondere gibt es auch nur einen Homomorphismus X ⟶ X).

Aufgabe

1. Formalisieren Sie die Begriffe des Modells (der Spezifikation endlicher Mengen), des Mengenhomomorphismus und des initialen Modells in PVS.

2. Beweisen Sie, dass das initiale Modell isomorph zu den in PVS definierten endlichen Mengen ist.

Detaillierte Hinweise

• Es ist zweckmäßig, für die Operationen eines Modells in PVS einen Recordtyp zu definieren. Dabei sind sowohl die Grundmenge als auch das Alphabet A Typparameter.

• Die Axiome können dann als Prädikat auf dem Operationenrecord formuliert werden.

• Die Mengenhomomorphismen definiert man am besten als Prädikat über dem Funktionsraum X ⟶ Y. Dafür braucht man natürlich drei Typparameter.

• Mit diesem Ansatz kann Initialität in PVS nicht formalisiert werden (weil man nicht über Typen quantifizieren kann). Es ist jedoch ausreichend, Initialität in Bezug auf eine (parametrische) Grundmenge zu definieren. Dafür braucht man drei Typparameter (Grundmenge X, Y und Alphabet A). Initialität wird dann als Prädikat über den Operationenrecords mit Grundmenge X definiert: Ein Operationenrecord a ist in diesem Prädikat, falls es für alle Operationenrecords b mit Grundmenge Y genau einen Mengenhomomorphismus gibt.