Poprawność - Historia wersji

AndrzejSalwicki o 10:26, 14 sty 2015

2015-01-14T10:26:54Z

AndrzejSalwicki o 10:25, 14 sty 2015

2015-01-14T10:25:24Z

AndrzejSalwicki o 10:23, 14 sty 2015

2015-01-14T10:23:08Z

AndrzejSalwicki o 10:22, 14 sty 2015

2015-01-14T10:22:08Z

AndrzejSalwicki o 10:20, 14 sty 2015

2015-01-14T10:20:35Z

AndrzejSalwicki o 10:18, 14 sty 2015

2015-01-14T10:18:10Z

AndrzejSalwicki o 10:15, 14 sty 2015

2015-01-14T10:15:58Z

AndrzejSalwicki o 10:14, 14 sty 2015

2015-01-14T10:14:23Z

AndrzejSalwicki o 09:23, 14 sty 2015

2015-01-14T09:23:00Z

AndrzejSalwicki: Utworzono nową stronę "Jakie znaczenie przypisać zwrotowi ''program $P$ jest poprawny''? Tak sformułowane zdanie nie może byc ani prawdziwe, ani fałszywe. Brakuje kilku element..."

2015-01-14T09:18:14Z

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

Nowa strona

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.
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ępujacy 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).

@@ Linia 12: / Linia 12: @@
 '''Przykłady'''
-# Niech początkowe wartości zmiennych x i y będą odpowiednio 7 i 3. Po wykonaniu programu
+# 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>
 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

@@ Linia 15: / Linia 15: @@
 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<br />
+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>
+<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> {'''block''' '''begin'''\ z:=y+x;\  '''end'''} <math> (z=10 \land x=3 \land y=7)</math>
+<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

@@ Linia 12: / Linia 12: @@
 '''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
+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<br />
 <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> {'''block'''\ '''begin'''\ z:=y+x;\  '''end'''} <math> (z=10 \land x=3 \land y=7)</math>
+<math>(x=7 \land y=3 \land z=z)\implies</math> {'''block''' '''begin'''\ z:=y+x;\  '''end'''} <math> (z=10 \land x=3 \land y=7)</math>
 ppp

@@ Linia 15: / Linia 15: @@
   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<br />
 <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> {'''block'''\ '''begin'''\ z:=y+x;\  '''end'''} <math> (x=3 \land y=7)</math>
+<math>(x=7 \land y=3 \land z=z)\implies</math> {'''block'''\ '''begin'''\ z:=y+x;\  '''end'''} <math> (z=10 \land x=3 \land y=7)</math>
 ppp

← poprzednia wersja		Wersja z 10:20, 14 sty 2015
Linia 19:		Linia 19:

	<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>		<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> {'''block'''\ '''begin'''\ z:=y+x;\ '''end'''} <math> (x=3 \land y=7)</math>
		+
	ppp		ppp

← poprzednia wersja		Wersja z 10:14, 14 sty 2015
Linia 12:		Linia 12:

	'''Przykłady'''		'''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 \and y=3)\implies block var z: integer begin z:=y; y:=x; x:=z end (x=3 \land y=7)</math>
		+	ppp

@@ Linia 1: / Linia 1: @@
 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 następujacy 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).