4962385657

while w do I

gdzie w jest wyrażeniem typu boolowskiego a I jest instrukcją.

Przykład.

while x<y do begin x:=x+2; y:=y+i end

Znaczenie tej instrukcji opisuje reguła

PAw{I } P P { while w do I } P A ~>w

Formułę P spełniającą przesłanki tej reguły nazywamy niezmiennikiem pętli. Instrukcja ta powoduje, że instrukcja I jest wykonywana dopóki warunek w jest spełniony. Zauważmy, że w regule (8) warunek P występuje zarówno w warunku początkowym jak i końcowym (stąd jego nazwa niezmiennik). Umiejętny wybór takiego niezmiennika jest zazwyczaj najistotniejszym problemem przy dowodzeniu częściowej poprawności programów.

Przykład. Pokażemy, że po wykonaniu poniższego fragmentu programu zmienna iloczyn ma wartość m*n. Wszystkie zmienne są typu całkowitego.

if n<0 then a:=-n else a:=n;

k:=0;

x:=0;

while k<a do begin x:=m+x; k:=k+l end;

if n<0 then iloczyn:=-x else iloczyn:=x

Mamy

T { if n<0 then a:=-n else a:=n } (a = |n|)

oraz

(a = |n|) { k:=0; x:=0 } (k = 0 A x = 0 A (a = |n|)). Prawdziwa jest następująca formuła

(fc = 0Ax = 0A(a= |n|))    (k < a Ax = k * m)

Ponadto dla formuły Q = (k<aAx = k* m) mamy

Q A (k < a) { x:=m+x;k:=k+l } Q Zatem Q jest niezmiennikiem pętli i na mocy reguły (8) mamy

Q { while k<a do begin x:=m+x;k:=k+l end } (-i(fc < a) A Q).