Dowód poprawności algorytmu - niezmienniki.

[lunex]

Witam, mam problem z poniższym zadaniem:
Udowodnij stosując metodę niezmienników, że dla dowolnej liczby naturalnej n>0,
następujący algorytm wylicza kwadrat liczby n.

Kod: Zaznacz cały

i=1;
s=1;
while (i<n) {
   s=s+2*i+1;
   i=i+1;
} 
return s;

W jaki sposób to udowodnić?

[etyre]

Kilka luźnych spostrzeżeń, które mogą Ci pomóc:

1. Jeśli się przyjrzeć, program jest implementacją algorytmu, który ma obliczać rekurencję:
\(\displaystyle{ \begin{cases} s_1 = 1 \\ s_{i+1} = s_i + 2i + 1 \end{cases}}\)
Czy aby na pewno? Pierwsze część jest jasna: masz na początku programu \(\displaystyle{ s = 1}\) (czyli \(\displaystyle{ s_1}\) w naszej rekurencji). W pętli zaś obliczasz kolejne wartości \(\displaystyle{ s_{i+1}}\) - zaczynasz od poprzedniej wartości (\(\displaystyle{ s_i}\)) dodajesz do tego \(\displaystyle{ 2i+1}\). Łatwo to sobie uzmysłowić, jeśli spojrzysz na jakiś prosty przykład. Weźmy kilka początkowych obiegów pętli:

Kod: Zaznacz cały

s1 = 1, i = 1; // przed wykonaniem pierwszego obiegu pętli
s2 = s1+2i+1 = 1+2+1=4; i++; // czyli s2 = 4, następnie powiększasz i o 1 i "nowe" i = 2. Jak widać, s2 = (i+1)^2
s3 = s2+2i+1 = 4+2*2+1=9; i++ // czyli s3 = 9, znowu mamy zależność si = (i+1)^2 

OK, co dalej?

2. Jak widać, pętla jest przerywana, jeśli \(\displaystyle{ i \ge n}\), następnie zwracasz ostatnią wartość \(\displaystyle{ s}\), jaką obliczyłeś, czyli będzie to w tym przypadku\(\displaystyle{ s_{n}}\). Generalnie, trzeba pokazać, że dla każdego \(\displaystyle{ i>0}\) zachodzi zależność \(\displaystyle{ s_{i+1} = (i+1)^2}\). Przez indukcję możesz pokazać, że jeśli zachodzi to dla \(\displaystyle{ s_i}\) to jest prawdziwe też dla \(\displaystyle{ s_{i+1}}\):
\(\displaystyle{ s_i \Rightarrow s_{i+1}}\)

Zakładamy więc, że \(\displaystyle{ s_i = i^2}\) i łatwo przekształcamy do wyjściowej postaci:
\(\displaystyle{ s_{i+1} = s_i + 2i + 1 = i^2 + 2i + 1 = (i+1)^2}\)
Co oznacza, że prawdziwa jest zależność \(\displaystyle{ s_i = i^2}\).

3. Skoro to ma być dowód z użyciem niezmiennika, musisz pokazać, że niezmiennik spełniony jest przed pierwszym obrotem pętli, w trakcie każdego obrotu i po zakończeniu działania pętli. Co będzie tu niezmiennikiem? Fakt, że w s (czyli wartość naszego \(\displaystyle{ s_i}\)) trzymamy kwadrat liczby, którą mamy zapisaną w i. Jest to spore uproszczenie, musisz to sformalizować. Zwróć uwagę, że obliczając \(\displaystyle{ s_{i+1}}\) bierzemy pod uwagę wartość \(\displaystyle{ i}\) z poprzedniego obiegu pętli.

4. Trochę się rozpisałem, mam nadzieję, że rozumiesz, o co chodzi. Zaznaczam, że są to luźne wskazówki i przemyślenia.