Wyrażalność semantycznych własności programów: Różnice pomiędzy wersjami
(→Własności semantyczne algorytmów) |
(→Przykłady) |
||
| (Nie pokazano 12 pośrednich wersji utworzonych przez tego samego użytkownika) | |||
| Linia 1: | Linia 1: | ||
==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. | ||
| − | + | =====Własność stopu===== | |
| − | + | Skończoność obliczenia programu, tj. własność stopu | |
| − | + | =====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. | |
| − | + | =====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> . | ||
| + | |||
| + | =====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>. | ||
| + | =====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===== | ||
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. | 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. | ||
| Linia 18: | Linia 28: | ||
<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>. | <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 /> | 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== | ==Przykłady== | ||
| Linia 25: | Linia 35: | ||
a) Rozpatrzmy prosty program <math>\color{blue}{\{y:=0;\,\mathbf{while}\,x\neq y \, \mathbf{do} \, y:=y+1 \, \mathbf{od}\}}</math>. | 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 | + | 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. | 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. | ||
Aktualna wersja na dzień 08:49, 9 paź 2018
Spis treści
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
Skończoność obliczenia programu, tj. własność stopu
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.
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] .
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].
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
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.
Schematy formuł wyrazających własności programów
Ad 1) Własność stopu programu [math]\color{blue}K[/math] najszybciej zapiszemy tak [math]\color{blue}K\,\mathbf{true}[/math].
Gdy program [math]\color{blue}K[/math] jest postaci [math]\color{blue}{\mathbf{while}\,\gamma \, \mathbf{do} \, M \, \mathbf{od}}[/math] to możemy użyć kwantyfikatora iteracji i napisać formułę algorytmiczną [math]\color{blue}{\bigcup \{ \mathbf{if}\,\gamma \, \mathbf{then} \, M \, \mathbf{fi} \}\neg \gamma}[/math]
Ad 2) Własność niekończącego się obliczenia programu [math]\color{blue}{\mathbf{while}\,\gamma \, \mathbf{do} \, M \, \mathbf{od}}[/math] można wyrazić w taki sposób [math]\color{blue}{\bigcap \{ \mathbf{if}\,\gamma \, \mathbf{then} \, M \, \mathbf{fi} \} \gamma}[/math]
Ad 4) 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:
- 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.
Przykłady
Ad 1)
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.
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.
c) algorytm Euklidesa
Ad 2) Własność niekończących się obliczeń programu [math]\color{blue}{\{\mathbf{while}\,x\geq 0 \, \mathbf{do} \, x:=x+1 \, \mathbf{od}\}}[/math] wyraża znaną w algebrze własność charakterystyka algebry A jest zero.
