HELP - Dokazovanje pravilnosti algoritmov

Dan je algoritem

 
 Function alg(A,B: integer): integer; (* fi(A,B)= (A>==0) and (B>=0)*)
 var i: integer;
 begin
 i:=0;
 while A >= B do begin
 A:=A -B; 
 i:=i+1;
 end;
 alg:=i;
 end; (* psi(A,B,alg)= A div B*)
 
 

Naloga: Dokaži parcijalno pravilnost algoritma!

:( Se je kdo s tem že za*ebaval? Zanima me predvsem, kakšno zančno invarijanto moram postavit?

to je še en star dolg... OAPS2