Algorytm do wyznaczania silni

[spider865]

witam,
szukam dowodu na poprawnosc algorytmu wyznaczania silni

oto algorytm:

Kod: Zaznacz cały

Silnia(n)
begin
silnia := 1;
m := n;
while m > 0 do
begin
silnia := silnia*m;
m := m-1;
end;
end:

[Ichiban]

A co tu udowadniać? Pętla przechodzi n razy za każdym razem mnożąc wynik (zmienna silnia) przez aktualne m, które jest zmniejszane o 1 za każdym przejściem. Czyli liczy np:
6! = 6 * 5 * 4 * 3 * 2 * 1

A jak n = 0 to nawet nie wchodzi w pętlę i zwraca 1.