Poprawność: Różnice pomiędzy wersjami
(Utworzono nową stronę "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...") |
|||
| (Nie pokazano 8 pośrednich wersji utworzonych przez tego samego użytkownika) | |||
| Linia 1: | Linia 1: | ||
Jakie znaczenie przypisać zwrotowi ''program <math>P</math> jest poprawny''? | 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. | + | Tak sformułowane zdanie nie może byc ani prawdziwe, ani fałszywe. |
| − | 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 | + | |
| + | Brakuje kilku elementów, zwrot ten musi być doprecyzowany. | ||
| + | |||
| + | Nieco lepiej brzmi zdanie <br /> | ||
| + | ''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). | 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''' | ||
| + | # 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</math> {'''block''' '''var''' z: integer '''begin''' z:=y; y:=x; x:=z '''end'''} <math> (x=3 \land y=7)</math> | ||
| + | # Nieco inny przykład | ||
| + | <math>(x=7 \land y=3 \land z=z)\implies</math> { z:=y+x } <math> (z=10 \land x=3 \land y=7)</math> | ||
| + | |||
| + | ppp | ||
Aktualna wersja na dzień 11:26, 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
- 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[/math] {block var z: integer begin z:=y; y:=x; x:=z end} [math] (x=3 \land y=7)[/math]
- Nieco inny przykład
[math](x=7 \land y=3 \land z=z)\implies[/math] { z:=y+x } [math] (z=10 \land x=3 \land y=7)[/math]
ppp
