Wyrażalność semantycznych własności programów - Historia wersji

AndrzejSalwicki: /* Przykłady */

2018-10-09T07:49:21Z

‎Przykłady

AndrzejSalwicki: /* Częściowa poprawność programu */

2018-10-09T07:35:09Z

‎Częściowa poprawność programu

AndrzejSalwicki: /* Poprawność programu */

2018-10-09T07:34:30Z

‎Poprawność programu

AndrzejSalwicki: /* Najsłabszy warunek wstępny */

2018-10-09T07:31:05Z

‎Najsłabszy warunek wstępny

AndrzejSalwicki o 07:30, 9 paź 2018

2018-10-09T07:30:09Z

AndrzejSalwicki o 07:28, 9 paź 2018

2018-10-09T07:28:23Z

AndrzejSalwicki: /* Schematy formuł wyrazających własności programów */

2018-10-09T07:24:26Z

‎Schematy formuł wyrazających własności programów

AndrzejSalwicki: /* Schematy formuł wyrazających własności programów */

2018-10-09T07:22:58Z

‎Schematy formuł wyrazających własności programów

AndrzejSalwicki: /* Własności semantyczne algorytmów */

2018-10-09T07:19:45Z

‎Własności semantyczne algorytmów

AndrzejSalwicki: /* Własności semantyczne algorytmów */

2018-10-09T06:56:01Z

‎Własności semantyczne algorytmów

@@ Linia 35: / Linia 35: @@
 a) Rozpatrzmy prosty program <math>\color{blue}{\{y:=0;\,\mathbf{while}\,x\neq y \, \mathbf{do} \, y:=y+1 \, \mathbf{od}\}}</math>.
-Własność stopu tego programu czyli formuła  <math>\color{blue}{\{y:=0;\,\mathbf{while}\,x\neq y \, \mathbf{do} \, y:=y+1 \, \mathbf{od}\}(x=y)}</math> jest prawdziwa w strukturze liczb naturalnych (dla programistów: unsigned integer). Formułę tę lub jej równoważną formułę <math>\color{blue}{\{y:=0;\,\bigcup \mathbf{if}\,x\neq y \, \mathbf{then} \, y:=y+1 \, \mathbf{fi}\}(x=y)}</math>  można przyjąć jako aksjomat liczb naturalnych.
+Własność stopu tego programu czyli formuła  <math>\color{blue}{\{y:=0;\,\mathbf{while}\,x\neq y \, \mathbf{do} \, y:=y+1 \, \mathbf{od}\}(x=y)}</math> jest prawdziwa w strukturze liczb naturalnych (dla programistów: unsigned integer). Formułę tę lub jej równoważną formułę <math>\color{blue}{\{y:=0\}\,\bigcup \{\mathbf{if}\,x\neq y \, \mathbf{then} \, y:=y+1 \, \mathbf{fi}\}(x=y)}</math>  można przyjąć jako aksjomat liczb naturalnych.
 b) Niech  x i y będą zmiennymi typu real. Własność stopu programu <math>\color{blue}{\{z:=0;\,\mathbf{while}\,x\geq z \, \mathbf{do} \, z:=z+y \, \mathbf{od}\}(x=y)}</math> ma związek z prawem Archimedesa zob.

@@ Linia 16: / Linia 16: @@
 <math>K</math> ze względu na warunek poczatkowy <math>\alpha</math> i warunek końcowy <math>\beta</math>.
 =====Częściowa poprawność programu=====
-<math>K</math> ze względu na warunek poczatkowy <math>/alpha</math> i warunek końcowy <math>\beta</math>.
+<math>K</math> ze względu na warunek poczatkowy <math>\alpha</math> i warunek końcowy <math>\beta</math>.
 =====Równoważność programów=====

@@ Linia 14: / Linia 14: @@
 =====Najmocniejszy warunek końcowy=====
 =====Poprawność programu=====
- <math>K</math> ze względu na warunek poczatkowy <math>\alpha</math> i warunek końcowy <math>\beta</math>.
+<math>K</math> ze względu na warunek poczatkowy <math>\alpha</math> i warunek końcowy <math>\beta</math>.
-=====Częściowa poprawność programu===== <math>K</math> ze względu na warunek poczatkowy <math>/alpha</math> i warunek końcowy <math>\beta</math>.
+=====Częściowa poprawność programu=====
 =====Równoważność programów=====

@@ Linia 8: / Linia 8: @@
 polegający na tym, że podczas obliczenia programu argument(y) nie należą do dziedziny operacji np. błąd dzielenia przez zero.
 =====Najsłabszy warunek wstępny=====
-'''Definicja'''. ''Najsłabszym warunkiem wstępnym'' programu <math>\color{blue}K</math> ze względu na warunek końcowy <math>\color{blue}\beta</math>, jest taki warunek <math>\color{blue}\alpha</math>, który posiada dwie własności: 1) jeżeli początkowe dane programu spełniają warunek <math>\color{blue}\alpha</math> to obliczenie programu jest skończone i spełnia warunek <math>\color{blue}\beta</math>, (czyli <math>\color{blue}\alpha</math> jest warunkiem wstępnym dla programu <math>\color{blue}K</math> i warunku końcowego <math>\color{blue}\beta</math>)  oraz 2) jeśli jakiś inny warunek <math>\color{blue}\delta</math> jest warunkiem wstępnym to jest mocniejszy niż warunek <math>\color{blue}\alpha</math> tj w rozpatrywanej strukturze danych prawdziwa jest implikacja <math>\color{blue}\delta \implies \alpha</math> .
+'''Definicja'''. ''Najsłabszym warunkiem wstępnym'' programu <math>\color{blue}K</math> ze względu na warunek końcowy <math>\color{blue}\beta</math>, jest taki warunek <math>\color{blue}\alpha</math>, który posiada dwie własności:
 =====Najmocniejszy warunek końcowy=====
 =====Poprawność programu=====

← poprzednia wersja		Wersja z 07:30, 9 paź 2018
Linia 1:		Linia 1:
−	~~{{spis treści}}~~
	==Własności semantyczne algorytmów==		==Własności semantyczne algorytmów==
	Prawie wszystkie semantyczne własności programów mogą być wyrażone przez odpowiednio napisane formuły języka rachunku programów.		Prawie wszystkie semantyczne własności programów mogą być wyrażone przez odpowiednio napisane formuły języka rachunku programów.

← poprzednia wersja		Wersja z 07:28, 9 paź 2018
Linia 1:		Linia 1:
		+	{{spis treści}}
	==Własności semantyczne algorytmów==		==Własności semantyczne algorytmów==
	Prawie wszystkie semantyczne własności programów mogą być wyrażone przez odpowiednio napisane formuły języka rachunku programów.		Prawie wszystkie semantyczne własności programów mogą być wyrażone przez odpowiednio napisane formuły języka rachunku programów.

@@ Linia 23: / Linia 23: @@
 <big>Ad 4</big>) Własność ''najsłabszy warunek wstępny warunku <math>\color{blue}\alpha</math> ze względu na program <math>\color{blue}K</math> ,  wyraża się przy pomocy formuły'' <math>\color{blue}K\,\alpha</math>.
 By się o tym przekonać wystarczy sprawdzić dwie własności:<br />
-;1) czy formuła <math>\color{blue}K\,\alpha</math> jest warunkiem wstępnym?
+:1) czy formuła <math>\color{blue}K\,\alpha</math> jest warunkiem wstępnym?
-;2) czy formuła ta jest najsłabszym warunkiem wst<math>\color{blue}K\,\alpha</math>pnym.<br />
+:2) czy formuła ta jest najsłabszym warunkiem wst<math>\color{blue}K\,\alpha</math>pnym.<br />
 ==Przykłady==

@@ Linia 1: / Linia 1: @@
 ==Własności semantyczne algorytmów==
 Prawie wszystkie semantyczne własności programów mogą być wyrażone przez odpowiednio napisane formuły języka rachunku programów.
-===Własność stopu===
+=====Własność stopu=====
 Skończoność obliczenia programu, tj. własność stopu
-===Własność zapętlenia===
+=====Własność zapętlenia=====
 Niekończenie obliczeń
-===Błąd=== polegający na tym, że podczas obliczenia programu argument(y) nie należą do dziedziny operacji np. błąd dzielenia przez zero.
+=====Błąd=====
- ===Najsłabszy warunek wstępny==='''Definicja'''. ''Najsłabszym warunkiem wstępnym'' programu <math>\color{blue}K</math> ze względu na warunek końcowy <math>\color{blue}\beta</math>, jest taki warunek <math>\color{blue}\alpha</math>, który posiada dwie własności: 1) jeżeli początkowe dane programu spełniają warunek <math>\color{blue}\alpha</math> to obliczenie programu jest skończone i spełnia warunek <math>\color{blue}\beta</math>, (czyli <math>\color{blue}\alpha</math> jest warunkiem wstępnym dla programu <math>\color{blue}K</math> i warunku końcowego <math>\color{blue}\beta</math>)  oraz 2) jeśli jakiś inny warunek <math>\color{blue}\delta</math> jest warunkiem wstępnym to jest mocniejszy niż warunek <math>\color{blue}\alpha</math> tj w rozpatrywanej strukturze danych prawdziwa jest implikacja <math>\color{blue}\delta \implies \alpha</math> .
+polegający na tym, że podczas obliczenia programu argument(y) nie należą do dziedziny operacji np. błąd dzielenia przez zero.
- ===Najmocniejszy warunek końcowy===
+=====Najsłabszy warunek wstępny=====
-# ===Poprawność programu===
+'''Definicja'''. ''Najsłabszym warunkiem wstępnym'' programu <math>\color{blue}K</math> ze względu na warunek końcowy <math>\color{blue}\beta</math>, jest taki warunek <math>\color{blue}\alpha</math>, który posiada dwie własności: 1) jeżeli początkowe dane programu spełniają warunek <math>\color{blue}\alpha</math> to obliczenie programu jest skończone i spełnia warunek <math>\color{blue}\beta</math>, (czyli <math>\color{blue}\alpha</math> jest warunkiem wstępnym dla programu <math>\color{blue}K</math> i warunku końcowego <math>\color{blue}\beta</math>)  oraz 2) jeśli jakiś inny warunek <math>\color{blue}\delta</math> jest warunkiem wstępnym to jest mocniejszy niż warunek <math>\color{blue}\alpha</math> tj w rozpatrywanej strukturze danych prawdziwa jest implikacja <math>\color{blue}\delta \implies \alpha</math> .
   <math>K</math> ze względu na warunek poczatkowy <math>\alpha</math> i warunek końcowy <math>\beta</math>.
-# ===Częściowa poprawność programu=== <math>K</math> ze względu na warunek poczatkowy <math>/alpha</math> i warunek końcowy <math>\beta</math>.
+=====Częściowa poprawność programu===== <math>K</math> ze względu na warunek poczatkowy <math>/alpha</math> i warunek końcowy <math>\beta</math>.
-# ===Równoważność programów===
+=====Równoważność programów=====
 Więcej o obliczeniach, semantyce i o semantycznych własnościach programów znajdziesz w książkach Algorithmic Logic str.  oraz Logika Algorytmiczna dla programistów str.