Wyrażalność semantycznych własności programów: Różnice pomiędzy wersjami
(→Własności semantyczne algorytmów) |
(→Własności semantyczne algorytmów) |
||
| Linia 4: | Linia 4: | ||
# Niekończenie obliczeń | # 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 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ł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 ... | 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 | # Najmocniejszy warunek końcowy | ||
Wersja z 15:58, 6 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
Schematy formuł wyrazających własności programów
Własność stopu programu [math]K[/math] najszybciej zapiszemy tak [math]K\,\mathbf{true}[/math].
Gdy program [math]K[/math] jest postaci [math]\mathbf{while}\,\gamma \, \mathbf{do} \, M \, \mathbf{od}[/math] to możemy użyć kwantyfikatora iteracji i napisać formułę algorytmiczną [math]\bigcup \{ \mathbf{if}\,\gamma \, \mathbf{then} \, M \, \mathbf{fi} \}\neg \gamma[/math]
