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

Z Lem
Skocz do: nawigacji, wyszukiwania
(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 to możemy użyć kwantyfikatora iteracji  
+
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.

  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
  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

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]

Przykłady