Semantyka i weryfikacja programów/Ćwiczenia 15

Zawartość

Ostatnie ćwiczenia poświęcone będa dowodzeniu poprawności całkowitej programów.

Poprawność całkowita

Ćwiczenie 1 (potęgowanie binarne)

Przeprowadź dowód poprawności całkowitej (poprawność częściowa plus własność stopu) potęgowania binarnego:

 $[y \geq 0]$ 
z := 1; p := x; q := y;
while q <> 0 do
  if odd(q) then
    z := z * p;
  q := q div 2;
  p := p * p
 $[z = x^{y}]$

Rozwiązanie

Intuicyjnie, pownniśmy wskazać wyrażenie, którego wartość maleje w każdym obrocie pętli i jest zawsze nieujemna. Naturalnym kandydatem jest wyrażenie $q$ . W dowodzie poprawności częściowej używaliśmy niezmiennika $N \equiv z \cdot p^{q} = x^{y}$ . Intuicyjnie mówiąc, dla własności stopu potrzebujemy dodatkowo własności $q \geq 0$ , więc naturalnym pomysłem byłoby dodanie tej własności do niezmiennika. Dla formalnego dowodu potrzebujemy jednak, "kontrolować" wartość zmiennej $q$ za pomocą zewnętrzenego parametru:

$N^{'} (l) \equiv z \cdot p^{q} = x^{y} \land q = l$ .

Formalnie rzecz biorąc, wykażemy:

 $[\exists l \geq 0 . N^{'} (l)]$ 
while q <> 0 do
  if odd(q) then
    z := z * p;
  q := q div 2;
  p := p * p
 $[N^{'} (0)]$

i dodatkowo dwie implikacje:

$y \geq 0 ⟹ \exists l \geq 0 . N^{'} (l)$
$N^{'} (0) ⟹ z = x^{y}$ .

Zastosujemy teraz następującą regułę dla pętli (jest to odmiana reguły zaprezentowanej na wykładzie, która jest wygodna w tym zadaniu :)

$\frac{l > 0 \land N^{'} (l) ⟹ b [l > 0 \land N^{'} (l)] I [N^{'} (l d i v 2)] N^{'} (0) ⟹ \neg b}{[\exists l . l \geq 0 \land N^{'} (l)] 𝐰 𝐡 𝐢 𝐥 𝐞 b 𝐝 𝐨 I [N^{'} (0)]}$

Wystarczy zatem dowieść:

   $[l > 0 \land N^{'} (l)]$ 
  if odd(q) then
    z := z * p;
  q := q div 2;
  p := p * p
   $[N^{'} (l d i v 2)]$

oraz kolejnych dwóch łatwych implikacji:

$l d i v 2 \geq 0 \land N^{'} (l) ⟹ q \neq 0$
$N^{'} (0) ⟹ q = 0$ .

Stosując teraz zwykłe reguły "przeciągamy" asercję $N^{'} (l d i v 2)$ w tył:

   $[l > 0 \land z \cdot p^{q} = x^{y} \land q = l]$ 
  if odd(q) then
  (
     $[l > 0 \land z \cdot p^{q} = x^{y} \land q = l \land o d d (q)]$ 
         $⇓$ 
     $[(z \cdot p) \cdot (p \cdot p)^{(q d i v 2)} = x^{y} \land q d i v 2 = l d i v 2]$ 
    z := z * p;
     $[z \cdot (p \cdot p)^{(q d i v 2)} = x^{y} \land q d i v 2 = l d i v 2]$ 
  )
   $[z \cdot (p \cdot p)^{(q d i v 2)} = x^{y} \land q d i v 2 = l d i v 2]$ 
  q := q div 2;
   $[z \cdot (p \cdot p)^{q} = x^{y} \land q = l d i v 2]$ 
  p := p * p
   $[z \cdot p^{q} = x^{y} \land q = l d i v 2]$

Oprócz implikacji zaznaczonej w anotacjach, powinniśmy też udowodnić:

$l > 0 \land z \cdot p^{q} = x^{y} \land q = l \land \neg o d d (q) ⟹ z \cdot (p \cdot p)^{(q d i v 2)} = x^{y} \land q d i v 2 = l d i v 2 .$

W przyszłości będziemy pomijać formalny dowód własności stopu i ograniczymy się do podania wyrażenia, które maleje w każdym obiegu pętli. Będziemy używali następującej notacji:

...

while   $[N]$   q <> 0 do  $[𝐝 𝐞 𝐜 𝐫 q 𝐢 𝐧 ℕ 𝐰 𝐫 𝐭 <]$ 
(
  if odd(q) then
    z := z * p;
  q := q div 2;
  p := p * p
)
 $[N \land q = 0]$ 

...

Ćwiczenie 2

Przeprowadź dowód poprawności całkowitej poniższego programu.

 ${n \geq 0}$ 

s := 1; i := 1;
while i < n do
  k := 1; l := 0; p := 1;
  while p < i do
    k := k + 1;
    if l < p then
      l := l + 1;
      p := 1
    else
      p := p + 1;
  s := s + 6 * k + p - l;
  i := i + 1;
 
 ${s = n^{3}}$

Wskazówka

$(m + 1)^{3} = m^{3} + 3 \cdot m^{2} + 3 \cdot m + 1$

$Σ_{j = 1}^{m} j = \frac{m \cdot (m + 1)}{2}$

Rozwiązanie (poprawność częściowa)

Zacznijmy od niezmiennika dla pętli zewnętrznej: $N_{1} \equiv s = i^{3} \land 1 \leq i \leq n$ .

 ${n \geq 1}$ 
   $⇓$         // 1 
 ${N_{1} [i \mapsto 1] [s \mapsto 1]}$ 
s := 1; 
i := 1;
while   ${N_{1}}$   i < n do
(
   ${N_{1} \land i < n}$ 
  k := 1; 
  l := 0; 
  p := 1;
   ${N_{1} \land i < n \land k = 1 \land l = 0 \land p = 1}$ 
  while p < i do
  (
    k := k + 1;
    if l < p then
    (
      l := l + 1;
      p := 1
    )
    else
    (
      p := p + 1;
    )
  )
  s := s + 6 * k + p - l;
  i := i + 1;
   ${N_{1}}$ 
) 
 ${N_{1} \land i \geq n}$ 
   $⇓$         // 2 
 ${s = n^{3}}$

Dwie zaznaczone implikacja są łatwe do udowodnienia. Trudniej jest znależć niezmiennik dla pętli wewnętrznej. Przede wszystkim zauważmy, że jeśli $N_{1}$ ma się "odnawiać" po każdym obrocie zewnętrznej pętli, to wartość dodawana do zmiennej $s$ powinna wynosić:

$(i + 1)^{3} - i^{3} = 3 \cdot i^{2} + 3 \cdot i + 1 = 3 \cdot (i^{2} + i) + 1 = 3 \cdot i \cdot (i + 1) + 1 .$

Zatem pętla wewnętrzna powinna prawdopodobnie obliczać na zmiennej $k$ wartość $\frac{i \cdot (i + 1)}{2} = 1 + 2 + \dots + i$ . Jeśli uważnie przyjrzymy się pętli wewnętrznej, to zaobserwujemy, że zmienna $k$ przechowuje wartość $1 + 2 + \dots + l$ plus "zaczęte" $l + 1$ , czyli plus $p$ . Spróbujmy niezmiennik postaci:

$N_{2} \equiv k = (1 + 2 + \dots + l) + p \land \dots$

Pozostaje jeszcze ustalić ograniczenia górne lub dolne zmiennych p, l. Po pierwsze, zawsze zachodzi $p \leq l + 1$ . Po drugie, oczekujemy, że spełniony będzie warunek $l < i$ . Zauważmy, że zmienna $l$ nigdy nie osiągnie wartości $i$ , gdyż wcześniej zmienna $p$ osiągnie tę wartość, a wtedy nastąpi od razu wyjście z pętli. Połączmy te ograniczenia w jeden zwięły warunek:

$N_{2} \equiv k = (1 + 2 + \dots + l) + p \land 1 \leq p \leq l + 1 \leq i .$

Oto odpowiednie anotacje całego programu:

 ${n \geq 1}$ 
   $⇓$         // 1 
 ${N_{1} [i \mapsto 1] [s \mapsto 1]}$ 
s := 1; 
i := 1;
while   ${N_{1}}$   i < n do
(
   ${N_{1} \land i < n}$ 
  k := 1; 
  l := 0; 
  p := 1;
   ${N_{1} \land i < n \land k = 1 \land l = 0 \land p = 1}$ 
     $⇓$         // 3  
   ${N_{2}}$ 
  while   ${N_{2}}$   p < i do
  (
    k := k + 1;
    if l < p then
    (
      l := l + 1;
      p := 1
    )
    else
    (
      p := p + 1;
    )
  )
   ${N_{2} \land p \geq i}$ 
     $⇓$         // 4 
   ${N_{1} [i \mapsto i + 1] [s \mapsto s + 6 \cdot k + p - l]}$ 
  s := s + 6 * k + p - l;
  i := i + 1;
   ${N_{1}}$ 
) 
 ${N_{1} \land i \geq n}$ 
   $⇓$         // 2 
 ${s = n^{3}}$

Musimy teraz udowodnić dwie kolejne zaznaczone powyżej implikacje:

$N_{1} \land i < n \land k = 1 \land l = 0 \land p = 1 ⟹ N_{2}$
$N_{2} \land p \geq i ⟹ N_{1} [i \mapsto i + 1] [s \mapsto s + 6 \cdot k + p - l]$ .

Pierwsza z nich jest oczywista, natomiast nie jesteśmy w stanie dowieść drugiej! Jest tak dlatego, że w $N_{2}$ nie mamy informacji o tym, że przed wejściem do pętli wewnętrznej zachodziło $s = i^{3}$ , a jest to niezbędne w dowodzie. Zmodyfikujmy $N_{2}$ następująco:

$N_{2} \equiv s = i^{3} \land k = (1 + 2 + \dots + l) + p \land 1 \leq p \leq l + 1 \leq i$

i wróćmy do ostatniej z implikacji powyżej. Wciąż brakuje nam pewnych informacji! Tym razem nie potrafimy pokazać, że zachodzi $i + 1 \leq n$ , co stanowi część formuły $N_{1} [i \mapsto i + 1] [s \mapsto s + 6 \cdot k + p - l]$ . Powinniśmy dodać do $N_{2}$ warunek $i < n$ , który zachodzi zawsze po wejściu do pętli zewnętrznej. Otrzymujemy ostatecznie:

$N_{2} \equiv s = i^{3} \land i < n \land k = (1 + 2 + \dots + l) + p \land 1 \leq p \leq l + 1 \leq i .$

Teraz dowód ostatniej implikacji jest możliwy. Zauważmy w szczególności, że warunek $p \geq i$ w połączeniu z warunkiem $p \leq l + 1 \leq i$ obecnym w $N_{2}$ daje nam $p = l + 1 = i$ . Ponieważ $p = l + 1$ mamy:

$s + 6 \cdot k + p - l = s + 6 \cdot (1 + 2 + \dots + (l + 1)) + 1$

a ponieważ $l + 1 = i$ , otrzymujemy:

$s + 6 \cdot k + p - l = s + 6 \cdot (1 + 2 + \dots + (l + 1)) + 1 = s + 6 \cdot (1 + 2 + \dots + i) + 1 = s + 6 \cdot \frac{i \cdot (i + 1)}{2} + 1 = s + 3 \cdot i^{2} + 3 \cdot i + 1 = (i + 1)^{3} .$

Na koniec pozostał nam dowód poprawności instrukcji wewnętrznej w wewnętrznej pętli:

    ...
    
     ${N_{2} \land p < i}$ 
    k := k + 1;
     ${?}$ 
    if l < p then
    (
      l := l + 1;
      p := 1
    )
    else
    (
      p := p + 1;
    )
     ${N_{2}}$ 
    
    ...

Musimy wpisać jakąś asercję w miejsce znaku zapytania. Nietrudno jest odgadnąć właściwą formułę: wystarczy dodać jeden do wyrażenia, które stoi po prawej stronie w równaniu $k = (1 + 2 + \dots l) + p$ w $N_{2} \land p < i$ , czyli zastąpić je przez $k = (1 + 2 + \dots l) + p + 1$ . Oznaczmmy przez $N^{'}$ asercję, którą otrzymujemy w ten sposób z $N_{2}$ :

$N^{'} \equiv s = i^{3} \land i < n \land k = (1 + 2 + \dots l) + p + 1 \land 1 \leq p \leq l + 1 \leq i .$

Oto szczegółowa anotacja rozważanego fragmentu programu:

    ...
    
     ${N_{2} \land p < i}$ 
       $⇓$         // 5 
     ${N^{'} [k \mapsto k + 1] \land p < i}$ 
    k := k + 1;
     ${N^{'} \land p < i}$ 
    if l < p then
    (
       ${N^{'} \land l < p}$ 
         $⇓$         // 6 
       ${N_{2} [p \mapsto 1] [l \mapsto l + 1]}$ 
      l := l + 1;
      p := 1
       ${N_{2}}$ 
    )
    else
    (
       ${N^{'} \land l \geq p}$ 
         $⇓$         // 7 
       ${N_{2} [p \mapsto p + 1]}$ 
      p := p + 1;
       ${N_{2}}$ 
    )
     ${N_{2}}$ 
    
    ...

oraz implikacje niezbędne dla dokończenia dowodu:

$N_{2} \land p < i ⟹ N^{'} [k \mapsto k + 1] \land p < i$
$N^{'} \land l < p < i ⟹ N_{2} [p \mapsto 1] [l \mapsto l + 1]$
$N^{'} \land l \geq p < i ⟹ N_{2} [p \mapsto p + 1]$ .

Rozwiązanie (poprawność calkowita)

Własność stopu pętli zewnętrznej łatwo jest pokazać, gdyż w każdym obiegu rośnie wartość zmiennej $i$ , czyli maleje wartość wyrażenia $n - i$ . Dodatkowo $n - i \geq 0$ zagwarantowane jest przez niezmiennik $N_{1}$ .

Trudniej jest pokazać własność stopu pętli wewnętrznej. Choć dozór tej pętli to $p < i$ , to zasadnicze znaczenie dla tej pętli ma nie tyle wzrost wartości zmiennej $p$ (zmienna i nie zmienia się w tej pętli) co wzrost wartości zmiennej $l$ . Ale wyrażenie $i - l$ nie maleje po każdym obiegu pętli! Może ono pozostać niezmienione, ale wtedy rośnie na pewno wartość zmiennej $p$ , czyli maleje $i - p$ . Widać zatem, że warto tutaj wziąć pod uwagę porządek leksykograficzny par liczb: para wartości wyrażeń $⟨ i - l, i - p ⟩$ maleje w porządku leksykograficznym po każdym obiegu pętli. Obydwa mają przy tym zawsze wartość większą lub równą 0, dzięki niezmiennikowi $N_{2}$ .

Odpowiednie anotacje całego programu to:

 $[n \geq 1]$ 
   $⇓$         // 1 
 $[N_{1} [i \mapsto 1] [s \mapsto 1]]$ 
s := 1; 
i := 1;
while   $[N_{1}]$   i < n do  $[𝐝 𝐞 𝐜 𝐫 n - i 𝐢 𝐧 ℕ 𝐰 𝐫 𝐭 <]$ 
(
   $[N_{1} \land i < n]$ 
  k := 1; 
  l := 0; 
  p := 1;
   $[N_{1} \land i < n \land k = 1 \land l = 0 \land p = 1]$ 
     $⇓$         // 3  
   $[N_{2}]$ 
  while   $[N_{2}]$   p < i do  $[𝐝 𝐞 𝐜 𝐫 ⟨ i - l, i - p ⟩ 𝐢 𝐧 ℕ^{2} 𝐰 𝐫 𝐭 <_{lex}]$ 
  (
    
    ...
    
    )
  )
   $[N_{2} \land p \geq i]$ 
     $⇓$         // 4 
   $[N_{1} [i \mapsto i + 1] [s \mapsto s + 6 \cdot k + p - l]]$ 
  s := s + 6 * k + p - l;
  i := i + 1;
   $[N_{1}]$ 
) 
 $[N_{1} \land i \geq n]$ 
   $⇓$         // 2 
 $[s = n^{3}]$

Zadania domowe

Ćwiczenie 1

Przeprowadź dowód poprawności całkowitej poniższego programu.

 $[(\forall x . 1 \leq x < n ⟹ A [x] \leq A [x + 1]) \land (\forall x . n + 1 \leq x < 2 \cdot n ⟹ A [x] \leq A [x + 1])]$ 
i := 1; j := 2 * n;
while A[i] < A[j] do
  ,,zamień A[i] i A[j]";
  i := i + 1;
  j := j - 1;
 $[\forall x, y . 1 \leq x \leq n < y \leq 2 \cdot n ⟹ A [x] \geq A [y]]$

Semantyka i weryfikacja programów/Ćwiczenia 15

Zawartość

Poprawność całkowita

Zadania domowe

Menu nawigacyjne

Działania na stronie

Opcje strony

Narzędzia osobiste

Nawigacja

Szukaj

Narzędzia