CC:	
Subj:	ZTP 19.5.


1. (20 bodov)
Sformulujte a dokazte vysledky o (ne)rozhodnutelnosti problemu |divergencie|
v triede
standartnych, volnych a dosiahnutelnych schem.

2. (15 bodov)
Uvazujme triedu schem L s rozhodnutelnym problemom dosiahnutelnosti prikazu
(napr. liberalne schemy). Dokazte, alebo vyvratte tvrdenie: Problem, ci je
lubovolna schema z L priechodna je rozhodnutelny.

3. (15 bodov)
Sformulujte a dokazte vzatjomny vztah tried standartnych S a rekurzivnych R
programovych
schem z hladiska |prelozitelnosti|.

4. (15 bodov)
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]

5. (15 bodov)
Uvazujme konstrukciu cyklu
  loop S1; when b exit; S2 pool
Vyjadrite ju pomocou strukturovanych riadiacich konstrukcii, sformulujte
inferencne
pravidlo a dokazte ze je |zdrave|.

6. (10 bodov)
Formulou relacneho kalkulu vyjadrite |ciastocnu spravnost programu| P
vzhladom
na podmienky p,q a zdovodnite, ze tato formula naozaj vyjadruje pozadovanu
vlastnost.
Vyjadrite a zdovodnite inferencne Hoareovske pravidla v relacnom kalkule.

7. (15 bodov)
Vyjadrite vstupno-vystupnu operacnu a denotacnu semantiku jednoducheho
imperativneho
jazyka so "standartnymi" prikazmi priradenia, kompozicie, vetvenia a s
cyklom
 loop S1; when b exit; S2 pool

8. (15 bodov)
Sformulovat a dokazat vetu o vztahu medzi C_p_r a F_p.

9. (15 bodov)
Overte a zdovodnite, ci je funkcia f |najmensim pevnym bodom| funkcionalu
zodpovedajuceho
rekurzivnej definicii Fi nad oborom N
 f(x,y): if xy=0 then x+y+1 else dolnik

 Fi(x,y) <= if xy=0 then x+y+1 else Fi(Fi(x-1,1),y-1)

10. (15 bodov)
Definujte vypoctove pravidlo, ktore je |korektne|, ale nie je |bezpecne| a
zdovodnite
svoje tvrdenie.


Pojmy vlozene medzi |...| treba aj zadefinovat.

Atmosfera na skuske:
 Pisalo sa v A-cku, bolo nas 15, ale obsadili sme len tri rady. Privara si
sadol do
 jedneho z nich a cely cas cital SME. Iba asi dvakrat sa presiel po
miestnosti.
 Pozadoval, aby kazdy odlozil svoje veci "najmenej 5 metrov daleko"


 Vela stastia, praje CINO...dufam ze sa tam uz neukazem.




||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||



CC:	
Subj:	ZTP 26.5.


1. (15 bodov)
Sformulujte a dokazte vysledky o (ne)rozhodnutelnosti prslusnosti
lub. standartnej schemy k triede  |volnych| schem.

2. (15 bodov)
Uvazujme triedu schem N definovanu symbolmi element. prikazov {A,...}, 
symbolmi predikatov {b,...}
   P:= A| P1;P2 | if b then P1 else P2 fi | while b do P od
Predpokl. ze symboly elementarnych prikazov A su interprerovane ako funkcie
a symboly predikatov ako predikaty na mnozine stavov S. Zistite, ci je problem
divergencie v N rozhodnutelny, ale nie, svoje tvrdenie zdovodnite.

3. (15 bodov)
Problem, ci sa zastavi st. schema pre nejaku |interpretaciu| je 
nerozhodnutelny. Na zaklade toho posudte, (ne)rozhodnutelnost
dosiahnutelnosti lubovolneho priradovacieho prikazu v standartnej scheme.

4. (15 bodov)
Uvedte, ako sa odlisuju Floydova a Hoarova metoda z hladiska indukcnych
technik, charakterizujte tieto indukcne techniky 

5. (15 bodov)
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]
 
 
6. (15 bodov)
Definujte poziadavky na algebraicku strukturu semantickych domen a uvedte ich
konstrukciu vratane dokazu, ze domeny maju pozadovane vlastnosti. Vysvetlite
intuitivnu motivaciu, kt. nas priviedla k tymto poziadavkam.

7. (15 bodov)
Uvazujte semantiku charakterizovanu:
                       oo
N[ while b do S od ]= U   Psi_i
                       0 
kde
Psi_0 = lambda_sigma . dolnik
Psi_i+1 = lambda_sigma . if W[b]sigma then N[S](Psi_i(sigma)) else sigma

Plati |M| = N ? Svoje tvrdenie zdovodnite

8. (15 bodov)
Sformulujte a dokazte tvrdenia, kt. zarucuju, ze semantiku rekurz. definicie
mozno definovat pomocou najmensieho pevneho bodu.
 
9. (15 bodov)
Overte a zdovodnite, ci je funkcia f |najmensim pevnym bodom| funkcionalu
zodpovedajuceho
rekurzivnej definicii Fi nad oborom N
   f(x,y): if x=0 then y else 1
   Fi(x,y) <= if x=0 then y else if y=0 then Fi(x-1,1) else Fi(x-1,Fi(x,y-1))

10. (15 bodov)
Definujte na striktnych relaciach vlastnost 
    [ 
 R  =  S

kt. vyjadruje fakt, ze R aproximuje S (specialny pripad R a S su funkcie
musi zodpovedat aproximacii funkcii)

Pojmy vlozene medzi |...| treba aj zadefinovat.

----------------------------------------
tym, co ich to este caka drzim palce
cemi


||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||