A Následující program power počíta pro přijatá čísla z a n mocninu zn. Napište specifikaci tohoto programu, a pak ověřte jeho totální korektnost vzhledem k zapsané specifikaci.
float power(float z, int n) { float r = 1;
f or (int i = 1; i<=n; i = i + 1)
r = r * z; return r;
}
A Program linearSearch, jehož kód je uveden níže, přijímá pole celých čísel a a snaží se zjistit, jestli v intervalu [l,u] pole a leží hodnota e nebo ne. Zapište specifikaci tohoto programu, a pak ověřte jeho totální korektnost vzhledem ke specifikaci.
bool linearSearch(int [] a, int 1, int u, int e) { for (int i = 1; i<=u; i = i + 1)
if (a[i] == e) return true; return falše;
}
A Mějme dám program binarySearch, který přijme pole celých čísel a a snaží se zjistit, jestli v intervalu [l,u] pole a leží hodnota e nebo ne. Zapište specifikaci tohoto programu, a pak ověřte jeho totální korektnost vzhledem ke specifikaci. Zde je kód programu.
bool binarySearch(int [] a, int 1, int u, int e) { if (1 > u) return falše; int m = (1 + u) div 2; if (a[m] == e) return true; if (a[m] < e)
return binarySearch(a,m+l,u,e); else
return binarySearch(a,1,m-l,e);
A Následující program bubbleSort přijímá pole celých čísel a a vrací jeho seřazenou kopii. Zapište specifikaci tohoto programu, a pak ověřte jeho totální korektnost vzhledem ke specifikaci.
int[] bubbleSort (int [] a0) { int[] a = a0;
for (int i = |a| - 1; i > 0; i = i - 1) for (int j = 0; j < i; j = j + 1) if (a[j] > a[j + l]) { int m = a[j] ; a[j] = a[j+l] ; a[j + l] = m;
}
return a;
}
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í?
Vzhledem ke kterým z uvedených vstupních podmínek a výstupní podmínce
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 ip(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: <fi(Á) = A je dvouprvkové pole celých čísel
y], [p, q]) = V < Q A (p, q) je 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
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 Dokazte konvergenci funkce power vzhledem ke vstupní podmínce
(f((z, nj) ezgI - {0} A n £ 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^\ = 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
<p(A) = Vz. A, e Z A 3k>l.Ak = 0 odvodit výstupní podmínku
k
A,s) = 3k>0.[Ak = 0 A (Vj. 1 < j < k    A3 ^ 0) A s = ^ A{
□ Následující algoritmus seřadí číselnou posloupnost CL —     1 ' ' ' i
) uloženou v poli
A vzestupně. Tedy na konci výpočtu bude v poli A posloupnost a! = (a^,..., ařn), která je permutací posloupnosti a a platí a[ < • • • < a'n
for i f- [2 . . n] do begin
rp       • —       A . • n       • —      i _ \ •
while O' > 0) && (A, > z) do begin
: = Aj 5 Í := Í - 1
end;
:= x
end
Formulujte vstupn í a výstupn í podm ínky a nalezněte invarianty pro vnějš í a vnitřn í cyklus.
□ Nenulový realny polynom je zadan neprazdnou posloupnost í koeficientu
p = Va0ia\ia2i-. - ,an] . Napiste funkci h se dvema parametry, p, x, ktera vypoCte
funkCn í hodnotu polynomu p v bode x.
□ Stanovte vstupn í a vystupn í podm ínky a dokaZte konvergenci a spravnost funkce h.