Heja!
To nasz algorytm:
x=0; y=m;
do { x=x+n; y=y-1; } while(y!=0);
Niezmiennik jest to pewien warunek, który w ustalonym miejscu algorytmu jest zawsze prawdziwy. Tutaj można podać warunek, który jest prawdziwy na początku i na końcu każdego obrotu pętli while:
x = n * (m - y)
Sprawdźmy:
- Przed pierwszym obrotem pętli mamy x = 0, y = m, jeśli wstawimy to do naszego niezmiennika, to dostaniemy 0 = 0, czyli ok, niezmiennik jest prawdziwy
- Jeśli przed którymś z kolejnych obrotów pętli niezmiennik był prawdziwy, to widać że po zwiększeniu x o n i zmniejszeniu y o 1 (kod pętli) dalej będzie prawdziwy, bo zwiększamy lewą stronę niezmiennika o n, i prawą też zwiększamy o n (po prawej mamy n * "coś", i "coś" zwiększyło się o 1, bo y zmniejszyło się o 1)
I co nam to daje? Daje nam to tyle, że skoro w pewnym momecie y staje się w końcu 0 (po ostatnim obrocie pętli), a niezmiennik nadal jest zachowany (tak jak po każdym obrocie), to x = n * (m - y) = n * m. Czyli wnioskujemy, że "to" rzeczywiście mnoży.
Contrast: nie podaję maila, którego wpisałem Ci do komórki, bo nie chcę żeby "poszedł w świat" :) Ale to ja jestem :)