Wyrażalność semantycznych własności programów
Spis treści
[ukryj]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 K
- 1) jeżeli początkowe dane programu spełniają warunek αto obliczenie programu jest skończone i spełnia warunek β, (czyli αjest warunkiem wstępnym dla programu Ki warunku końcowego β) oraz
- 2) jeśli jakiś inny warunek δjest warunkiem wstępnym to jest mocniejszy niż warunek αtj w rozpatrywanej strukturze danych prawdziwa jest implikacja δ⟹α.
Najmocniejszy warunek końcowy
Poprawność programu
K
Częściowa poprawność programu
K
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 K
Gdy program K
Ad 2) Własność niekończącego się obliczenia programu whileγdoMod
Ad 4) Własność najsłabszy warunek wstępny warunku α
- 1) czy formuła Kαjest warunkiem wstępnym?
- 2) czy formuła ta jest najsłabszym warunkiem wstKαpnym.
Przykłady
Ad 1)
a) Rozpatrzmy prosty program {y:=0;whilex≠ydoy:=y+1od}
b) Niech x i y będą zmiennymi typu real. Własność stopu programu {z:=0;whilex≥zdoz:=z+yod}(x=y)
c) algorytm Euklidesa
Ad 2) Własność niekończących się obliczeń programu {whilex≥0dox:=x+1od}