Sent: 15. júna 2000 0:35 Subject: ZTP 14. juna 2000 ZTP 14. juna 2000 1. (15b) Sformulujte a dokazte vysledky o (ne)rozhodnutelnosti problemu |zastavenia| v S, V, D (stand, volne a dosiahnutelne schemy) 2. (15b) Ktoru z uvedenych konstrukcii je (nie je) mozne prelozit do |ekvivalentnej schemy| z W? Preco? W1: while b1 /\ b2 do S od W2: while b1 \/ b2 do S od W3: while not b do S od 3. (15b) Urcite a zdovodnite vztahy medzi triedami S, V, D a P (priechodne sch.) vzhladom na relacie podmozina a prelozitelnost. 4. (15b) 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)] 5. (15b) Strucne popiste Hoareovsky inferencny system na dokazovanie ciastocnej spravnosti programu a definujte pojmy: platnost a dokaz induktivnej formuly, resp. korektnost a uplnost inf. sys. 6. (10b) 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. 7. (20b) Definujte denotacnu a vstupno/vystupnu operacnu semantiku jednoducheho jazyka (priradenie, kompozicia, vetvenie, cyklus) a dokazte, ze pre vsetky programy P plati: M||P|| = O||P|| 8. (15b) Dana je nasledovna definicia vyznamu "simultanne priradenie" M||x1,x2 := t1,t2||sigma = sigma'{x2/V||t2||sigma'}; sigma'=sigma{x1/V||t1||sigma} Uvedte kontrapriklad zdovodnujuci, ze to nie je simultanne priradenie a navrhnite spravne riesenie. Zdovodnite. 9. (15b) Sformulujte a dokazte syntakticke kriteria korektnosti vypoctovych pravidiel. Uvedte pravidlo, ktore splna toto kriterium. 10. (15b) Vyjadrite V/V operacnu a rel. denotacnu semantiku jednoducheho imperativneho jazyka so stand. prikazmi priradenia, kompozicie tzv. Dijkstrovymi "guarded" prikazmi: if p1 -> S1; ... pn -> Sn if .. do p1 ->S1; ... pn -> Sn od Na ZTP si velmi vazim to, ze ako (skoro) jediny predmet si Privara uvedomil, ze na haluze podobneho razenia treba aspon dost casu. Aj ked po styroch hodinach som si nohy necitil, je to furt lepsie ako napr. nemenovane fojaky. Majte sa fajn, Tomas -- I have been infected, too. Hi! I'm a .signature virus, copy me to your .signature to help me spread. Sent: 8. júna 2000 10:45 Subject: ZTP 7.6.2000 8 Jun 00 11:09:13 +0200 (MET) by amos.sdjls.uniba.sk with SMTP; 8 Jun 2000 09:09:36 -0000 Thu, 8 Jun 2000 11:10:26 +0200 Resent-Date: Thu, 8 Jun 2000 11:08:10 +0200 (DECnet); Thu, 8 Jun 2000 11:04:49 +0200 Thu, 8 Jun 2000 11:06:53 +0200 8 Jun 2000 09:05:13 -0000 Message-ID: <003b01bfd126$088ec540$05191919@agem> Subject: ZTP 7.6.2000 Date: Thu, 8 Jun 2000 10:45:22 +0200 Zdravim Posielam Vam parafrazovane zadania zo ZTP. Dufam, ze to niekomu pomoze ... Kubo Veci medzi ! bolo treba defimovat 1) Sformulovat a dokazat tvrdenie o (ne)rozhodnutelnosti prislusnosti standartnych schem k triede !volnych schem!. 2) Boli zadane nasledujeca triad schem: P := {A | P1;P2 | if b then P1 else P2 | while b do P od } pricom b boli predikaty intepretovane nad mnozinou stavou A boli elementerne prikazy - funkcie interpretovane na mnozine stavov bolo treba urcit ci je problem !divergencie! rozhodnutelny v tejto triede 3) Uvazujme triedu schem L s !rozhodnutelnym! problemom dosiahnutelnosti prikazu (napr. liberalne schemy). Treba dokazat rozhodnutelnost divergencie priechodnych schem z L. 4) Popisat !Hoareovu a Floydovu metodu! a charkterizovat ich indukcen techniky 5) Odvodit postacujuce podmienky !ciastocnej spravnosti! schemy S (bola zadana nejaka standartna (!!!) schema) pomocou Hoareovej metody. 6) Definovat podmienky na algebraicku strukturu semantickych domen a uviest ich konstrukciu + dokaz. Vysvetlit induktivnu motivaciu,ktora nas viedla k tymto poziadavkam. 7) ... velmi vela cudzich znakov, takze sa mi to nechce pisat. Ale ide asi o to, ze mame definovanu semantiku N a mame ukazat, ze M = N. 8) Definovat vlastnu semantiku tak aby platilo platilo nieco s I/O semantikou O. 9) Sformulovat a dokazt semanticke kriterium !korektnosti vypoctovych pravidel!. Uviest vypoctove pravidla, ktore ho splnaju v jazykoch L1 a L2. 10) Nech A (na pisomke bola sigma, ale ...) je mnozina stavov a B = A zjednotenie {dolnik} (na pisomke bolo B sigma s hornym indexom dolnik). Uvazujme triedu striktnych relacii nad B (t.j. takych, ze (dolnik,y) in R <=> y=dolnik) Definujte na striktnych relaciach vlastnost R<=S (hranate mensie rovne), ktora vyjadruje fakt, ze R aproximuje relaciu S (specialny pripad, ked R a S su funkcie musi zodpovedat aproximacii funkcii) Sent: 1. júna 2000 0:23 Subject: ZTP 31.5 Caute. Tu mate co sme mali na ZTP. Inac takato presne ista pisomka uz bola niekedy v minulosti. 1. (10 bodov) Sformulujte a dokazte tvrdenia umoznujuce vyuzit Herbrandove interpretacie ------------------------- pri dokazovani zakladnych vlastnosti programovych schem. 2. (20 bodov) Sformulujte a dokazte tvrdenie o (ne)rozhodnutelnosti problemu izomorfizmu ----------- volnych schem. Uvedte definiciu historie vypoctu, pre ktore vase tvrdenie plati. 3. (15 bodov) Dokazte, ze trieda standardnych schem S sa neda prelozit do triedy struktoruovanych schem W. 4. (15 bodov) 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. --------- ------- 6. (10 bodov) Nech C1 a C2 su cpo. --- - Dokazte tvrdenie: ak C1 je diskretne cpo, potom C1 ->s C2 je podm. C1 ->m C2 - Plati toto tvrdenie, aj ked C1 nie je diskretne cpo? Dokazte, resp. uvedte kontrapriklad pre svoje tvrdenie. 7. (15 bodov) Uvazujme hypoteticky iterativny prikaz loop (b, S1, S2) definovany semantickou rovnicou M [loop (b, S1, S2)] = najm.h.hr fi_i kde fi_0 = lambda sigma.dolnik fi_i+1 = lambda sigma.if W[b]sigma then fi_i (M[S1]sigma) else M[S2]sigma Na zaklade zakladnych prikazov (priradenie, kompozicia, vetvenie, cykllus) definujte programovy segment S taky, ze plati M [loop (b, S1, S2)] = M [S]. Dokazte. Zrejme to asi bolo M||S|| = ||while b do S1 od;S2|| 8. (20 bodov) Sformulujte a dokazte tvrdenia, ktore zarucuju, ze semantiku rekurzivnej 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 prirodzenych cisel. f (x, y): if x = 0 then y else 0 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) Sformulujte vyznam zakladnych riadiacich konstrukcii kompozicie, vetvenia a iteracie v relacnom kalkule. Dokazte, ze v relacnej algebre plati vlastnost: S;(~b;S)*;b <=> (S;~b)*;S;b podciarknute treba zadefinovat Sent: 28. mája 2000 22:06 Subject: FW: ZTP.ZIP -----Original Message----- Sent: Sunday, May 28, 2000 9:58 PM Subject: Re: ZTP.ZIP tak tuto to mas, vybrala som take, co sa opakovali (je toho dost), plus tam boli aj nejake priklady, ale nemozes mat vsetko :) bye, chel --- :) Keep cool Zkontrolovano antivirovym systemem AVG (http://www.grisoft.cz). Verze: 6.0.129 / Virova baze: 61 - datum vydani: 3. 3. 2000 Sent: 25. mája 2000 0:22 Subject: ZTP -- 24.5.2000 Este nieco k tomu ZTP ... > 1. Divergencia v standartnych, volnych a dosiahnutelnych schemach. > 2. Z nerozhodnutelnosti zastavenia nejakej interpretacie satndartnej schemy > urcit, ci je rozhodnutelna dosiahnutelnost lubovolneho priradenia. > 3. W s countrom . Efektivna prelozitelnost S->WC Odpoved: ano, S sa da efektivne prelozit do W^1c. Problem robia prikazy goto, ktore mozu skocit uplne hocikam (vid kontrapriklad na preklad S -> W). Schemu z S: begin 1: if p1(y) then goto 3 2: goto end 3: if p2(y) then goto 5 4: goto end 5: [y]:=[f(y)] 6: goto 1 end Prelozime takto do W^1c: W: begin c=1 while c<=6 do if c=1 then if p1(y) then c=3 else c=2 else if c=2 then c=7 else if c=3 then if p2(y) then c=5 else c=4 else if c=4 then c=7 else if c=5 then [y]:=[f(y)] c=6 else if c=6 then c=1 od Skratka v c si pamatame riadok v scheme S, ktory prave vykonavame. c najprv nastavime na c=1 a vbehneme do cyklu while. Kym je c<=6 (este sme sa nedostali na koncovy prikaz), tak postupne otestujeme c a vykoname prislusny prikaz (riadok) zo schemy S. A nastavime c na dalsi riadok, ktory sa ma vykonat. > 4. Standartna schema, sformulovat podmienky pre uplnu spravnost. Bola > zadefinovana 4 riadkova schema. > 5. Hoareho infernalne pravidla. Napisat ich + co znamena{p}P{q}. > 6. Napisat strukturovanymi prikazmi loop S1; when b exit; S2 pool. Urobit > inferencne pravidlo a dokazat, ze je zdrave. > 7. Semantiky O,M pre loop. > 8. f(x):if x>100 then x-10 else gulova sedma( alebo cervene eso?) ci je > najmensi pevny bod pre Fi<=if x >100 then x-10 else Fi(Fi(x+11)) Udajny pevny bod bol f(x)=if x>100 then x-10 else dolnik. Staci vsak vypocitat f(100) a Fi(100) a vyjdu rozne vysledky. > 9. fp vs. Cpr > 10. Nebezpecne korektne pravidlo. Take pravidlo je napr. SPOS - sekvencny POS. Najprv vyberie vsetky vyskyty Fi, ktore bude nahradzat a potom ich jeden po druhom (rozumej postupne) nahradi. SPOS je korektny, lebo po konecne vela krokoch nahradi vsetky vyskyty Fi presne ako POS (a ten je korektny). SPOS ale nie je bezpecny. Niektora z tych substitucii nemusi byt bezpecna (vid definicia bezpecnej substitucie), lebo moze substituovat "nepotrebne" Fi. Asi tolko ... Bodo Sent: 24. mája 2000 17:46 Subject: Zdravotne Tazko Postihnuti 24.5.2000 utrzky Ak si pametame, tak: 1. Divergencia v standartnych, volnych a dosiahnutelnych schemach. 2. Z nerozhodnutelnosti zastavenia nejakej interpretacie satndartnej schemy urcit, ci je rozhodnutelna dosiahnutelnost lubovolneho priradenia. 3. W s countrom . Efektivna prelozitelnost S->WC 4. Standartna schema, sformulovat podmienky pre uplnu spravnost. Bola zadefinovana 4 riadkova schema. 5. Hoareho infernalne pravidla. Napisat ich + co znamena{p}P{q}. 6. Napisat strukturovanymi prikazmi loop S1; when b exit; S2 pool. Urobit inferencne pravidlo a dokazat, ze je zdrave. 7. Semantiky O,M pre loop. 8. f(x):if x>100 then x-10 else gulova sedma( alebo cervene eso?) ci je najmensi pevny bod pre Fi<=if x >100 then x-10 else Fi(Fi(x+11)) 9. fp vs. Cpr 10. Nebezpecne korektne pravidlo. Plus bolo treba zadefinovat nejake podciarknute pojmy z vyssie uvedenych. S pozdravom Kolektiv repelentov. Sent: 17. mája 2000 19:32 Subject: ztp - skuska (fwd) ---------- Forwarded message ---------- Date: Sat, 6 May 2000 15:34:57 +0200 Subject: ztp - skuska (fwd) Resent-Date: Sat, 6 May 2000 15:35:00 +0200 Povodna sprava: Datum a cas: 27-APR-1999 16:50 Vec: ztp - skuska Datum a cas: 26-MAY-1997 9:46 Vec: Privara - 22.5. Ahojte, sice trochu neskor, ale predsa som sa odhodlala podelit sa s Vami o dojmy zo skusky z teorie programovania... Tak tu su priklady: (Mozno boli mierne ine, zadania sme totiz vratili, takze mozno na nieco aj zabudnem.) 1. Dok., ze dve Janov. sch. su ekviv. prave vtedy, ked sa pre kazdu herb. interpr. bud obe nezastavia alebo sa zastavia a plati val(S1,I) = val(S2,I) = f_k f_{k-1} ... f_1 x. 2. Porovnajte triedy schem S a R. 3. Popiste Floydovu metodu. 4. Porovnajte sposoby indukcie v Hoare a Floydovi. 5. Def. zdrave pravidlo. Urcte, ci nasl. su zdrave (a dok.): nieco na sposob {p} repeat S until b {q} ale predpoklady si nespomeniem... nieco na sposob {p} while b do S {q} - tiez si predpoklady nespominam... (spytajte sa niekoho ineho) 6. Porovnajte semantiky M a N. N je def.: N[while b do S] = najm.horna.hr. fi_i Q_0 = omega Q_i+1 = alfa.sigma if W[b]sigma then N[S](fi_i(sigma)) else dolnik 7. Sformulujte a dokazte vetu o C_p^r a F_p. 8. Bol dany nejaky funkcional a mozno pevny bod. Bolo treba urcit, ci je to najm. pevny bod. 9. Definicia operacnej semantiky (nie vstupno-vystupna!). Len to bolo menej zretelne zadane, co vlastne treba urobit... 10. Bolo treba urcit, ci je pravidlo SPOS korektne alebo bezpecne. SPOS je sekvencny POS, t.j. najskor sa vyberu fi pomocou POS-u a potom sa v kazdom dalsom kroku zlava vzdy jedno fi nahradi. Takze nam prajem vela stastia, bude nam ho treba. ivona. Este cosi. Rata sa cca 3 hodiny, no my sme tam boli nieco vyse - 3+1/4, mozno az 3+1/2, teda ked sa budete tvarit, ze nechcete odovzdavat a jeho vyzvy budete ignorovat, je to celkom uspesna taktika. ------------------------------------------ Datum a cas: 19-MAY-1997 11:00 Vec: ztp Nazdar, kedze som bol ucastnikom skusky zo ZTP vo stvrtok 15.5., bol som poproseny o zdelenie mojich pocitov. Tu su: Bolo 10 prikladov, vacsinou po 15 bodov, ale boli tam aj za 10 a 20, jeden za 5. Treba sa nasprtat definicie, nakolko v niektorych prikladoch su urcite pojmy podciarknute a je treba ich zadefinovat. Oblast prikladov: I. Schemy - rozhodnutelnost, ... (bola tam nejaka trieda schem a bolo treba urcit, ci je v tejtp triede rozhodnutelna nejaka vlastnost - prekladom do janovovych schem). Z prvej state ma uz nic nenapada. II. Veci okolo inferencnych pravidiel, zadefinovat ich, ... Dokazovat spravnost sme nemali. III. Hovoria vam nieco funkcionaly? Ak nie, tak to zmente, pretoze tam toho okolo nich bolo dost. Sformulovat a dokazat vetu o pevnom bode a podobne. ------------------------------------------ Subject: ZTP (20.5.) add-on Date: Thu, 21 May 1998 14:56:42 +0000 (GMT) Caute ludia! Cital som Borov mail a trochu som podoplnal, co som si pamatal. 1. Boli zadane nasledujeca triad schem: P ::= {A | P1;P2 | if b then P1 else P2 | while b do P od } pricom b boli predikaty intepretovane nad mnozinou stavou A boli elementerne prikazy - funkcie interpretovane na mnozine stavov bolo treba urcit ci je problem divergencie rozhodnutelny v tejto triede 2. problem zastavenia pre standardne, volne a dosiahnutelne schemy 3. definovat a zdovodnit podmienku ciastocnej spravnosti v relacnom kalkule definovat pravidla inferencneho systemu v relacnom kalkule 4. rozdiel medzi floydovou a hoareovou metodou z hladiska indukcie popisat obe indukcie 5. definovat zdrave pravidlo definovat cyklus 'repeat S until b' ako inferencne pravidlo a dokazat, ze je zdrave pricom repat bol definovany: repeat S until b = S; while ~b do S od (to = chapte ako ekvivalenciu - tri ciarky nad sebou) 6. definovat denotacnu semantiku M je dana semantika N: N||while b do S od|| = najm. horna cast z retazca psi_i psi_0 = lambda.sigma dolnik psi_i+1 = lambda.sigma if W||b||sigma then N||S||(psi_i(sigma)) else sigma treba urcit ci N=M a zdvovodnit 7. definovat operacnu semantiku C: Stat -> (Sigma -> Sigma^nekonecno) 8. sformulovat a dokazat vetu o c_p^r a f_p 9. zistit ci je dany pevny bod najmensim a zdovodnit 10. definovat korektne a bezpecne pravidlo definovat korektne, ale nie bezpecne pravidlo Dalej boli podciarknute nejake pojmy v otazkach a bolo ich treba definovat ako napr.: zdrave pravidlo semantika M (denotacna) a podobne veci... A este jedna rada na zaver sadnite si ako chcete len nie moc na husto napr. vedla mna bola volna len 1 stolicka a hned dalsi kolega. Privara na zaciatku prenesie nieco ako, ze by ste mohli vyuzit cely priestor prednaskovej miestonsti ale treba to ignorovat. Casu bolo dost (aspon pre mna) bez vaznejsieho prehovarania sme to natiahli na 3 1/2 hod. Takze pohoda. Mirec ------------------------------------------ Date: Wed, 27 May 1998 17:37:05 MET Subject: ZTP 27.5. 1. (10 bodov) Sformulujte a dokazte tvrdenia umoznujuce vyuzit Herbrandove interpretacie ------------------------- pri dokazovani zakladnych vlastnosti programovych schem. 2. (20 bodov) Sformulujte a dokazte tvrdenie o (ne)rozhodnutelnosti problemu izomorfizmu ----------- volnych schem. Uvedte definiciu historie vypoctu, pre ktore vase tvrdenie plati. 3. (15 bodov) Dokazte, ze trieda standardnych schem S sa neda prelozit do triedy struktoruovanych schem W. 4. (15 bodov) 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. --------- ------- 6. (10 bodov) Nech C1 a C2 su cpo. --- - Dokazte tvrdenie: ak C1 je diskretne cpo, potom C1 ->s C2 je podm. C1 ->m C2 - Plati toto tvrdenie, aj ked C1 nie je diskretne cpo? Dokazte, resp. uvedte kontrapriklad pre svoje tvrdenie. 7. (15 bodov) Uvazujme hypoteticky iterativny prikaz loop (b, S1, S2) definovany semantickou rovnicou M [loop (b, S1, S2)] = najm.h.hr fi_i kde fi_0 = lambda sigma.dolnik fi_i+1 = lambda sigma.if W[b]sigma then fi_i (M[S1]sigma) else M[S2]sigma Na zaklade zakladnych prikazov (priradenie, kompozicia, vetvenie, cykllus) definujte programovy segment S taky, ze plati M [loop (b, S1, S2)] = M [S]. Dokazte. 8. (20 bodov) Sformulujte a dokazte tvrdenia, ktore zarucuju, ze semantiku rekurzivnej 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 prirodzenych cisel. f (x, y): if x = 0 then y else 0 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) Sformulujte vyznam zakladnych riadiacich konstrukcii kompozicie, vetvenia a iteracie v relacnom kalkule. Dokazte, ze v relacnej algebre plati vlastnost: S;(~b;S)*;b <=> (S;~b)*;S;b podciarknute treba zadefinovat Sent: 17. mája 2000 19:32 Subject: ZTP 19.5. (fwd) ---------- Forwarded message ---------- Date: Sat, 6 May 2000 15:34:54 +0200 Subject: ZTP 19.5. (fwd) Resent-Date: Sat, 6 May 2000 15:34:56 +0200 Povodna sprava: Datum a cas: 20-MAY-1999 11:57 Vec: 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. Sent: 17. mája 2000 19:31 Subject: ZTP 26.5. (fwd) ---------- Forwarded message ---------- Date: Sat, 6 May 2000 15:34:51 +0200 Subject: ZTP 26.5. (fwd) Resent-Date: Sat, 6 May 2000 15:34:53 +0200 Povodna sprava: Datum a cas: 26-MAY-1999 20:46 Vec: 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