SpecVer:O projekcie: Różnice pomiędzy wersjami

Z Lem
Skocz do: nawigacji, wyszukiwania
Linia 1: Linia 1:
 
To jest formuła <math>\alpha \implies K\,\beta </math>
 
To jest formuła <math>\alpha \implies K\,\beta </math>
 
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>.
 +
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>
 +
 
  
 
[[Category:SpecVer]]
 
[[Category:SpecVer]]

Wersja z 08:52, 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]. 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]