4962385654

(3)

Często użyteczna jest reguła która nieznacznie uogólnia regułę (2)

P => P', P'{ I }Q, Q => Q', Q'{ J }R, R'

P{ /; J }_R'

Przykład. Zamianę wartość zmiennych x i y dowolnego typy T można wykonać używając dodatkowej zmiennej z typu T w następujący sposób:

z:=x;

x:=y;

y:=z

Można to wykazać używając opisu znaczenia instrukcji podstawiania (1) oraz reguły (2) w następujący sposób:

(x = a A y = b) {z \= x} (z = a A y = b)

(z = a A y = b) {x := y} (z = a A x = b)

(z = a A x = b) {y := z} (y = a A x = b)

W praktyce takie rozumowania jest lepiej prowadzić od końca.

Zatem, używając dwukrotnie reguły (2), otrzymujemy

(x = a A y = b) {z := x\ x := y; y := z} (y = a A x = b)

Gdy T jest typem całkowitym lub rzeczywistym to możemy zamienić wartości zmiennych x i y nie używając dodatkowej zmiennej, w następujący sposób: x:=x+y; y:=x-y;

x:=x-y

By pokazać, że powyższe trzy instrukcje rzeczywiście wymieniają wartości zmiennych x i y znowu użyjemy aksjomatu (1) zaczynając od końca (gdzie wstawiamy formułę którą chcemy udowodnić (y = a A x = b)):

((x + y) - ((x + y) -y)) = bA(x + y) -y = a {x := x + y} x- (x-y) = bAx-y = a x    — (x — y) = b A x — y = a {y := x — y} (x — y) = b A y =    a)

(x    — y) = b Ay = a) {x := x — y} x = b A y = a)

Formuła pierwsza ((x + y) — ((& + y) — y)) = b A(x + y) — y = a (otrzymana na końcu) nie jest    tą    o którą    nam chodzi. Ale zauważmy, że prawdziwa jest formuła

(x    =    a A    y = b)    ((x + y) - ((z + y) - y)) = b A (x + y) - y = a

A teraz używając reguły (3) otrzymujemy żądany wynik:

(x = a A y = b) {x := x + y\ y := x — y\ y := x — y} (x = b A y = a) Instrukcja pusta

Instrukcja pusta to pusty ciąg znaków i znaczy ’nic nie rób’. Jej znaczenie opisuje się aksjomatem

p{ }p

dla dowolnej formuły P. Jeśli napiszemy ciąg instrukcji I\\    ; I2 to jest to złożenie

trzech instrukcji przy czym drugą instrukcją jest instrukcja pusta.