Wyrażalność semantycznych własności programów: Różnice pomiędzy wersjami
Z Lem
(Utworzono nową stronę "==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 pro...") |
(→Schematy formuł wyrazających własności programów) |
||
| Linia 11: | Linia 11: | ||
==Schematy formuł wyrazających własności 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>. <br /> | Własność stopu programu <math>K</math> najszybciej zapiszemy tak <math>K\,\mathbf{true}</math>. <br /> | ||
| − | Gdy program jest postaci | + | 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> |
| + | |||
==Przykłady== | ==Przykłady== | ||
Wersja z 15:44, 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
- 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]
