[Semantyka i weryfikacja] Niezmiennik pętli

[lunex]

Witam, mam problem z poniższym zadaniem:

Program liczy funkcję \(\displaystyle{ \frac{n(n+1)}{2}}\).
Prosze sformulowac niezmiennik petli,
warunki poczatkowe na wejscie n
oraz warunek, ktory gwarantuje,
ze petla sie zatrzyma.

Oto program:

Kod: Zaznacz cały

IPUT: n
x:=1;
y:=0;
while (x<=n) do
{
y:=y+x;
x:=x+1;
}
OUTPUT: y; 

Głównie mam trudności ze znalezieniem niezmiennika pętli. Jeżeli ktoś mógłby mi go wskazać to byłbym niezmiernie wdzięczny :>

[Zordon]

po kazdym obrocie pętli zachodzi:
\(\displaystyle{ y=0+1+2+...+(x-1)= \frac{x(x-1)}{2}}\)