SpecVer:O projekcie - Historia wersji

AndrzejSalwicki o 18:34, 13 mar 2013

2013-03-13T18:34:30Z

AndrzejSalwicki o 07:38, 12 lut 2013

2013-02-12T07:38:43Z

AndrzejSalwicki o 08:27, 10 lut 2013

2013-02-10T08:27:56Z

AndrzejSalwicki o 07:01, 10 lut 2013

2013-02-10T07:01:38Z

AndrzejSalwicki o 09:50, 4 lut 2013

2013-02-04T09:50:45Z

AndrzejSalwicki o 22:57, 3 lut 2013

2013-02-03T22:57:01Z

AndrzejSalwicki o 20:18, 3 lut 2013

2013-02-03T20:18:35Z

AndrzejSalwicki o 20:16, 3 lut 2013

2013-02-03T20:16:28Z

AndrzejSalwicki o 20:08, 3 lut 2013

2013-02-03T20:08:50Z

AndrzejSalwicki o 20:08, 3 lut 2013

2013-02-03T20:08:08Z

← poprzednia wersja		Wersja z 18:34, 13 mar 2013
Linia 97:		Linia 97:


−	~~[[Category:SpecVer]]~~	+
	\color{black}		\color{black}

@@ Linia 4: / Linia 4: @@
-To jest formuła <math>\alpha\Rightarrow  \implies K\,\beta </math>
+To jest formuła <math>\color{red}\alpha\Rightarrow   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>\color{blue}\alpha </math>
-i warunku końcowego <math> \beta </math>.
+i warunku końcowego <math> \color{blue}\beta </math>.
 Próba
@@ Linia 28: / Linia 28: @@
 Jeśli założenia o programie <math>M</math> odziedziczy program <math>K</math>, to mamy wtedy
 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}
 \end{array} \right )^i
   \end{array}   \right \}\alpha    \implies
   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}
 \end{array} \right )^i ; \\
   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}
 \end{array} \right )^i
@@ Linia 98: / Linia 98: @@
 [[Category:SpecVer]]

@@ Linia 2: / Linia 2: @@
 {{Witaj}}
 To jest formuła <math>\alpha\Rightarrow  \implies K\,\beta </math>
 opisująca poprawność algorytmu K względem warunku poczatkowego <math>\alpha </math>

@@ Linia 1: / Linia 1: @@
 <big>Obecna wersja tej strony to szkicownik brulion do ćwiczeń. Nie ma nic wspólnego z docelową treścią tego artykułu.</big>
+{{Witaj}}
 To jest formuła <math>\alpha\Rightarrow  \implies K\,\beta </math>
 opisująca poprawność algorytmu K względem warunku poczatkowego <math>\alpha </math>

@@ Linia 2: / Linia 2: @@
-To jest formuła <math>\alpha \implies K\,\beta </math>
+To jest formuła <math>\alpha\Rightarrow  \implies K\,\beta </math>
 opisująca poprawność algorytmu K względem warunku poczatkowego <math>\alpha </math>
 i warunku końcowego <math> \beta </math>.

← poprzednia wersja		Wersja z 22:57, 3 lut 2013
Linia 1:		Linia 1:
		+	<big>Obecna wersja tej strony to szkicownik brulion do ćwiczeń. Nie ma nic wspólnego z docelową treścią tego artykułu.</big>
		+
		+
	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>

@@ Linia 89: / Linia 89: @@
 \mathbf{end}\ Traverser;
 \end{array} \right . \\
-</math>
+\end{array}</math>
 [[Category:SpecVer]]

@@ Linia 13: / Linia 13: @@
-Zacznijmy od tego, że jest tautologią każda formuła o nastepujacym schemacie
+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
@@ Linia 24: / Linia 24: @@
 taką tautologię
 <center><math>S:  \left \{   \begin{array}{l}  P:  \delta:=true; n1:=n; \\
-   M:  \left ( \begin{array}{l}
+    M:  \left ( \begin{array}{l}
 \mathbf{if}\ \delta\ \mathbf{then}\ K\ \mathbf{fi}
 \end{array} \right )^i
@@ Linia 41: / Linia 41: @@
 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}

@@ Linia 6: / Linia 6: @@
 <math> \left ( \begin{array}{l}
-\left ( \alpha \\
+  \alpha \\
-\beta \right )
+\beta
-\end{array} \right
+\end{array} \right )
 </math>

@@ Linia 11: / Linia 11: @@
 </math>
-$$\left ( \begin{array}{l} \left ( \alpha \\ \beta \right ) \end{array} \right )$$
 Zacznijmy od tego, że jest tautologią każda formuła o nastepujacym schemacie