SpecVer:O projekcie: Różnice pomiędzy wersjami
| (Nie pokazano 6 pośrednich wersji utworzonych przez tego samego użytkownika) | |||
| Linia 1: | Linia 1: | ||
| − | To jest formuła <math>\alpha \ | + | <big>Obecna wersja tej strony to szkicownik brulion do ćwiczeń. Nie ma nic wspólnego z docelową treścią tego artykułu.</big> |
| − | opisująca poprawność algorytmu K względem warunku poczatkowego <math>\alpha </math> | + | |
| − | i warunku końcowego <math> \beta </math>. | + | {{Witaj}} |
| + | |||
| + | |||
| + | To jest formuła <math>\color{red}\alpha\Rightarrow K\,\beta </math> | ||
| + | opisująca poprawność algorytmu K względem warunku poczatkowego <math>\color{blue}\alpha </math> | ||
| + | i warunku końcowego <math> \color{blue}\beta </math>. | ||
Próba | Próba | ||
| Linia 23: | Linia 28: | ||
Jeśli założenia o programie <math>M</math> odziedziczy program <math>K</math>, to mamy wtedy | Jeśli założenia o programie <math>M</math> odziedziczy program <math>K</math>, to mamy wtedy | ||
taką tautologię | taką tautologię | ||
| − | <center><math>S: \left \{ \begin{array}{l} | + | <center><math>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}\ K\ \mathbf{fi} | \mathbf{if}\ \delta\ \mathbf{then}\ K\ \mathbf{fi} | ||
\end{array} \right )^i | \end{array} \right )^i | ||
\end{array} \right \}\alpha \implies | \end{array} \right \}\alpha \implies | ||
S^2: \left \{ \begin{array}{l} P: \delta:=true; n1:=n; \\ | S^2: \left \{ \begin{array}{l} P: \delta:=true; n1:=n; \\ | ||
| − | + | \color{red} M: \color{black} \left ( \begin{array}{l} | |
\mathbf{if}\ \delta\ \mathbf{then}\ K\ \mathbf{fi} | \mathbf{if}\ \delta\ \mathbf{then}\ K\ \mathbf{fi} | ||
\end{array} \right )^i ; \\ | \end{array} \right )^i ; \\ | ||
P: \delta:=true; n1:=n; \\ | P: \delta:=true; n1:=n; \\ | ||
| − | + | \color{red} M: \color{black} \left ( \begin{array}{l} | |
\mathbf{if}\ \delta\ \mathbf{then}\ K\ \mathbf{fi} | \mathbf{if}\ \delta\ \mathbf{then}\ K\ \mathbf{fi} | ||
\end{array} \right )^i | \end{array} \right )^i | ||
| Linia 89: | Linia 94: | ||
\mathbf{end}\ Traverser; | \mathbf{end}\ Traverser; | ||
\end{array} \right . \\ | \end{array} \right . \\ | ||
| − | </math> | + | \end{array}</math> |
| − | + | ||
| + | \color{black} | ||
Aktualna wersja na dzień 19:34, 13 mar 2013
Obecna wersja tej strony to szkicownik brulion do ćwiczeń. Nie ma nic wspólnego z docelową treścią tego artykułu.
Witaj na stronach projektu LEM!
To jest formuła [math]\color{red}\alpha\Rightarrow K\,\beta [/math]
opisująca poprawność algorytmu K względem warunku poczatkowego [math]\color{blue}\alpha [/math]
i warunku końcowego [math] \color{blue}\beta [/math].
Próba
[math] \left ( \begin{array}{l} \alpha \\ \beta \end{array} \right ) [/math]
Zacznijmy od tego, że jest tautologią każda formuła o następujacym schemacie [math]S \alpha \implies S \alpha [/math] a więc także formuła postaci
Niech program P składa się z dwu instukcji [math]\color{red}P:\color{black}\delta:=true; n1:=n [/math] , a o programie ([math] M [/math])wiadomo, że nie zmienia wartości zmiennej [math]n[/math], a jego obliczenie zależy tylko wartości zmiennych [math]\delta [/math] oraz [math]n1[/math]. Przy tych założeniach prawdziwa jest następująca równoważność
Jeśli założenia o programie [math]M[/math] odziedziczy program [math]K[/math], to mamy wtedy taką tautologię
Tak, tak, prawdę mówił Maciej stary...
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 . \\ \end{array}[/math]
\color{black}
