Методика верификации программы Пример 1 Cтроим схему алгоритма ((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

2) P: inv A1 (x, y) ((x 0) (y>0)) Q: inv A2 (х, у, q, r) ((x = r+у* q) (r<у)) Пример 3) inv A3 (x, y, q, r) (x = r+y*q) 4) Список путей: а) αl: от А1 к A3; б) α2: от A3 к A3 через тело цикла; в) α3: от A3 к А2 через условие цикла. 5) Cтроим условия верификации U 1, U α2 и U α3

Пример а) путь α 1 : U 1 : inv A3 (x, у, q, r) (х=r+у*q); U 0 : inv A3 (х, у, q 0, r x) (х=х+у*0); U α1 : ((x 0) (у>0))t. б) путь α 2 : U 2 : inv A3 (х, у, q, r) (х=r+у*q); U 1 : inv A3 (х, у, qq+1, rr-у) (х=r+y*q); U 0 : (ук)(х=r+y*q); U α2 : (x=r+y×q)((yr)(x= r+y*q)).

в) путь α 3 : Пример U 1 : inv A2 (х, у, q, r) ((x=r+у*q) (r<у)); U 0 : ¬(ук)inv A2 (x, y, q, r) ( ¬(yr)((x=r+у*q) (r<у))); U α3 : (x=r+y*q)((y>r)((x=r+y*q) (y>r))). 6 Доказательство истинности условий верификации U α1 : ((x0) (y>0))t t Примем: а = (х=r+у*q), с = (ук), d = (у>r) U 2 : a(са) (a c)a ¬(а с) а (¬ а ¬ с) а t U 3 : a(d(a d)) ((a d)(a d)) t