Návrat na detail prednášky / Stiahnuť prednášku / Univerzita Komenského / Fakulta matematiky, fyziky a informatiky / Zaklady teorie programovania
Ukážky skúšok (sent.doc)
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
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.
BTW. Prepocitajte si priklady, ktore su na Stefankovicovej stranke!
Boli tam...
Karol Ruckschloss
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: 29-MAY-1997 18:27
Vec: ztp
dobry den prajem
ti stastnejsi co uz maju ztp za sebou uz tento mail asi spokojne zmazali
ostatni ak chcete citajte...
zlozenie bolo klasicke cize my Privara a 10 prikladov. za vsetky zopar
co si pametam...
rozhodnutelnost zastavenia na standardnych a dosiahnutelnych schemach
prelozitelnosti priechodnych a dosiahnutelnych
mame nejaky >loop S1 when b break S2 pool< ... skonstruujte k tomu ekvivalentnu
zalezitost v strukturovanych schemach a inferencne pravidlo... dokazte ze je
zdrave
napiste co najviac kalerabov na konstrukciu spravnych programov pomocou
Hoareovej metody
skonstruujte takto program ktory triedi pole pomocou select-sortu (* vyberie sa
minimalny prvok a da sa na zaciatok... go to *)
definujte denotacnu a operacnu vstupno vystupnu semantiku. dokazte
ekvivalenciu
zadefinujte bezpecne a korektne vypoctove pravidlo. vymyslite (opiste) vetu o
vytahu medzi nimi a dokazte
zistit ci je cosi najmensi pevny bod
dokazte C1 ->s C2 je podmnozina C1 ->m C2 kde C1 je diskretne cpo. co ak nebude
diskretne?
rozhodnutelnost izomorfizmu na volnych schemach
... no... dufam ze to mam za sebou prajem vela stastia a dobre ukryte skripta
a lucim sa
koza
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: 27-MAY-1997 12:32
Vec: ZTP ... PRIVARA
Datum a cas: 24-MAY-1996 15:51
Vec: Privara
Cafte, ja som mal Privaru hned prvy termin, sory, ze pisem az teraz. Otazky:
1. zastavenie, ekvivalencia, izomorfizmus
2. najslabsia vstupna a najsilnejsia vystupna podmienka
3. semantika nedeterminist. schem
Skuska sa niesla v priatelskom duchu ;-) nebolo to nic strasne.
Vinko
Datum a cas: 27-MAY-1997 12:32
Vec: ZTP ... PRIVARA
Adresat(i): 2i-l@pascal
Datum a cas: 29-MAY-1996 10:53
Vec: Privara 27.05.96
Zdravim fsetkyx ynformatykov
Mam to uz za sebou a prislo to tak najednou ...
Takze Privara mi privaril nasledovnymi otazkami:
1. Volne sxemy
2. Najslabsia vstupna (wp) a najsilnejsia vystupna (sp) podmienka
3. Porovnanie operacne a denotacnej semantiky (tu som poriadne
pohorel)
Eta vsjo.
Cafte.
Ugi
Datum a cas: 27-MAY-1997 12:31
Vec: ZTP ... PRIVARA
Adresat(i): 2i-l@pascal
Datum a cas: 28-MAY-1996 14:13
Vec: ZTP 27.5.`96
Zdravim !!!
Tak a tu su moje ? zo ZTP :
1. Porovnanie S a W schem.
2. Hoareho metoda (aj upnost systemu ... ).
3. Algebraicke struktury a semanticke obory
( zamerat sa na tie, ke su vyuzivane vo funkcionalnych jazykoch ...)
Nie je coho sa bat. ( Otazku aj viac krat preformuluje ... )
Este raz Zdravim ....
Stano.
Datum a cas: 27-MAY-1997 12:31
Vec: ZTP ... PRIVARA
Datum a cas: 27-MAY-1996 15:35
Vec: ZTP 27.5.
Otazky :
1.divergencia standartnych schem
2. intermitenty
3 kriteria spravnosti vyp.pravidiel
Moj predpokladany zaciatok 10.30 sa posunul o dve hodiny...
O 15.10 som skoncil za 2 ( keby som chcel prist inokedy na
1....tak..ale odmietol som)
znamky predo mnou jedna 1,jedna 2 ,dve 3 a po mne este 5 ludi....
---
/-------------------------------------------------------------------------\
| Vladimir Chovanec |
| Student of Informatics,Comenius University Bratislava,Slovakia |
|-------------------------------------------------------------------------|
\-------------------------------------------------------------------------/
Datum a cas: 27-MAY-1997 12:31
Vec: ZTP ... PRIVARA
Datum a cas: 18-MAY-1996 16:34
Vec: Privara 13.5.
Ahojte
Ja som mal:
1) Standardne schemy (definicie) a KOREKTNE definovat ich OPERACNU semantiku.
K tomuto sa ma aj cosi pytal a dost podrobne mi kontroloval tu moju semantiku,
ci by naozaj nenastal niekde problem; napr. odovzdavanie celeho programu ci
variant stavu pre paralelne priradenie.
2) Vyuzitie dokazovacich metod programov - naco je to dobre.
Rozpraval som o Hoarem (pravidla sa tu pouzivaju ODSPODU!) a o konstrukcii
spravnych programov. Nebojte, az tak vela som toho nepovedal.
3) Definicie, domeny pre funckie a pred-kecy a nakoniec KLEENEHO VETA
samozrejme s duokazom.
Myslim, ze cim mal clovek
-lepsie pisomku;
-lepsie ulohy,
tym lepsie dopadne, lebo nema az take krute otazky...
Juro+
Datum a cas: 27-MAY-1997 12:31
Vec: ZTP ... PRIVARA
Datum a cas: 16-MAY-1996 20:39
Vec: Privara 13.5. (fwd)
Nejak to asi nikomu nedoslo, takze skusam este raz:
Povodna sprava:
> Odosielatel: 4brejova
> Datum a cas: 13-MAY-1996 14:15
> Vec: Privara 13.5.
>
> Ahojte,
>
> Takze dnes bol prvy termin z Privaru, celkom uspesny, co ja viem, prvi styria
za
> jedna. Privara dosiel asi o pol desiatej, dal kazdemu tri otazky, cas na
> priprav dost dlhy (vyse hodiny) a potom si to cital a este sa k tomu nieco
> pytal ( a pozeral aj do pisomiek).
>
> Ja som mala porovnat triedu rekurzivnych a standardnych schem, Flyodovu metodu
> a bezpecne pravidla.
>
> Spytal sa ma este nieco k peblovaniu, preco sa vo Floydovi robi spatna
> substitucia a nie dopredna a aby som mu povedala nejake pravidlo, ktore je
> korektne, ale nie je bezpecne.
>
> Takze vela stastia.
Datum a cas: 27-MAY-1997 12:31
Vec: ZTP ... PRIVARA
Datum a cas: 20-MAY-1996 12:44
Vec: Privara 20.5
Ahojte.
Moje priklady:
1) Vsetko, co viem o Zastaveni,Ekvivalencii a Izomorfizme.
Tzn. definicie,vsetko pre standartne,volne,Janovove schemy + dokazy(mohol som
sa odvolavat na riesenie Divergencie)
2) Floyd. := vypoctova indukcia, ciastocna spravnost, uplna spravnost,
konstrukcia verifikacnych formul (chcel vysvetlit preco sa R a r buduju spatne)
3) Algebraicke struktury pre semanticke domeny
Vseobecne, cpo - vsetko az po striktne funkcie (aj dokazy)
Nebolo to velmi tazke.
Vela stastia Vam zela Lubor.
- rozhodnutelnost zastavenia na standardnych a dosiahnutelnych schemach
- prelozitelnosti priechodnych a dosiahnutelnych
- rozhodnutelnost izomorfizmu na volnych schemach
- Porovnajte triedy schem S a R.
- problem zastavenia pre standardne, volne a dosiahnutelne schemy
- Sformulujte a dokazte tvrdenia umoznujuce vyuzit Herbrandove interpretacie
pri dokazovani zakladnych vlastnosti programovych schem.
- Sformulujte a dokazte tvrdenie o (ne)rozhodnutelnosti problemu izomorfizmu
volnych schem. Uvedte definiciu historie vypoctu, pre ktore vase tvrdenie
plati.
{tu moze dat vlastne porovnat alebo rozhodnut hocico}
- Popiste Floydovu metodu.
- rozdiel medzi floydovou a hoareovou metodou z hladiska indukcie
popisat obe indukcie
- Sformulujte principy konstrukcie spravnych programov vyuzitim Hoareovho
kalkulu.
- 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.
- definujte denotacnu a operacnu vstupno vystupnu semantiku. dokazte
ekvivalenciu
- Porovnajte semantiky M a N.
N je def.:
N[while b do S] = najm.horna.hr. fi_i
Q_0 = lambda.sigma dolnik
Q_i+1 = lambda.sigma if W[b]sigma then N[S](fi_i(sigma))
else dolnik
- Definicia operacnej semantiky (nie vstupno-vystupna!). Len to bolo menej
zretelne zadane, co vlastne treba urobit...
- zadefinujte bezpecne a korektne vypoctove pravidlo. vymyslite (opiste) vetu o
vytahu medzi nimi a dokazte
- Sformulujte a dokazte vetu o C_p^r a F_p.
- Sformulujte a dokazte tvrdenia, ktore zarucuju, ze semantiku rekurzivnej
definicie mozno definovat pomocou najmensieho pevneho bodu.
- definovat a zdovodnit podmienku ciastocnej spravnosti v relacnom kalkule
definovat pravidla inferencneho systemu v relacnom kalkule
+ vsetky definicie :)
PRIKLADY NA POCITANIE:
~~~~~~~~~~~~~~~~~~~~~~
Priklad 1:
-----------
Ukazte, ze problem zastavenia pre standardne schemy je ciastocne
rozhodnutelny.
Priklad 2:
-----------
Zistite, ci je nasledujuca schema volna, resp. ci sa zastavi
S: begin [y1,y2,y3]:=[x,f(x),f(f(x))]
1: [y2]:=[f(y2)]
2: if p(y2) then goto 4
3: goto end
4: [y3]:=[f(y3)]
5: [y2]:=[f(y2)]
6: if p(y2) then goto end
7: [y1]:=[f(y1)]
8: if p(y1) then goto 10
9: goto 5
10: [y3]:=[f(y3)]
11: if p(y3) then goto end
12: goto 1
end [z]:=[a]
Priklad 3:
-----------
Najdite nekonecnu mnozinu M standardnych schem taku, ze pre jej lubovolnu
konecnu podmnozinu M' existuje interpretacia, pre ktoru vsetky schemy z M'
zastavia, ale neexistuje interpretacia pre ktoru zastavia vsetky schemy
z mnoziny M.
Priklad 4:
-----------
Ukazte, ze problem volnosti Janovovych schem je rozhodnutelny.
Priklad 5:
-----------
Nech S je lubovolna volna schema. Tvoria vystupne termy (po odstraneni
zatvoriek) cez vsetky mozne Herbrandovske interpretacie regularnu
mnozinu? Aku podmienku staci pridat, aby regularnu mnozinu tvorili?
Priklad 6:
-----------
Keby sme pri vypocte rekurzivneho programu prepisovali term zodpovedajuci
najpravejsiemu najvnutornejsiemu vyskytu funkcnej premennej mohli by sme
dostat iny vysledok ako pri normalnom vyhodnocovani?
Priklad 7:
-----------
Uvazujme nasledovnu rekurzivnu schemu:
begin
F(y) = if p(y) then f(y) else h(y,F(g(y)))
end [z]:=[F(a)]
Najdite ekvivalentnu standardnu schemu pouzivajucu iba tri pracovne
premenne.
Priklad 8:
-----------
Uvazujme triedu standardnych schem, ktore zastavia pre kazdu interpretaciu.
Su v triede tychto schem problemy izomorfizmu a ekvivalencie rozhodnutelne?
PREMIOVE ULOHY:
~~~~~~~~~~~~~~~
Priklad 1: (3 body)
-----------
Dokazte, ze izomorfizmus volnych schem je rozhodnutelny. (Uvazujeme
definiciu 2, teda dve kompatibilne schemy su izomorfne akk pre kazdu
interpretaciu a ohodnotenie vstupnych premennych maju rovnaku postupnost
vykonanych priradovacˇch prikazov)
Priklad 2: (3 body)
-----------
Su dosiahnutelne schemy efektivne prelozitelne do priechodnych?
Dokazte, alebo vyvratte.
Priklad 3: (3 body)
-----------
Dokazte, ze Janovove schemy su efektivne prelozitelne do volnych schem.
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
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
||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Kazda uloha je za 10 bodov.
Dufam, ze som sa nepomylil pri prepisovani.
1. Najdite ekvivalentnu standardnu schemu, pricom pouzijete najviac 4 pomocne
premenne
begin
FI(y) <= if p(y) then f(g(y))
else h(FI(g(y)),g(y))
end [z]:=[FI(a)]
2. Uvazujme triedu strukturovanych schem. Je problem divergencie pre tuto
triedu rozhodnutelny (resp. ciastocne rozhodnutelny)?
Svoje tvrdenie zdovodnite.
3. Najdite ekvivalentnu volnu schemu
begin [y1,y2]:=[x,a]
1: if p(y2) then goto end
2: if q(y1) then goto 7
3: [y1,y2]:=[g(y1),f(y2)]
4: if p(y1) then goto 2
5: [y1]:=[f(y1)]
6: goto end
7: if p(y1) then goto 11
8: [y2]:=[f(y2)]
9: if q(y1) then goto 4
10: goto 7
11: [y1,y2]:=[f(y1),f(y2)]
12: if p(y2) then goto 5
13: [y2]:=[g(y2)]
14: goto 5
end [z]:=[y1]
4. Oznacme Z triedu tych standardnych schem, ktore sa zastavia. (t.j. Z={s
patri S; s sa zastavi}, V triedu volnych schem. Dokazte, ze Z je efektivne
prelozitelne do V (neformalne popiste prislusny algoritmus).
Pisomna praca zo ZTP, 14. marca 2001
Uloha 1. (10 bodov) Najdite ekvivalentnu volnu schemu k nasledujucej
standardnej scheme. Zakreslite ju graficky (vyvojovym diagramom).
begin [y1,y2] := [f(a),a]
1: if p(y1) then goto end
2: if q(y2) then goto 7
3: [y1,y2] := [f(y1),g(y2)]
4: if p(y2) then goto 2
5: [y2] := [g(y2)]
6: goto end
7: if q(y2) then goto 11
8: [y1] := [f(y1)]
9: if q(y2) then goto 4
10: goto 7
11: [y1,y2] := [g(y1),f(y2)]
12: if p(y1) then [y1] := [f(y1)]
end [z] := [h(y1,y2)]
Uloha 2. (10 bodov) Uvazujme triedu dosiahnutelnych schem D. Je
prislusnost k trede D rozhodnutelny (resp. ciastocne rozhodnutelny)
problem? Svoje tvrdenie zdovodnite.
Uloha 3. (10 bodov) Najdite ekvivalentnu rekurzivnu schemu s minimalnym
poctom rekurzivych definici k nasledujucej standardnej scheme.
begin [y1,y2] := [x,x]
1: [y1,y2] := [f(y1),g(y2)]
2: if p(y1) then goto 4
3: goto 1
4: [y2] := [f(y1)]
5: if p(y2) then [y1] := [f(y2)]
6: if q(y1,y2) then goto end
7: goto 4
end [z] := [y2]
Uloha 4. (10 bodov) Uvazujme triedu priechodnych schem P a triedu
volnych schem V. Sformulujte a zdovodnite vztahy medzi triedami P a V
pomocou relacii podtrieda, prelozitelna trieda a efektivne prelozitelna
trieda.
Uloha 1. (15 bodov)
Uvazujme nasledujuci standardny program P.
begin [y_1,y_2] := [2,|a[2]-a[1]|]
1: [y_1] := [y_1+1]
2: if y_1 > n then goto end
3: if |a[y_1]-a[y_1-1]| > y_2 then [y_2] := [|a[y_1]-a[y_1-1]|]
4: goto 1
end [z] := [y_2]
Definujte *invarianty* a Floydovou metodou dokazte ciastocnu spravnost
programu vzhladom na vstupnu podmienku
I_B : n > 1
a vystupnu podmienku
I_E : (\forall i: 1 < i <= n : | a[i]-a[i-1] | <= z)
Uloha 2. (15 bodov)
Napiste strukturovany program, ktory dostane na vstupe cele cislo n a
pole celych cisel a[1], a[2] , ...,a[n] a bude spravny vzhladom na
vstupnu podmienku
I_B : n > 0
a vystupnu podmienku
I_E : z \in {0,1} &
(z = 1 <=> \forall i: 1 <= i < n: a[i] <= a[i+1]).
Dokazte Hoareho metodou *ciastocnu spravnost* tohto programu
vzhladom na zadanu vstupnu a vystupnu podmienku.
Uloha 3. (10 bodov)
Navrhnite inferencne pravidlo Hoarovho dokazovacieho systemnu pre
nasledujucu riadiacu strukturu (tzv. jede a pol cyklus):
do
S1;
exit when b;
S2
od
Dokazte *zdravost* navrhnuteho pravidla.
-----
Definujte ohviezdickovane pojmy!
Prednášky sú zverejnené v súlade s ustanovením § 33 ods. 1 písm. c) zákona č. 618/2003 v znení neskorších prepisov a teda výhradne na informačné účely. Prosíme Vás aby ste všetky porušenia autorských práv bezodkladne ohlásili administrátorovi. Podmienky používania
