A   Mějme následující algoritmus se vstupní a výstupní doménou R:
input x i <— x; z <(- 0; while   |_±J   ť^ 0 do
z <(— z + x;
i «— i - 1; endwhile; output z
Vzhledem ke kterým z následujících vstupních podmínek je algoritmus konvergentní?
a) ip(x) = x G R                                            b) (^(x) = x G M+
c) (^(x) exgZ                                            d) (^(x) = x G N
Vzhledem ke kterým z uvedených vstupních podmínek a výstupní podmínce
7/^(x, z) = z = x2 je algoritmus parciálně korektní?
Najděte vstupní podmínku, pro kterou je algoritmus parciálně korektní vzhledem k libovolné výstupní podmínce.
A   Napište definici funkce minimum pro nalezení nejmenšího prvku v neprázdné konečné posloupnosti čísel. Posloupnost je reprezentovaná neprázdným seznamem. Funkce bude mít jednu bázovou (nerekursivní) větev pro jednoprvkovou posloupnost a jednu rekursivní větev pro aspoň dvouprvkovou posloupnost s prvním prvkem x, druhým prvkem y a zbytkem posloupnosti s.
A   Dokažte parciální korektnost funkce minimum vzhledem ke vstupní podmínce (p(s) = s je neprázdný seznam celých čísel a výstupní podmínce s, n) =  n leží v s a pro všechna m ze seznamu s platím > n.
A   Dokažte parciální korektnost algoritmu pro seřazení prvků v dvouprvkovém poli A indexovaném od jedničky vzhledem k podmínkám: <p(A) = A je dvouprvkové pole celých čísel
' nx, y], [p, q]) = p < q A (p, q) ß permutací (x, y]
input A
if   (A[l]   > A [2])   then z <- A[l]; A[l]   <r- A[2]; A[2]   <- z; endif output A
A   Napište definici funkce power, která má dva parametry, zGl- {0},^ G N, a počítá mocninu zn.
A   Formulujte vstupní a výstupní podmínku pro funkci power.
A   Najděte hodnotu, která v cyklu ostře klesá (v každém průchodu aspoň o 1), a zdůvodněte konvergenci vzhledem ke vstupní podmínce.
A   Najděte v zápisu funkce power invariant cyklu a pomocí něho dokažte parciální korektnost.
Jiná varianta funkce power:
power z 0    =    1
power z n = if odd n then z * t else t
where t = power (z*z) (n fdivf 2)
A   Dokažte konvergenci funkce power vzhledem ke vstupní podmínce
(f((z, n)) = z G R — {0} A n G N. Která hodnota v definici ostře klesá? Proč nemůže
být záporná?
A   Funkce součet vypočte pro danou posloupnost A\,A<i,... celých čísel součet
A\ + • • • + Ak, v němž jsou všechny sčítance nenulové a A^+i = 0 je prvním výskytem
nuly v posloupnosti.
function součet   (A:posl):   integer; var k:   integer;   s:   integer; begin k   :=  1;     s   := 0;
while A [k]   ť^ 0          /*%nv*/
do begin s   := s + A [k] ; k  := k +  1 end; return s end
Určete invariant cyklu ve vyznačeném místě tak, aby s jeho pomocí bylo možno ze vstupní podmínky
cp(A)  = Vi.A.eZ A 3k>l.Ak = 0 odvodit výstupní podmínku
ý(A, s)  = 3k> 0. í Ak = 0 A (Vj.l<j<k=>Aj^0) A s = ^ A% j
D   Následující algoritmus seřadí číselnou posloupnost  a = (ai,..., an)   uloženou v poli A vzestupně. Tedy na konci výpočtu bude v poli A posloupnost  o! = (a^,..., afn), která je permutací posloupnosti a a platí a[ < • • • < o!n
for i <—   [2 . . n]   do begin
/y»       • —        l\  . •            /i        • ~      7    ___    T   •
^     •        -rL% y        J                     L             ± y
while   {j > 0)   &&   (Aj > x)   do begin
Aj+i   : = A j ;
Í   := j-1 end;
yi^_)_^   i = x
end
Formulujte vstupní a výstupní podmínky a nalezněte invarianty pro vnější a vnitřní cyklus.
D   Nenulový reálný polynom je zadán neprázdnou posloupností koeficientů
p = [ao,ai,a2,... ,an] . Napište funkci /z se dvěma parametry, p,x, která vypočte
funkční hodnotu polynomu p v bodě x.
D   Stanovte vstupní a výstupní podmínky a dokažte konvergenci a správnost funkce /z.