Wyrażalność semantycznych własności programów: Różnice pomiędzy wersjami

Z Lem
Skocz do: nawigacji, wyszukiwania
(Własności semantyczne algorytmów)
(Własności semantyczne algorytmów)
Linia 1: Linia 1:
 
==Własności semantyczne algorytmów==
 
==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.
 
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
+
# ===Własność stopu===
# Niekończenie obliczeń
+
Skończoność obliczenia programu, tj. własność stopu
# Błąd polegający na tym, że podczas obliczenia programu argument(y) nie należą do dziedziny operacji np. błąd dzielenia przez zero.
+
# ===Własność zapętlenia ===
# Najsłabszy warunek wstępny'''Definicja'''. ''Najsłabszym warunkiem wstępnym'' programu <math>\color{blue}K</math> ze względu na warunek końcowy <math>\color{blue}\beta</math>, jest taki warunek <math>\color{blue}\alpha</math>, który posiada dwie własności: 1) jeżeli początkowe dane programu spełniają warunek <math>\color{blue}\alpha</math> to obliczenie programu jest skończone i spełnia warunek <math>\color{blue}\beta</math>, (czyli <math>\color{blue}\alpha</math> jest warunkiem wstępnym dla programu <math>\color{blue}K</math> i warunku końcowego <math>\color{blue}\beta</math>)  oraz 2) jeśli jakiś inny warunek <math>\color{blue}\delta</math> jest warunkiem wstępnym to jest mocniejszy niż warunek <math>\color{blue}\alpha</math> tj w rozpatrywanej strukturze danych prawdziwa jest implikacja <math>\color{blue}\delta \implies \alpha</math> .
+
Niekończenie obliczeń
# Najmocniejszy warunek końcowy
+
# ===Błąd===
# Poprawność programu <math>K</math> ze względu na warunek poczatkowy <math>\alpha</math> i warunek końcowy <math>\beta</math>.
+
polegający na tym, że podczas obliczenia programu argument(y) nie należą do dziedziny operacji np. błąd dzielenia przez zero.
# Częściowa poprawność programu <math>K</math> ze względu na warunek poczatkowy <math>/alpha</math> i warunek końcowy <math>\beta</math>.
+
# ===Najsłabszy warunek wstępny===
# Równoważność programów
+
'''Definicja'''. ''Najsłabszym warunkiem wstępnym'' programu <math>\color{blue}K</math> ze względu na warunek końcowy <math>\color{blue}\beta</math>, jest taki warunek <math>\color{blue}\alpha</math>, który posiada dwie własności: 1) jeżeli początkowe dane programu spełniają warunek <math>\color{blue}\alpha</math> to obliczenie programu jest skończone i spełnia warunek <math>\color{blue}\beta</math>, (czyli <math>\color{blue}\alpha</math> jest warunkiem wstępnym dla programu <math>\color{blue}K</math> i warunku końcowego <math>\color{blue}\beta</math>)  oraz 2) jeśli jakiś inny warunek <math>\color{blue}\delta</math> jest warunkiem wstępnym to jest mocniejszy niż warunek <math>\color{blue}\alpha</math> tj w rozpatrywanej strukturze danych prawdziwa jest implikacja <math>\color{blue}\delta \implies \alpha</math> .
 +
# ===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.
 
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.

Wersja z 18:30, 8 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.

  1. ===Własność stopu===

Skończoność obliczenia programu, tj. własność stopu

  1. ===Własność zapętlenia ===

Niekończenie obliczeń

  1. ===Błąd===
polegający na tym, że podczas obliczenia programu argument(y) nie należą do dziedziny operacji np. błąd dzielenia przez zero.
  1. ===Najsłabszy warunek wstępny===

Definicja. Najsłabszym warunkiem wstępnym programu [math]\color{blue}K[/math] ze względu na warunek końcowy [math]\color{blue}\beta[/math], jest taki warunek [math]\color{blue}\alpha[/math], który posiada dwie własności: 1) jeżeli początkowe dane programu spełniają warunek [math]\color{blue}\alpha[/math] to obliczenie programu jest skończone i spełnia warunek [math]\color{blue}\beta[/math], (czyli [math]\color{blue}\alpha[/math] jest warunkiem wstępnym dla programu [math]\color{blue}K[/math] i warunku końcowego [math]\color{blue}\beta[/math]) oraz 2) jeśli jakiś inny warunek [math]\color{blue}\delta[/math] jest warunkiem wstępnym to jest mocniejszy niż warunek [math]\color{blue}\alpha[/math] tj w rozpatrywanej strukturze danych prawdziwa jest implikacja [math]\color{blue}\delta \implies \alpha[/math] .

  1. ===Najmocniejszy warunek końcowy===
  2. ===Poprawność programu===
[math]K[/math] ze względu na warunek poczatkowy [math]\alpha[/math] i warunek końcowy [math]\beta[/math].
  1. ===Częściowa poprawność programu=== [math]K[/math] ze względu na warunek poczatkowy [math]/alpha[/math] i warunek końcowy [math]\beta[/math].
  2. ===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]
Ad 4) Własność najsłabszy warunek wstępny warunku [math]\color{blue}\alpha[/math] ze względu na program [math]\color{blue}K[/math] , wyraża się przy pomocy formuły [math]\color{blue}K\,\alpha[/math]. By się o tym przekonać wystarczy sprawdzić dwie własności:
1) czy formuła [math]\color{blue}K\,\alpha[/math] jest warunkiem wstępnym? 2) czy formuła ta jest najsłabszym warunkiem wst[math]\color{blue}K\,\alpha[/math]pnym.

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.