Domaca uloha c. 5, do 30.3.1999 14:40

Dany je program P:

begin [y1,y2]:=[0,x]

1: if y2<x2 then goto end

2: [y1,y2]:=[y1+1,y2-x2]

3: goto 1

end [z1,z2]

Dokazte Floydovou metodou, ze program je ciastocne spravny vzhladom na dvojicu:
vstupna podmienka p(x1,x2): x1>=0 and x2>0
vystupna podmienka q(x1,x2,z1,z2): x1=z1*x2+z2 and 0<=z2<x2

Okrem toho vyuzite invariant

I_A(x1,x2,y1,y2): x1=y1*x2+y2 and y2>=0
ktory plati pri kazdom prechode bodom A, ktory je tesne pred vykonanim podmienkoveho prikazu na riadku 1.

Vase riesenie ma obsahovat graficku reprezentaciu schemy (diagram) so zakreslenymi deliacimi bodmi, invarianty v jednotlivych deliacich bodoch, verifikacne podmienky pre jednotlive konecne cesty v scheme (aj s ich odvodenim pomocou spatnej substitucie) a strucne zdovodnenie platnosti verifikacnych podmienok.