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

Charakterisierung des reflexiven, symmetrischen und transitiven

Abschlusses einer Relation mittels Zickzacks

Der reflexive, symmetrische und transitive Abschluss (im folgenden kurz Abschluss) einer Relation R ist die kleinste Relation, die R enthält und reflexiv, symmetrisch und transitiv ist. Den Abschluss kann man wie folgt konstruieren:

Ein Zickzack in einer Relation R ist eine endliche Folge x_{1}, x_{2}, …, x_{n} mit wenigstens einem Element, so dass x_{i} R x_{i+1} oder x_{i+1} R x_{i} gilt (für i < n). Zwei Elemente x und y sind im Abschluss genau dann in Relation gesetzt, wenn es einen Zickzack von x nach y gibt.

Aufgabe

1. Formalisieren Sie die Zickzackkonstruktion in Pvs.

2. Beweisen Sie, dass man so tatsächlich den Abschluss einer beliebigen Relation erhält.