Анализ завершения программы while В do А
Пример ((x 0) (y>0)) A1A1 Начало r:=x; q:=0 (x=r+y*q) A3A3 (x=r+y*q) (r<y) A2A2 Конец - + r:=r-y; q:=q+1 y r
Пример у>0 ук rу r>0 r+у>0 Обозначения: a = (х = r + у*q) и b = (r + у > 0) (х = r + у*q) (ук)(r + у> 0) (х = r + у*q) (r + у > 0)(r + у > 0) a bb ¬ (а b) b (¬а ¬b) b t Р = Q(rr-у) (0<r+у<t 0 )(rr-у) (0<r<t 0 ) (y<r+y<t 0 +y) (0<r+y=t 0 )