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