SpecVer:O projekcie: Różnice pomiędzy wersjami
| Linia 2: | Linia 2: | ||
opisująca poprawność algorytmu K względem warunku poczatkowego <math>\alpha </math> | opisująca poprawność algorytmu K względem warunku poczatkowego <math>\alpha </math> | ||
i warunku końcowego <math> \beta </math>. | i warunku końcowego <math> \beta </math>. | ||
| + | |||
| + | Próba | ||
| + | |||
| + | <math> \left ( \begin{array}{l} | ||
| + | \left ( \alpha \\ | ||
| + | \beta \right ) | ||
| + | \end{array} \right ) | ||
| + | </math> | ||
| + | |||
| + | Zacznijmy od tego, że jest tautologią każda formuła o nastepujacym schemacie | ||
| + | \[S \alpha \implies S \alpha \] | ||
| + | a więc także formuła postaci | ||
| + | \[S: \left \{ \begin{array}{l} P; \\ M \end{array} \right \}\alpha \implies S: \left \{ \begin{array}{l} P; \\ M \end{array} \right \} \alpha \] | ||
| + | Niech program P składa się z dwu instukcji $\color{red}P:\color{black}\delta:=true; n1:=n $ , a o programie $ M $ wiadomo, że nie zmienia wartości zmiennej $n$, a jego obliczenie zależy tylko wartości zmiennych $\delta $ oraz $n1$. Przy tych założeniach prawdziwa jest następująca równoważność | ||
| + | \[\{ P;M \}\, \alpha \implies \{ P;M;P;M \} \, \alpha \] | ||
| + | Jeśli założenia o programie $M$ odziedziczy program $K$, to mamy wtedy | ||
| + | taką tautologię | ||
| + | \[S: \left \{ \begin{array}{l} P: \delta:=true; n1:=n; \\ | ||
| + | M: \left ( \begin{array}{l} | ||
| + | \mathbf{if}\ \delta\ \mathbf{then}\ K\ \mathbf{fi} | ||
| + | \end{array} \right )^i | ||
| + | \end{array} \right \}\alpha \implies | ||
| + | S^2: \left \{ \begin{array}{l} P: \delta:=true; n1:=n; \\ | ||
| + | M:\color{black} \left ( \begin{array}{l} | ||
| + | \mathbf{if}\ \delta\ \mathbf{then}\ K\ \mathbf{fi} | ||
| + | \end{array} \right )^i ; \\ | ||
| + | \color{red}P: \color{black}\delta:=true; n1:=n; \\ | ||
| + | \color{red} M:\color{black} \left ( \begin{array}{l} | ||
| + | \mathbf{if}\ \delta\ \mathbf{then}\ K\ \mathbf{fi} | ||
| + | \end{array} \right )^i | ||
| + | \end{array} \color{black} \right \}\alpha \] | ||
| + | |||
| + | |||
I większa formuła | I większa formuła | ||
<math> \begin{array}{l} S: \left \{ \begin{array}{l} \color{red}P: \color{black}\delta:=true; n1:=n; \\ | <math> \begin{array}{l} S: \left \{ \begin{array}{l} \color{red}P: \color{black}\delta:=true; n1:=n; \\ | ||
Wersja z 09:34, 3 lut 2013
To jest formuła [math]\alpha \implies K\,\beta [/math] opisująca poprawność algorytmu K względem warunku poczatkowego [math]\alpha [/math] i warunku końcowego [math] \beta [/math].
Próba
[math] \left ( \begin{array}{l} \left ( \alpha \\ \beta \right ) \end{array} \right ) [/math]
Zacznijmy od tego, że jest tautologią każda formuła o nastepujacym schemacie \[S \alpha \implies S \alpha \] a więc także formuła postaci \[S: \left \{ \begin{array}{l} P; \\ M \end{array} \right \}\alpha \implies S: \left \{ \begin{array}{l} P; \\ M \end{array} \right \} \alpha \] Niech program P składa się z dwu instukcji $\color{red}P:\color{black}\delta:=true; n1:=n $ , a o programie $ M $ wiadomo, że nie zmienia wartości zmiennej $n$, a jego obliczenie zależy tylko wartości zmiennych $\delta $ oraz $n1$. Przy tych założeniach prawdziwa jest następująca równoważność \[\{ P;M \}\, \alpha \implies \{ P;M;P;M \} \, \alpha \] Jeśli założenia o programie $M$ odziedziczy program $K$, to mamy wtedy taką tautologię \[S: \left \{ \begin{array}{l} P: \delta:=true; n1:=n; \\ M: \left ( \begin{array}{l} \mathbf{if}\ \delta\ \mathbf{then}\ K\ \mathbf{fi} \end{array} \right )^i \end{array} \right \}\alpha \implies S^2: \left \{ \begin{array}{l} P: \delta:=true; n1:=n; \\ M:\color{black} \left ( \begin{array}{l} \mathbf{if}\ \delta\ \mathbf{then}\ K\ \mathbf{fi} \end{array} \right )^i ; \\ \color{red}P: \color{black}\delta:=true; n1:=n; \\ \color{red} M:\color{black} \left ( \begin{array}{l} \mathbf{if}\ \delta\ \mathbf{then}\ K\ \mathbf{fi} \end{array} \right )^i \end{array} \color{black} \right \}\alpha \]
I większa formuła
[math] \begin{array}{l} S: \left \{ \begin{array}{l} \color{red}P: \color{black}\delta:=true; n1:=n; \\
\color{red} M:\color{black} \left ( \begin{array}{l}
\mathbf{if} \ \delta\\
\mathbf{then} \\
\quad K\\ \mathbf{fi}
\end{array} \right )^i
\end{array} \color{black} \right \}\alpha \implies
S^2: \left \{ \begin{array}{l} \color{red}P: \color{black}\delta:=true; n1:=n; \\
\color{red} M:\color{black} \left ( \begin{array}{l}
\mathbf{if} \ \delta\\
\mathbf{then} \\
\quad K\\ \mathbf{fi}
\end{array} \right )^i ; \\
\color{red}P: \color{black}\delta:=true; n1:=n; \\
\color{red} M:\color{black} \left ( \begin{array}{l}
\mathbf{if} \ \delta\\
\mathbf{then} \\
\quad K\\ \mathbf{fi}
\end{array} \right )^i
\end{array} \color{black} \right \}\alpha \end{array} [/math]
popatrzmy
[math] \begin{array}{l} \mathbf{var}\ T:\ arrayof\ Traverser; \\ \\ \left \{ \begin{array}{l} \mathbf{unit}\ Traverser:\ \mathbf{coroutine}(n: node); \\ \quad \mathbf{var}\ kolejny:\ integer; \\ \left \vert \begin{array}{l} \quad \mathbf{unit}\ traverse:\ \mathbf{procedure}(m:\ node); \\ \quad \mathbf{begin} \\ \qquad \mathbf{if}\ m \neq none \\ \qquad \mathbf{then} \\ \qquad\ \ \ \mathbf{call}\ traverse(m.left); \\ \qquad\ \ \ kolejny:=m.val; \\ \qquad \ \ \ \mathbf{detach};\ \ (*\ instrukcja\ \mathbf{detach}\ wznawia \\ \qquad \ \quad \ \ \ \ wspolprogram\ w,\ ktory\ ostatnio\ uaktywnil\ \\ \qquad \ \quad \ \ \ \ ten\,(\mathrm{this})\ obiekt\ Traverser\ wykonujac\ \mathbf{attach}(.)\ *) \\ \qquad\ \ \ \mathbf{call}\ traverse(m.right); \\ \qquad \mathbf{fi} \\ \quad \mathbf{end}\ traverse; \end{array} \right . \\ \mathbf{begin} \\ \quad \mathbf{return}; \\ \quad \mathbf{call}\ traverse(n) \\ \mathbf{end}\ Traverser; \end{array} \right . \\ [/math]
