Реферат: Семантика оператора case

"i: 1 £ i £ n : {PÙB_i } S {P}

PÙØBBÞR

Доказать,что в следующих циклах Р - инвариант и цикл заканчивается в нужном состоянии R:

1.

{0 £ n }

i:=0 ;

{P: 0 £ i £ n Ù xÏ b [0: i-1]}

while (i < n) and (x¹ b[i]) do i:=i+1;

{R: (0 £ i £ n Ù x= b[i])Ú( i = n Ù xÏ b [0: i-1])}

2.

{0 < n }

i:=1 ;

{P: 0 < i £ n Ù ($p: i=2^p )}

while 2*i £ n do i:=2*i ;

{R: 0 < i £ n< 2*i Ù ($p: i=2^p )}.