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!