4962385655

Instrukcja złożona

Instrukcja złożona łączy ciąg instrukcji w jedną instrukcję i ma postać begin II; ... ; In end gdzie II, ... , In są instrukcjami. Znaczenie tej instrukcji opisuje reguła

Pi { h } Pi+1 i =    ₍₄,

Pl { begin    end } P_n+1

Przykład. Fragment programu

begin x:=x+2; y:=2*x; end;

jest złożeniem trzech instrukcji, z których ostatnia jest instrukcją pustą.

Instrukcje warunkowe

Mamy dwie instrukcje warunkowe. Pierwsza ma postać if w then I

gdzie w jest wyrażeniem typu boolowskiego a I jest instrukcją. Znaczenie tej instrukcji opisuje reguła

P Aw{I}Q P A->w Q P {if w then /} Q

tzn. instrukcja oznacza ’jeśli w to wykonaj I’. Druga instrukcja warunkowa jest rozszerzeniem pierwszej i ma postać

if w then II else 12

gdzie w jest wyrażeniem typu boolowskiego a II i 12 są instrukcjami. Znaczenie tej instrukcji opisuje reguła

P A w { II } Q P A ->w { 12 } Q P {if w then /lelse 12} Q

tzn. instrukcja oznacza 'jeśli w to wykonaj II w przeciwnym wypadku wykonaj 12’. Przykład. Jeśli x jest typu całkowitego to mamy

T { if x < 0 then abs := —x else abs := x } abs = |x|    (7)

gdzie T oznacza formułę zawsze prawdziwą. Z (1) i (3) mamy

(TAx<0)=> (—x = —x A x < 0),    (abs = —x A x < 0) => (abs = |rr|)

((—x = —x A x < 0) { abs := —x } (abs = —x A x < 0)

(TAx<0){ abs := —x } (abs = |x|)

i podobnie można pokazać, że

(T A -i(x < 0)) { abs := x } (abs := |a:|).

Zatem (7) wynika z powyższych dwóch formuł na mocy reguły (6).

Iteracja warunkowa (pętla while)

Instrukcja iteracji warunkowej ma postać