Cvičenie 5 (9. marca 2000)

Uvažujme program P:

begin [y1,y2]:=[0,x1]
1:    if y2<x2 then goto end
2:    [y1,y2]:=[y1+1,y2-x2]
3:    goto 1
end   [z1,z2]:=[y1,y2]

Čo počíta program P? 
Nájdite najslabšiu vstupnú a najsilnejšiu výstupnú podmienku pre program P. 
Dokážte čiastočnú správnosť programu P vzhľadom na špecifikáciu z predchádzajúcej úlohy Floydovou metódou. 
Určte deliace body programu P. 
Pre tieto body zostrojte invarianty. 
Zostrojte verifikačné podmienky pre všetky cesty medzi deliacimi bodmi. 
Verifikačné podmienky dokážte.





Cvičenie 6 (16. marca 2000)

Uvažujme program P:

begin [y1,y2]:=[x1,x2]
1:    if y1=y2 then goto end
2:    if y1>y2 then goto 5
3:    [y2]:=[y2-y1]
4:    goto 1
5:    [y1]:=[y1-y2]
6:    goto 1
end   [z]:=[y1]

Čo počíta program P? 
Dokážte zastavenie programu P vzhľadom na vstupnú podmienku p(x): x1>0 & x2>0 modifikoanou Floydovou metódou. 
Určte deliace body programu P. 
Pre tieto body zostrojte invarianty a miery. 
Zostrojte verifikačné podmienky pre všetky cesty medzi deliacimi bodmi. 
Verifikačné podmienky dokážte.





Cvičenie 7 (23. marca 2000)

Uvažujme program P:

begin [y1,y2]:=[1,a[1]]
  while y1Łn do
    [y1]:=[y1+1];
    if y2>a[y1] then
      [y2]:=[a[y1]]
  od
end [z]:=[y2]

Čo počíta program P? 
Nájdite najslabšiu vstupnú a najsilnejšiu výstupnú podmienku pre program P. 
Dokážte čiastočnú správnosť programu P vzhľadom na špecifikáciu z predchádzajúcej úlohy Hoareovou metódou. 
Zostrojte invarianty. 
Dokážte verifikačné podmienky.





Cvičenie 8 (30. marca 2000)

Metódou konštrukcie správnych programou navrhnite program, ktorý bude vyhovovať nasledujúcej špecifikácii. 

vstupná podmienka p(n): nł0 
výstupná podmienka q(n,z): z=Fn.
------------------------------------

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&gt0
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.
-------------------------------------
Domáca úloha č. 4 do 16.3.2000 16:30

Napíšte program, ktorý vyhovuje nasledujúcej špecifikácii. 

vstupná podmienka p(x): xł0 
výstupná podmienka q(x,z): z=x!

Samozrejme bez použitia funkcie, ktorá by vrátila faktoriál. Formálne dokážte správnosť vášho programu. Teda určte deliace body, nájdite invarianty, zostrojte verifikačné podmienky a ukážte, že platia. 

(3 body)





Domáca úloha č. 5 do 30.3.2000 16:30

Napíšte program, ktorý vyhovuje nasledujúcej špecifikácii. 

vstupná podmienka p(x): xł0 
výstupná podmienka q(x,z): z=x!

Samozrejme bez použitia funkcie, ktorá by vrátila faktoriál. Formálne dokážte správnosť vášho programu pomocou Hoarovej metódy. Teda pomocou axiomy priradenia a odvodzovacích pravidiel napíšte dokaz formuly {p}P{q}, kde P je váš program. (Nezabudnite dokázať a verifikačné podmienky.) 

(3 body)





Domáca úloha č. 6 do 6.4.2000 16:30

Metódou konštrukcie správnych programpov nájdite program, ktorý dostane na vstupe dve celé čísla x1 a x2, a ktorý vyhovuje nasledujúcej špecifikácii. 

vstupná podmienka p(x1,x2): x2ł0 
výstupná podmienka q(x1,x2,z): z = x1x2, (čítaj: x1 na x2)

Použite iba operácie súčinu, súčtu(príp. rozdielu), bitový šift (teda delenie alebo násobenie mocninou 2). Navyše sa kvôli efektívnosti pokúste použiť čo najmenej operácii z vyššie uvedenej množiny. Ak pri konštrukcii použijete pravidlo následku, nezabudnite dokázať použité implikácie zo špecifikačného jazyka. 

(3 body)

------------------------------------
Domáca úloha č. 3 do 28. marca 2001

Daný je štandardný program P:

begin [y1,y2]:=[1,1]

1:    if y2 ł x then goto end

2:    [y1,y2]:=[y1 + 1,(y1 + 1)2]

3:    goto 1

end   [z]:=[y1]

 

Floydovou metódou formálne dokážte správnosť programu P vhľadom na podmienky: 

vstupná podmienka p(x): x > 0 
výstupná podmienka q(x,z): (z - 1)2 < x Ł z2 (t.j. z = éÖxů)

Teda určte deliace body, nájdite invarianty, zostrojte verifikačné podmienky a ukážte, že platia. 




Domáca úloha č. 4 do 4. apríla 2001

Daný je štrukturovaný program P:

begin [y1,y2]:=[1,1]

  while y2 < x do

    [y1,y2]:=[y1 + 1,(y1 + 1)2]

  od

end [z]:=[y1]

Hoarovou metódou formálne dokážte správnosť programu P vhľadom na podmienky: 

vstupná podmienka p(x): x > 0 
výstupná podmienka q(x,z): (z - 1)2 < x Ł z2 (t.j. z = éÖxů)

Teda pomocou axiomy priradenia a odvodzovacích pravidiel napíšte dokaz formuly {p}P{q}. 
---------------------------------------
Na zaklade Floydovej metody sformulujte postacujuce podmienky |ciastocnej
spravnosti| schemy S vzhladom na vst. podmienku p(x), vystupnu podmienku
q(x,z) a invariant Ii(x,y) v prislusnych deliacich bodoch i.

S:

   begin: [y1, y2] := [x,a]
       1: if p1(y1) then goto 4
       2: [y1,y2] := [f1(y1), f2(y2)]
       3: goto 1
       4: [y2] := [g2(y1)]
       5: if p2(y2) then goto end
       6: [y1,y2] := [g1(y1),g2(y2)]
       7: goto 1
     end: [z] := [g1(y1)]
-----------------------------------------
Rozhodnite, ci su nasledovne inf. pravidla zdrave:

         {p} S {p}
----------------------------
{p} repeat S until b {p & b}


{p} S1 {p} {p} S2 {p}
-----------------------------------------
{p} loop S1; when b exit; S2 pool {p & b}

Svoje tvrdenie dokazte, alebo vyvratte kontraprikladom.

Urcite a zdovodnite, ci su nasledujuce dve inferencne pravidla zdrave:
                                                                            
                        --------
{p \/ (q & q & ~b)} S {q}           {p & b} S {(p & ~b) => q}
-----------------------             -------------------------
{p} repeat S until b {q}            {p} while b do S od {q}

5. (15 bodov)
Sformulujte principy konstrukcie spravnych programov vyuzitim Hoareovho
kalkulu.                                                                  
--------------------------------
Na zaklade formalneho dokazu pomocou Hoareovej metody odvodte postacujuce
podmienky
|ciastocnej spravnosti| schemy S vzhladom na vstupnu podmienku p(x) a
vystupnu
podm. q(x,z) a invariant I(x,y1,y2,y3)
S: begin [y1,y2,y3]:=[a,x,c]
     1: [y2]:=[f(y2,y3)]
     2: if b(x,y2) then goto end
     3: [y1,y3]:=[g1(y1),g2(y3)]
     4: goto 1
   end [z]:=[y1]
---------------------------------
Uvazujme konstrukciu cyklu
  loop S1; when b exit; S2 pool
Vyjadrite ju pomocou strukturovanych riadiacich konstrukcii, sformulujte
inferencne
pravidlo a dokazte ze je |zdrave|.
--------------------------------
Na zaklade formalneho dokazu pomocou Floydovej metody odvodte postacujuce
podmienky |totalnej spravnosti| schemy S vzhladom na vstupnu podmienku p(x) a
vystupnu podmienku. q(x,z) a invariant I(x,y1,y2,y3)
 S: begin [y1,y2,y3]:=[a,a,c]
    I1
      1: [y2]:=[f(y2,y3)]
      2: if b(x,y2) then goto end
      3: [y1,y3]:=[g1(y1),g2(y3)]
      4: goto 1
    end [z]:=[y1]
--------------------------------