program MaxVet;

{pre:}  
{post: trovare il massimo elemento in un vettore 
       di interi}

var i, max: int;
    a: array [1..10] of integer;

begin
   {assumiamo che al posto di questo commento ci siano 
    le istruzioni atte a caricare opportunamente l'array
    'a'}
   max:=a[1];                      {max >= a[k], per 1<= k < 1}
   for i:=2 to 10 do
     if (a[i]>max) then max:=a[i]; {INVARIANTE: max >= a[k], per 1 <= k < i}
   writeln('il massimo e`', max)   {i = n+1, per cui max >= a[k] 
				    per 1 <= k < n+1, ovvero per 1<= k <= n}
end.

NOTA: l'invariante di ciclo e` valida dopo l'incremento della variabile 'i'.  
      Ho scelto di scrivere come invariante principale un predicato che 
      descrive la situazione in quel momento della computazione perche' mi 
      sembra sia l'invariante piu' intuitiva da scrivere (notare che 
      l'invariante principale del programma Fibonacci visto a lezione il 
      12 Ottobre segue la stessa idea).



program Ordinamento;

VEDERE LEZIONE DEL 2 NOVEMBRE (procedura 'SelectionSort')