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

Z Lem
Skocz do: nawigacji, wyszukiwania
(Schematy formuł wyrazających własności programów)
(Przykłady)
Linia 18: Linia 18:
  
 
==Przykłady==
 
==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>.
+
<big>Ad 1</big>) 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.
 
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.  
 
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  
 
c) algorytm Euklidesa  
 
<br />
 
<br />
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''.
+
<big>Ad 2</big>) 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''.

Wersja z 08:53, 7 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. Skończoność obliczenia programu, tj. własność stopu
  2. Niekończenie obliczeń
  3. Błąd polegający na tym, że podczas obliczenia programu argument(y) nie należą do dziedziny operacji np. błąd dzielenia przez zero.
  4. 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 ...
  5. Najmocniejszy warunek końcowy
  6. Poprawność programu [math]K[/math] ze względu na warunek poczatkowy [math]\alpha[/math] i warunek końcowy [math]\beta[/math].
  7. Częściowa poprawność programu [math]K[/math] ze względu na warunek poczatkowy [math]/alpha[/math] i warunek końcowy [math]\beta[/math].
  8. 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]

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.