next up previous contents
Nächste Seite: Erfüllung der Erwartungen eines Aufwärts: Verfügbarkeit der Services eines Vorherige Seite: Subtyping von regulären Typen   Inhalt

Algorithmus zum Überprüfen der Subtyp-Relation

Zunächst wird zu dem nichtdeterministischen endlichen Automaten, der durch einen regulären Typ gegeben ist, ein deterministischer endlicher Automat konstruiert, indem Mengen von Zuständen anstelle der einzelnen Zustände betrachtet werden.

Die Definitionen von $ init() $ und $ \rightarrow $ werden dann auf Zustandsmengen erweitert:

$\displaystyle init(X)=\{r\mid \exists x\in X,x',x\overset {r}{\rightarrow }x'\}$

$\displaystyle X\overset {r}{\rightarrow }X':\Leftrightarrow X'=\{x'\mid \exists x\in X,x\overset {r}{\rightarrow }x'\}$

Der folgende Algorithmus überprüft, ob $ x:<y $ gilt

1. falls nicht $ init(y)\subseteq init(x) $, dann FAIL

2. add $ (\{x\},\{y\},init(y)) $ to $ LIST $

3. falls möglich, ein $ (X,Y,R) $ mit $ R\neq \emptyset $ in $ LIST $ auswählen,

sonst SUCCEED

4. ein $ r $ aus $ R $ auswählen

und $ (X,Y,R) $ in $ LIST $ durch $ (X,Y,R\setminus \{r\}) $ ersetzen

5. $ X' $ und $ Y' $ mit $ X\overset {r}{\rightarrow }X' $ und $ Y\overset {r}{\rightarrow }Y' $ berechnen

6. falls $ (X',Y',R') $ mit $ R' $ beliebig bereits in $ LIST $, dann goto 3

7. falls nicht $ init(Y')\subseteq init(X') $, dann FAIL

8. falls nicht $ \forall x\in X' $ $ \exists y\in Y' $: $ init(y)\subseteq init(x) $, dann FAIL

9. add $ (X',Y',init(Y')) $ to $ LIST $

10. goto 3
Die Arbeitsweise dieses Algorithmus soll beispielhaft für die regulären Typen $ NewNDStack $ und $ Buf $ gezeigt werden. Es soll überprüft werden, ob $ NewNDStack:<Buf $ gilt.

\resizebox*{!}{3cm}{\includegraphics{StackBuf.eps}}

Wir beginnen mit $ x=s1 $ und $ y=b1 $, und erhalten die folgende Liste

$ LIST= $ $ (\{s1\},\{b1\},\{put\}) $

\resizebox*{!}{3cm}{\includegraphics{StackBuf1.eps}}

$ \rightarrow $ $ LIST= $ $ (\{s1\},\{b1\},\{\}) $ $ (\{s2\},\{b2\},\{get\}) $

\resizebox*{!}{3cm}{\includegraphics{StackBuf2.eps}}

$ \rightarrow $ $ LIST= $ $ (\{s1\},\{b1\},\{\}) $ $ (\{s2\},\{b2\},\{\}) $ $ (\{s1,s2\},\{b1\},\{put\}) $

\resizebox*{!}{3cm}{\includegraphics{StackBuf3.eps}}

$ \rightarrow $ $ LIST= $ $ (\{s1\},\{b1\},\{\}) $ $ (\{s2\},\{b2\},\{\}) $ $ (\{s1,s2\},\{b1\},\{\}) $

$ (\{s2\},\{b2\},\{get\}) $ ist unter 6. bereits in $ LIST $ und unter 3. gibt es kein $ (X,Y,R) $ mit $ R\neq \emptyset $ in $ LIST $ mehr. Also gilt die Beziehung $ NewNDStack:<Buf $.


next up previous contents
Nächste Seite: Erfüllung der Erwartungen eines Aufwärts: Verfügbarkeit der Services eines Vorherige Seite: Subtyping von regulären Typen   Inhalt
Jörg Haeger 2001-04-26