4962385653

gdzie a jest zmienną a w jest wyrażeniem tego samego typu co zmienna a.

Przykład. Przy deklaracji zmiennych

var a,x:real;

p:boolean; n,m:integer;

możemy na przykład dokonać takich podstawiań

a:=(x+n)/2; n:=n¹m; n:=n+2;

p:=(a<x) or (n=0);

Opis logiczny instrukcji. Znaczenie tej instrukcji opisuje aksjomat

P(a\w){ a := w }P    (1)

gdzie P jest dowolną formułą, a P(a\w) jest formułą powstałą z P przez zastąpienie wszystkich¹ wystąpień zmiennej a wyrażeniem w. Cała formula (1) oznacza, że jeśli przed wykonaniem instrukcji a:=w spełniony jest warunek P(a\w) to po wykonaniu instrukcji a: =w spełniony jest warunek P.

Przykłady zastosowania aksjomatu (1):

(6 = (x + ń) + l){a := x +    = a + 1)

czyli, jeśli przed wykonaniem instrukcji a := x + n zachodzi (b = (x + n) + 1) to po jej wykonaniu zachodzi (6 = a + 1).

(n+l<fcAn+l> 0){n := n + l}(n < k A n > 0)

czyli, jeśli przed wykonaniem instrukcji n := n + 1 zachodzi (n+1 < k A n + 1 >0) to po jej wykonaniu zachodzi (n < k A n > 0).

Innymi słowy instrukcja podstawiania jest wykonywana w ten sposób, że najpierw wyliczamy wartość wyrażenia po prawej stronie a potem wstawiamy wyliczoną wartość na zmienną po lewej stronie.

Do opisu znaczenia instrukcji przypisania użyliśmy zapisu logicznego. Ogólnie zapis logiczny ma postać

P{I}Q

gdzie P i Q są formułami a / instrukcją, i oznacza, że jeśli przed wykonaniem instrukcji I prawdziwa jest formuła P to po jej wykonaniu (o ile wykonywanie instrukcji się zakończy) prawdziwa jest formuła Q. P nazywamy warunkiem początkowym a Q warunkiem końcowym.

Prawdziwa jest następująca reguła wnioskowania

P{i}Q, Q{J}R    ₍₀,

P{I,J}R    ^u

Ta reguła, jak i inne reguły wnioskowania, pozwala wywnioskować formułę pod kreską o ile ustalimy prawdziwość formuł nad kreską. W tym przypadku reguła (2) wyraża to, że ; łączy dwie instrukcje nic w nich nie zmieniając.

1

Są tu pewne ograniczenia które nas w praktyce nie będą dotyczyć. Gdy formuła P ma kwan-tyfikatory to wyrażenie w wstawiamy na tak zwane wolne wystąpienia zmiennej a. Ponadto, takie podstawienie nie może wiązać żadnej ze zmiennych występujących w wyrażeniu w.