Poprawność: Różnice pomiędzy wersjami

Z Lem
Skocz do: nawigacji, wyszukiwania
Linia 16: Linia 16:
 
końcowe wartości zmiennych x i y sa 3 i 7.
 
końcowe wartości zmiennych x i y sa 3 i 7.
  
Zapiszmy to tak
+
Zapiszmy to tak<br />
<math>(x=7 \and y=3)\implies block var z: integer begin z:=y; y:=x; x:=z end  (x=3 \land y=7)</math>
+
 
 +
<math>(x=7 \land y=3)\implies '''block'''\ var\ z:\ integer\ begin\ z:=y;\ y:=x;\ x:=z\ end  (x=3 \land y=7)</math>
 
ppp
 
ppp

Wersja z 11:15, 14 sty 2015

Jakie znaczenie przypisać zwrotowi program [math]P[/math] jest poprawny? Tak sformułowane zdanie nie może byc ani prawdziwe, ani fałszywe.

Brakuje kilku elementów, zwrot ten musi być doprecyzowany.

Nieco lepiej brzmi zdanie
program [math]P[/math] jest poprawny ze względu na warunek początkowy [math]\alpha[/math] i warunek końcowy [math]\beta[/math].

Zdanie to należy odczytywać w następujący sposób:jeśli dane programu [math]P[/math] spełniają warunek poczatkowy [math]\alpha[/math] to obliczenie programu P jest skończone i udane, a jego wynik spełnia warunek końcowy [math]\beta[/math].

Widzimy, że brakuje tu informacji o danych i o obliczeniu. Dane to początkowe wartości zmiennych występujących w programie. Obliczenie programu może wyglądać różnie w różnych środowiskach. Przyjmiemy, że środowiskiem jest struktura danych (inaczej zwana: strukturą algebraiczną, algebrą, dziedziną matematyczną, modelem lub środowiskiem opisanym jako klasa -- w programowaniu obiektowym, lub zestaw pierwotnych typów danych w języku programowania LP).

Przykłady

  1. Niech początkowe wartości zmiennych x i y będą odpowiednio 7 i 3. Po wykonaniu programu
block var z:integer; begin z:=y; y:=x; x:=z end

końcowe wartości zmiennych x i y sa 3 i 7.

Zapiszmy to tak

[math](x=7 \land y=3)\implies '''block'''\ var\ z:\ integer\ begin\ z:=y;\ y:=x;\ x:=z\ end (x=3 \land y=7)[/math] ppp