Informatyka Teoretyczna , Poprawność Algorytmów

[liechmaster]

witam, mam problem :] , otóż mam pewien algorytm i chcę udowodnić jego poprawność używając logiki hoore'a. czy ktoś jest w miarę obeznany w tym temacie?

a alogrytm wygląda tak:

 

var T:array[1..N] of real;

suma,pom:real;

ws1,w1,ws2,w2:integer;

begin

pom:=0;suma:=0;w1:=1;

for w2:=1 to N do

begin

suma:=suma+T[w2];

if abs(180-pom)>abs(180-suma) then

begin

pom:=suma;ws1:=w1;ws2:=w2+1;

end;

while (suma>180) do

begin

suma:=suma - T[w1];w1:=w1+1;

if abs(180-pom)>abs(180-suma) then

begin

pom:=suma;ws1:=w1;ws2:=w2+1;

end;

end;

end;

end.