Wyrażalność semantycznych własności programów: Różnice pomiędzy wersjami
(→Schematy formuł wyrazających własności programów) |
(→Przykłady) |
||
| Linia 18: | Linia 18: | ||
==Przykłady== | ==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>. | + | <big>Ad 1</big>) 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. | 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 | c) algorytm Euklidesa | ||
<br /> | <br /> | ||
| − | 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''. | + | <big>Ad 2</big>) 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''. |
Wersja z 08:53, 7 paź 2018
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.
- Skończoność obliczenia programu, tj. własność stopu
- 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. Najsłabszym warunkiem wstępnym programu [math]K[/math] ze względu na warunek końcowy [math]\beta[/math], jest taki warunek [math]\alpha[/math], który posiada dwie własności: 1) jeżeli początkowe dane programu spełniają warunek [math]\alpha[/math] to obliczenie programu jest skończone i spełnia warunek [math]\beta[/math], (czyli [math]\alpha[/math] jest warunkiem wstępnym dla programu [math]K[/math] i warunku końcowego [math]\beta[/math]) 2) jeśli jakiś inny warunek [math]\delta[/math] jest warunkiem wstępnym to jest mocniejszy niż warunek [math]\alpha[/math] tj ...
- 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]
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.
