Aksiomatska semantika

Iz E-študij, proste zakladnice študentskega znanja

Skoči na: navigacija, iskanje

Vsebina

Lastnosti programa

Parcialna pravilnost (Partial correctness)

Program P je parcialno pravilen glede na vhodni predikat φ in izhodni predikat ψ, če velja:

\forall \vec x: (\phi (\vec x) \land (P\ se\ konca\ (iztece)\ za\ \vec x ) \Rightarrow \psi(\vec x,P(\vec x))).

Postopek dokazovanja

  1. določimo prerezne točke tako, da prekinemo z njimi vse zanke. Dodamo startno in izhodne točke.
  2. vsaki prerezni točki i priredimo nek predikat qi, ki označuje stanje programa v dani točki
  3. preverimo naslednji pogoj za vsako pot α med prereznima točkama i in j: \forall \vec x, \vec y : p_i (\vec x , \vec y) \land R_{\alpha} (\vec x , \vec y) \Rightarrow p_j (\vec x , r_{\alpha} (\vec x , \vec y))

pri čemer definiramo še:

  • \vec x - vektor vhodnih parametrov programa
  • \vec y - vektor notranjih spremenljivk programa
  • R_{\alpha} : D_x \times D_y \rightarrow \{ true, false \} - pogoj, da gre program po tej poti (če gre vedno po neki poti potem je enostavno true)
  • r_{\alpha} : D_x \times D_y \rightarrow D_y - sprememba notranjih spremenljivk programa na tej poti izvajanja

S tem dokažemo, da so vse induktivne trditve izpolnjene vedno, kadar gre izvajanje programa skozi ustrezne točke. To velja tudi za izhodne točke, kar implicira, da je program parcialno pravilen (Floydov izrek).

Iztekanje (Terminating)

Program P se izteče glede na vhodni predikat φ, če se izvajanje za vse pravilne podatke konča:

\forall \vec x: \phi(\vec x) \Rightarrow izvajanje\ P\ se\ konca\ (iztece)

Postopek dokazovanja

  1. Izberi množico prereznih točk, ki prekine vse zanke. Vsaki točki priredi „ustrezno“ induktivno trditev q_i (\vec x , \vec y)
  2. izberemo dobro utemeljeno množico W (množico, v kateri je definirana relacija delne urejenosti in nima neskončnih padajočih zaporedij)
  3. za vsako prerezno točko, ki jih določimo na isti način kot pri dokazovanju parcialne pravilnosti, določimo še ustrezno parcialno funkcijo ui: u_i : D_x \times D_y \rightarrow W, Funcija je ustrezna, če velja \forall \vec x, \vec y : q_i (\vec x , \vec y) \Rightarrow u_i (\vec x , \vec y \in W)
  4. za vse poti v programu, ki so del kake zanke, mora biti izpolnjen pogoj terminiranja: \forall \vec x , \vec y : q_i (\vec x , \vec y ) \land R_{\alpha} (\vec x , \vec y ) \Rightarrow (u_i (\vec x , \vec y) > u_j (\vec x , r_{\alpha} (\vec x , \vec y ))).
  5. za poti, ki niso zanke, lahko zgornji pogoj tudi ne velja (zahtevana je stroga neenakost), tako da je treba načeloma preveriti le zanke.

Totalna pravilnost (Total correctness)

Totalna pravilnost glede φ in ψ velja, če je program parcialno pravilen in se izteče, torej:

\forall \vec x: (\phi(\vec x) \Rightarrow (P\ se\ konca\ (iztece)\ za\ \vec x ) \land \psi(\vec x,P(\vec x))).

Najšibkejši predpogoj (Weakest precondition)

Najšibkejši predpogoj označimo z wp(S,R).

  • S označuje seznam ukazov, ki se izvršijo.
  • R je predikat ali "popogoj".

Funkcija wp določi najšibkejši predpogoj za ukaze S tako, da je predikat R pravilen.

1. Primer

wp(x := E, R)\ =\ R_E^x

Predikat R z vrednostjo x zamenjanega z E.

2. Primer

wp(x := y - 5, x > 10)\ =\ (y - 5 > 10)\ =\ (y > 15)

Da je "popogoj" x > 10 zadoščen, mora veljati predpogoj y > 15. To je tudi najšibkejši predpogoj, saj je 15 "najšibkejša" omejitev spremenljivke y, da predikat x > 10 še drži.

Zunanje povezave

Zapiski predavanj

Vzpostavljeno iz »http://www.e-studij.si/Aksiomatska_semantika«
Osebna orodja
Imenski prostori
Različice
Dejanja
navigacija

Tiskanje/izvoz
orodja