[Algorytmy] Dowód z użyciem niezmiennika pętli

[Assassin-Girl]

Witam, mam takie oto zadanie.

Korzystając z niezmiennika pętli, udowodnij, że poniższy algorytm jest poprawny.

Kod: Zaznacz cały

Mnożenie(y,z)
x ← 0
while z > 0 do
   if z % 2 = 1 then 
      x ← x + y
   y← 2*y
   z← ⌊z/2⌋.
return x

Nie do końca "łapię", jak się za to wziąć. Mamy \(\displaystyle{ x=0}\), gdy \(\displaystyle{ z}\) jest większe od zera, to sprawdzamy, czy \(\displaystyle{ z}\) jest liczbą nieparzystą. Jeśli \(\displaystyle{ z}\) spełnia ten warunek, to mam rozumieć, że można powiedzieć, że mamy do czynienia z niezmiennikiem pętli (w sumie to z dwoma, z while i if)?

Za wszelkie wskazówki będę wdzięczna.

[Dasio11]

Niezmiennik pętli to formuła zdaniowa zmiennych programu, która zawsze jeśli jest prawdziwa na początku pętli, to po jej jednorazowym przebiegu również. Używa się go, aby przeprowadzać dowody dotyczące wyniku działania programu.

Oznaczmy przez \(\displaystyle{ y_0, z_0}\) początkowe wartości zmiennych \(\displaystyle{ y, z.}\) W tym przypadku niezmiennikiem pętli jest \(\displaystyle{ x + y \cdot z = y_0 \cdot z_0.}\)

Dowód.
Załóżmy, że na początku pętli mamy \(\displaystyle{ x + y \cdot z = y_0 \cdot z_0}\) i oznaczmy przez \(\displaystyle{ x', y', z'}\) wartości zmiennych \(\displaystyle{ x, y, z}\) po jednym przebiegu pętli.

\(\displaystyle{ \bullet}\) Jeśli \(\displaystyle{ z}\) jest nieparzyste, to z kodu widać, że \(\displaystyle{ x' = x+y, y' = 2 \cdot y, z' = \frac{z-1}{2}.}\) Wtedy

\(\displaystyle{ x' + y' \cdot z' = (x+y) + (2 \cdot y) \cdot \frac{z-1}{2} = x+y+y \cdot (z-1) = x + y \cdot z = y_0 \cdot z_0.}\)

\(\displaystyle{ \bullet}\) Jeśli \(\displaystyle{ z}\) jest parzyste, to z kodu także widać, że \(\displaystyle{ x' = x, y' = 2 \cdot y, z' = \frac{z}{2}.}\) Wtedy

\(\displaystyle{ x' + y' \cdot z' = x + (2 \cdot y) \cdot \frac{z}{2} = x + y \cdot z = y_0 \cdot z_0.}\) \(\displaystyle{ \square}\)


Teraz możemy udowodnić, że program faktycznie wykonuje mnożenie. Na początku pętli mamy \(\displaystyle{ x + y \cdot z = 0 + y_0 \cdot z_0 = y_0 \cdot z_0.}\) Ponieważ to zdanie jest niezmiennikiem pętli, więc po zakończeniu ostatniego przebiegu tej pętli to nadal będzie prawda, tj. jeśli przez \(\displaystyle{ x', y', z'}\) oznaczymy wartości zmiennych \(\displaystyle{ x, y, z}\) po zakończeniu ostatniego przebiegu pętli, to wtedy \(\displaystyle{ x' + y' \cdot z' = y_0 \cdot z_0.}\) Ale skoro pętla się zakończyła, to \(\displaystyle{ z' = 0,}\) czyli \(\displaystyle{ x' = y_0 \cdot z_0.}\) To oznacza, że w zmiennej \(\displaystyle{ x}\) pod koniec znajduje się wynik mnożenia \(\displaystyle{ y_0 \cdot z_0,}\) tak jak miało być.


P.S. Precyzyjniej, wniosek na końcu, że \(\displaystyle{ z' = 0,}\) jest nie do końca uzasadniony. Aby go uzasadnić, niezmiennik należało sformułować tak (oraz uwzględnić to w jego dowodzie):

\(\displaystyle{ x + y \cdot z = y_0 \cdot z_0}\) oraz \(\displaystyle{ z \ge 0}\)

i wtedy \(\displaystyle{ z = 0}\) na końcu wynika z tego, że \(\displaystyle{ z \ge 0}\) ale \(\displaystyle{ \neg z > 0}\) skoro pętla się zakończyła. Ale mam nadzieję, że nie musimy być aż tak precyzyjni.

[Assassin-Girl]

Od razu jaśniej w głowie się zrobiło.

Dziękuję.