Wyrażalność semantycznych własności programów
Z Lem
Wersja AndrzejSalwicki (dyskusja | edycje) z dnia 15:39, 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 jest postaci to możemy użyć kwantyfikatora iteracji