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

Z Lem
Skocz do: nawigacji, wyszukiwania
Linia 12: Linia 12:
  
 
Zacznijmy od tego, że jest tautologią każda formuła o nastepujacym schemacie
 
Zacznijmy od tego, że jest tautologią każda formuła o nastepujacym schemacie
\[S  \alpha  \implies S  \alpha  \]
+
<math>S  \alpha  \implies S  \alpha  </math>
 
a więc także formuła postaci
 
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  \]
+
<center><math> S:  \left \{ \color{red} \begin{array}{l} P; \\ M \end{array} \color{black} \right \}\alpha    \implies S:  \left \{ \color{red} \begin{array}{l} P; \\ M \end{array} \color{black}\right \} \alpha  </math></center>
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ść
+
Niech program P składa się z dwu instukcji <math>\color{red}P:\color{black}\delta:=true; n1:=n </math> , a  o programie <math>\color{red} M \color{red}</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ść
\[\{   P;M   \}\, \alpha \implies \{   P;M;P;M \} \, \alpha  \]
+
<center><math>\{ \color{red}  P;M \color{black} \}\, \alpha \implies \{ \color{red} P;M;P;M \color{black}\} \, \alpha  </math></center>
Jeśli założenia o programie $M$ odziedziczy program $K$, 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ę
\[ \left \{  \begin{array}{l} P: \delta:=true; n1:=n; \\
+
<center><math>S: \left \{  \begin{array}{l} \color{red}P: \color{black}\delta:=true; n1:=n; \\
M: \left ( \begin{array}{l}
+
\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} \color{black} \right \}\alpha    \implies
S^2:  \left \{  \begin{array}{l} P: \delta:=true; n1:=n; \\
+
S^2:  \left \{  \begin{array}{l} \color{red}P: \color{black}\delta:=true; n1:=n; \\
M:\color{black} \left ( \begin{array}{l}
+
\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 ; \\
 
\color{red}P: \color{black}\delta:=true; n1:=n; \\
 
\color{red}P: \color{black}\delta:=true; n1:=n; \\
\color{red} M:\color{black} \left ( \begin{array}{l}
+
\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} \color{black} \right \}\alpha  \]
+
\end{array} \color{black} \right \}\alpha  </math></center>
  
 +
Tak, tak, prawdę mówił Maciej stary...
  
 
I większa formuła
 
I większa formuła

Wersja z 09:59, 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 [math]S \alpha \implies S \alpha [/math] a więc także formuła postaci

[math] S: \left \{ \color{red} \begin{array}{l} P; \\ M \end{array} \color{black} \right \}\alpha \implies S: \left \{ \color{red} \begin{array}{l} P; \\ M \end{array} \color{black}\right \} \alpha [/math]

Niech program P składa się z dwu instukcji [math]\color{red}P:\color{black}\delta:=true; n1:=n [/math] , a o programie [math]\color{red} M \color{red}[/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ść

[math]\{ \color{red} P;M \color{black} \}\, \alpha \implies \{ \color{red} P;M;P;M \color{black}\} \, \alpha [/math]

Jeśli założenia o programie [math]M[/math] odziedziczy program [math]K[/math], to mamy wtedy taką tautologię

[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} \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}\ 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 [/math]

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 . \\ [/math]