Základy teórie programovania

Cvičenia: 1 | 2 | 3 | 4 | 5 | 6 | 7 | 8 | 9 | 10 | 11 | 12
Domáce úlohy | Prémie | Body | Krúžky | Učebné texty

1. Majme 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]

   Čo ráta program P₁?
2. Napíšte štandardnú schemu S, ktorej interpretáciou vznikne P₁.
3. Nájdite interpretáciu I₁ tak, aby platilo P₁=(S, I₁).
4. Nájdite interpretáciu I₂ tak, aby program P₂=(S, I₂) počítal funkciu élog₂xů.
5. Popíšte históriu výpočtu programu P₁ pre ohodnotenie vstupu v[x ¬ 7] pomocou konfigurácii.
6. Napíšte Herbrandove univerzum pre schému S.
7. Nájdite zladenú Herbrandovu interpretáciu pre výpočet z úlohy 5.

1. Dokážte, že dve kompaktibilné schémy S₁, S₂ sú ekvivalentné práve vtedy, ak pre každú herbrandovskú interpretáciu buďto programy (S₁, I_H), (S₂, I_H) oba divergujú, alebo oba zastavia a val(S₁, I_H, "x") = val(S₂, I_H, "x").
2. Majme schému S:

   begin [y1,y2]:=[a,a]
   1:    if p(y1) then goto end
   2:    [y1]:=[f(y1)]
   3:    if p(y1) then goto end
   4:    [y1,y2]:=[f(y1),f(y1)]
   5:    if p(y1) then goto 7
   6:    goto end
   7:    if p(y2) then goto 4
   8:    goto 2
   end   [z]:=[a]

   1. Nájdite I, pre ktorú P = (S, I) diverguje.
   2. Ukážte, že pre každú I s konečnou doménou program (S, I) zastaví.
3. Dokážte, že každá Janovova schéma sa dá preložiť do ekvivalentnej voľnej janovovej schémy.

1. Dokážte, že problém divergencie štandardných schém nie je ani čiastočne rozhodnuteľný.
2. Dokážte, že problém zastavenia štandardných schém je čiastočne rozhodnuteľný. Popíšte výpočet procedúry riešiacej problém zastavenia štandardných schém pre vstupnú schému S:

   begin [y]:=[a]
   1:    if p(y) then goto end
   2:    [y]:=[f(y)]
   3:    goto 1
   end   [z]:=[y]

3. Dokážte, že problém ekvivalencie štandardných schém nie je ani čiastočne rozhodnuteľný.
4. Dokážte, že problém izomorfiznmu štandardných schém nie je ani čiastočne rozhodnuteľný.
5. Dokážte, že problém divergencie voľných schém je rozhodnuteľný.
6. Dokážte, že problém zastavenia voľných schém je rozhodnuteľný.
7. Dokážte, že problém dosiahnuteľnosti príkazu v štandarnej schéme je čiastočne rozhodnuteľný.

1. Pokúste sa preložiť nasledujúce časti štandarných schém do štrukturovaných schém:
   • if b₁ Ú b₂ then S₁ else S₂
   • if b₁ Ů b₂ then S₁ else S₂
   • if Řb then S₁ else S₂
   • while b₁ Ú b₂ do S
   • while b₁ Ů b₂ do S
   • while Řb do S
2. Určte vzťahy inklúzie, preložiteľnosti a efektívnej preložiteľnosti medzi triedami dosiahnuteľných, voľných a štandardných schém.
3. Ak existuje, tak zostrojte ekvivalentnú štandardnú schému k rekurzívnej schéme S:

   begin
         F(y) Ü if p(y) then f(y) else h(F(g(y)))
   end   [z]:=[F(a)]
   				

1. 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?
2. Nájdite najslabšiu vstupnú a najsilnejšiu výstupnú podmienku pre program P.
3. Dokážte čiastočnú správnosť programu P vzhľadom na špecifikáciu z predchádzajúcej úlohy Floydovou metódou.
4. Určte deliace body programu P.
5. Pre tieto body zostrojte invarianty.
6. Zostrojte verifikačné podmienky pre všetky cesty medzi deliacimi bodmi.
7. Verifikačné podmienky dokážte.

1. 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?
2. Dokážte zastavenie programu P vzhľadom na vstupnú podmienku p(x): x₁>0 & x₂>0 modifikoanou Floydovou metódou.
3. Určte deliace body programu P.
4. Pre tieto body zostrojte invarianty a miery.
5. Zostrojte verifikačné podmienky pre všetky cesty medzi deliacimi bodmi.
6. Verifikačné podmienky dokážte.

1. 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?
2. Nájdite najslabšiu vstupnú a najsilnejšiu výstupnú podmienku pre program P.
3. Dokážte čiastočnú správnosť programu P vzhľadom na špecifikáciu z predchádzajúcej úlohy Hoareovou metódou.
4. Zostrojte invarianty.
5. Dokážte verifikačné podmienky.

1. 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=F_n.

1. Popíšte zmysel použitia cpo ako sémantického modelu.
2. Uveďte základné vlastností cpo.
3. Pokúste sa rozšíriť diskrétne sémantické obory (napr. celé čísla) na cpo.
4. Rozhodnite či sú množiny {(0,1),Ł}. {á0,1),Ł} a {á0,1ń,Ł} cpo. Prečo?
5. Navrhnite rozšírenie množiny funkcii na cpo.
6. Zachovajú sa vlastnosti cpo, ak v predchádzajúcej úlohe zúžime množinu na striktné funkcie?.

1. Čo je to sémantika?
2. Aký význam má skúmať sémantiky?
3. Existuje ku každéhému jazyku iba jedna správna sémantika?
4. Aká je to kompozičná sémantika?
5. Aký je rozdiel medzi denotačnou a operačnou sémantikou?
6. Navrhnite úplnú operačnú semantiku imperatívnych programov z cyklami.

Cvičenia odpadli. Voľno pred Veľkonočnými sviatkami.

1. Čo je to rekurzívny program?
2. Popíšte syntax rekurzívnych programov.
3. Čo je interpertáciou rekurzívnej definície?
4. Vysvetli pojem funkcionál.
5. Čo je to pevný bod funkcionálu?
6. Navrhni postačujúce kritérium na existenciu pevného bodu.
7. Najdi pevný bod funkcionálu
   • t[F](x): if x=0 then 0 else 1+F(x-1).
8. Vypočítajte výsledok rekurzívneho programu

   begin
     F(x) Ü if x=0 then 0 else 1+F(x-1)
   end [z]:=[F(x)]

   pre ohodnotenie vstupu d(x ¬ 3).

Stránky jednotlivých krúžkov

• Krúžok 2i1
• Krúžok 2i2
• Krúžok 2i3
• Krúžok 2i4

Tu si môžete stiahnuť učebné texty v elektronickej forme.

• ztp.ps