Subtyping von regulären Typen

Für eine Subtyp-Relation auf reguläre Typen soll das Ersetzbarkeits-Prinzip von Wegner und Zdonik gelten:

Eine Instanz eines Subtyps kann überall dort verwendet werden, wo eine Instanz des Supertyps erwartet wird.

Um eine entsprechende Relation zu formulieren sind einige formale Schreibweisen und Begriffe notwendig.

Wenn ein Objekt im Zustand $x$ eine Anfrage $r$ akzeptieren kann und es sich anschließend im Zustand $x'$ befindet, läßt sich dies schreiben als

$$x\overset {r}{\to }x'$$

Hierbei handelt es sich im Allgemeinen nicht um eine Funktion, da das Objekt bei der Bearbeitung der Anfrage $r$ selbst Anfragen an andere Objekte senden kann, wodurch der Zustandsübergang auf das Objekt bezogen nichtdeterministisch erscheint.

Kann ein Objekt im Zustand $x$ eine Folge von Anfragen $s$ verarbeiten und befindet es sich anschließend im Zustand $x'$, soll dies ausgedrückt werden durch

$$x\overset {s}{\Rightarrow }x'$$

Definition 1: Das Protokoll eines Objektes im Zustand $x$ ist gegeben durch die Menge von Folgen von Anfragen, die es bedienen kann:

$$traces(x):=\{s\mid \exists x',x\overset {s}{\Rightarrow }x'\}$$

Eine weitere wichtige Menge ist die der im Zustand $x$ zulässigen Anfragen.

Definition 2: $init(x):=\{r\mid \exists x',x\overset {r}{\to }x'\}$.

Jetzt können wir die Menge der Fehlersituationen eines Protokolls definieren.

Definition 3:

$$failures(x):=\{(s,R)\mid \exists x',x\overset {s}{\Rightarrow }x',R\, ist\, endlich,R\cap init(x')=\emptyset \}$$

Wollen wir nun ein Objekt im Zustand $x$ für ein Objekt im Zustand $y$ einsetzen, muss sicher gelten, dass $traces(y)\subseteq traces(x)$ gilt, also alle Folgen von Anfragen, die $y$ akzeptiert, auch von $x$ akzeptiert werden. Für die Fehlersituationen muss sicher das Umgekehrte gelten, d. h. ein Fehler $(s,R)$ der für $x$ auftritt muss auch für $y$ möglich sein oder aber $s$ muss außerhalb des Protokolls von $y$ liegen.

Definition 4: Die relativen Fehlersituationen eines Objektes im Zustand $x$ bzgl. eines Objektes im Zustand $y$ sind:

$$failures_{y}(x):=\{(s,R)\in failures(x)\mid s\in traces(y)\}$$

Damit lautet dann die Definition der Einsetzbarkeits-Relation

Definition 5: Ein Objekt im Zustand $x$ ist für ein Objekt im Zustand $y$ einsetzbar, geschrieben $x:<y$, genau dann, wenn gilt: $traces(y)\subseteq traces(x)$ und $failures_{y}(x)\subseteq failures(y)$.

Es lässt sich zeigen, dass diese Einsetzbarkeits-Relation die Eigenschaften einer Halbordnung hat, also reflexiv und transitiv ist.

$x$ soll jetzt ein Subtyp von $y$ sein, genau dann, wenn gilt $x:<y$. Für den regulären Typ $Var$ einer Variablen gilt dann $Var:<Buf$, also ist $Var$ ein Subtyp von $Buf$.

Das Protokoll eines Objektes $x$ soll konform zum Protokoll eines Objektes $y$ heißen, wenn $x$ ein Subtyp von $y$ ist. Liegen die Protokolle der beiden Objekte als reguläre Typen vor, gibt es einen Algorithmus um die Konformität zu testen.