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

Wersja z 20:18, 3 lut 2013 (pokaż źródło) AndrzejSalwicki (dyskusja | edycje) ← poprzednia edycja		Aktualna wersja na dzień 18:34, 13 mar 2013 (pokaż źródło) AndrzejSalwicki (dyskusja | edycje)
(Nie pokazano 5 pośrednich wersji utworzonych przez tego samego użytkownika)
Linia 1:		Linia 1:
−	To jest formuła <math>\alpha \implies K\,\beta </math>	+	<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} 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}  \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; \\
−	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 ; \\
	P:  \delta:=true; n1:=n; \\		P:  \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
Linia 92:		Linia 97:
−	[[Category:SpecVer]]	+
		+	\color{black}

---

Aktualna wersja na dzień 18: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

$$\color{red}\alpha\Rightarrow K\,\beta$$ opisująca poprawność algorytmu K względem warunku poczatkowego $$\color{blue}\alpha$$ i warunku końcowego $$\color{blue}\beta$$ .

Próba

$$\left ( \begin{array}{l} \alpha \\ \beta \end{array} \right )$$

Zacznijmy od tego, że jest tautologią każda formuła o następujacym schemacie

$$S \alpha \implies S \alpha$$ a więc także formuła postaci

$$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$$ $$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ść

$$\{ \color{red} P;M \color{black} \}\, \alpha \implies \{ \color{red} P;M;P;M \color{black}\} \, \alpha$$

Jeśli założenia o programie

$$M$$ odziedziczy program $$K$$ , to mamy wtedy taką tautologię

$$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} \right \}\alpha \implies 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} \end{array} \right )^i ; \\ P: \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} \right \}\alpha$$

Tak, tak, prawdę mówił Maciej stary...

I większa formuła

$$\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}$$

popatrzmy

$$\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}$$

\color{black}