Semantyka i weryfikacja programów/Ćwiczenia 15

From Studia Informatyczne

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:


{\color{Red}[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
{\color{Red}[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:


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


i dodatkowo dwie implikacje:

  • y \geq 0 \, \implies \, \exists l \geq 0. N'(l)
  • N'(0) \, \implies \, 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) \implies b \quad {\color{Red}[l > 0 \land N'(l)]} I {\color{Red}[N'(l \,\mathrm{div}\, 2)]} \quad N'(0) \implies \neg b}      {{\color{Red}[\exists l. l \geq 0 \land N'(l)]} \mathbf{while}\, b \,\mathbf{do}\, I {\color{Red}[N'(0)]}}

Wystarczy zatem dowieść:


  {\color{Red}[l > 0 \land N'(l)]}
  if odd(q) then
    z := z * p;
  q := q div 2;
  p := p * p
  {\color{Red}[N'(l \,\mathrm{div}\, 2)]}


oraz kolejnych dwóch łatwych implikacji:

  • l \,\mathrm{div}\, 2 \geq 0 \land N'(l) \, \implies \, q \neq 0
  • N'(0) \implies q = 0.

Stosując teraz zwykłe reguły "przeciągamy" asercję N'(l \,\mathrm{div}\, 2) w tył:


  {\color{Red}[l > 0 \land z {\cdot} p^q = x^y \land q = l]}
  if odd(q) then
  (
    {\color{Red}[l > 0 \land z {\cdot} p^q = x^y \land q = l \land \,\mathrm{odd}(q)]}
        {\color{Green}\Downarrow}
    {\color{Red}[(z {\cdot} p) {\cdot} (p {\cdot} p)^{(q \,\mathrm{div}\, 2)} = x^y \land q \,\mathrm{div}\, 2 = l \,\mathrm{div}\, 2]}
    z := z * p;
    {\color{Red}[z {\cdot} (p {\cdot} p)^{(q \,\mathrm{div}\, 2)} = x^y \land q \,\mathrm{div}\, 2 = l \,\mathrm{div}\, 2]}
  )
  {\color{Red}[z {\cdot} (p {\cdot} p)^{(q \,\mathrm{div}\, 2)} = x^y \land q \,\mathrm{div}\, 2 = l \,\mathrm{div}\, 2]}
  q := q div 2;
  {\color{Red}[z {\cdot} (p {\cdot} p)^q = x^y \land q = l \,\mathrm{div}\, 2]}
  p := p * p
  {\color{Red}[z {\cdot} p^q = x^y \land q = l \,\mathrm{div}\, 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 \,\mathrm{odd}(q) \, \implies \, z {\cdot} (p {\cdot} p)^{(q \,\mathrm{div}\, 2)} = x^y \land q \,\mathrm{div}\, 2 = l \,\mathrm{div}\, 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  {\color{Red}[N]}  q <> 0 do {\color{Red}[\mathbf{decr}\, q \,\mathbf{in}\, \,\mathbb{N}\, \,\mathbf{wrt}\, <]}
(
  if odd(q) then
    z := z * p;
  q := q div 2;
  p := p * p
)
{\color{Red}[N \land q = 0]}

...



Ćwiczenie 2

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


{\color{Red}\{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;
 
{\color{Red}\{s = n^3\}}


Wskazówka

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

\Sigma_{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.


{\color{Red}\{n \geq 1\}}
  {\color{Green}\Downarrow}        // 1 
{\color{Red}\{N_1[i \mapsto 1][s \mapsto 1]\}}
s := 1; 
i := 1;
while  {\color{Red}\{N_1\}}  i < n do
(
  {\color{Red}\{N_1 \land i < n\}}
  k := 1; 
  l := 0; 
  p := 1;
  {\color{Red}\{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;
  {\color{Red}\{N_1\}}
) 
{\color{Red}\{N_1 \land i \geq n\}}
  {\color{Green}\Downarrow}        // 2 
{\color{Red}\{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 + \ldots + i.

Jeśli uważnie przyjrzymy się pętli wewnętrznej, to zaobserwujemy, że zmienna k przechowuje wartość 1 + 2 + \ldots + l plus "zaczęte" l{+}1, czyli plus p. Spróbujmy niezmiennik postaci:

N_2 \, \equiv \, k = (1 + 2 + \ldots + l) + p \land \ldots

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 + \ldots + l) + p \land 1 \leq p \leq l+1 \leq i.

Oto odpowiednie anotacje całego programu:


{\color{Red}\{n \geq 1\}}
  {\color{Green}\Downarrow}        // 1 
{\color{Red}\{N_1[i \mapsto 1][s \mapsto 1]\}}
s := 1; 
i := 1;
while  {\color{Red}\{N_1\}}  i < n do
(
  {\color{Red}\{N_1 \land i < n\}}
  k := 1; 
  l := 0; 
  p := 1;
  {\color{Red}\{N_1 \land i < n \land k = 1 \land l = 0 \land p = 1\}}
    {\color{Green}\Downarrow}        // 3  
  {\color{Red}\{N_2\}}
  while  {\color{Red}\{N_2\}}  p < i do
  (
    k := k + 1;
    if l < p then
    (
      l := l + 1;
      p := 1
    )
    else
    (
      p := p + 1;
    )
  )
  {\color{Red}\{N_2 \land p \geq i\}}
    {\color{Green}\Downarrow}        // 4 
  {\color{Red}\{N_1[i \mapsto i{+}1][s \mapsto s {+} 6 {\cdot} k {+} p {-} l]\}}
  s := s + 6 * k + p - l;
  i := i + 1;
  {\color{Red}\{N_1\}}
) 
{\color{Red}\{N_1 \land i \geq n\}}
  {\color{Green}\Downarrow}        // 2 
{\color{Red}\{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 \, \implies \, N_2
  • N_2 \land p \geq i \, \implies \, 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 + \ldots + 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 + \ldots + 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 + \ldots + (l{+}1)) + 1

a ponieważ l{+}1 = i, otrzymujemy:

s + 6 {\cdot} k + p {-} l \, = \, s + 6 {\cdot} (1 + 2 + \ldots + (l{+}1)) + 1 \, = \, s + 6 {\cdot} (1 + 2 + \ldots + 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:


    ...
    
    {\color{Red}\{N_2 \land p < i\}}
    k := k + 1;
    {\color{Red}\{?\}}
    if l < p then
    (
      l := l + 1;
      p := 1
    )
    else
    (
      p := p + 1;
    )
    {\color{Red}\{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 + \ldots l) + p w N_2 \land p < i, czyli zastąpić je przez k = (1 + 2 + \ldots 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 + \ldots l) + p + 1 \land 1 \leq p \leq l+1 \leq i.

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


    ...
    
    {\color{Red}\{N_2 \land p < i\}}
      {\color{Green}\Downarrow}        // 5 
    {\color{Red}\{N'[k \mapsto k{+}1] \land p < i\}}
    k := k + 1;
    {\color{Red}\{N' \land p < i\}}
    if l < p then
    (
      {\color{Red}\{N' \land l < p\}}
        {\color{Green}\Downarrow}        // 6 
      {\color{Red}\{N_2[p \mapsto 1][l \mapsto l{+}1]\}}
      l := l + 1;
      p := 1
      {\color{Red}\{N_2\}}
    )
    else
    (
      {\color{Red}\{N' \land l \geq p\}}
        {\color{Green}\Downarrow}        // 7 
      {\color{Red}\{N_2[p \mapsto p{+}1]\}}
      p := p + 1;
      {\color{Red}\{N_2\}}
    )
    {\color{Red}\{N_2\}}
    
    ...


oraz implikacje niezbędne dla dokończenia dowodu:

  • N_2 \land p < i \, \implies \, N'[k \mapsto k{+}1] \land p < i
  • N' \land l < p < i \, \implies \, N_2[p \mapsto 1][l \mapsto l{+}1]
  • N' \land l \geq p < i \, \implies \, 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ń \langle i - l, i - p \rangle 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:


{\color{Red}[n \geq 1]}
  {\color{Green}\Downarrow}        // 1 
{\color{Red}[N_1[i \mapsto 1][s \mapsto 1]]}
s := 1; 
i := 1;
while  {\color{Red}[N_1]}  i < n do {\color{Red}[\mathbf{decr}\, n{-}i \,\mathbf{in}\, \,\mathbb{N}\, \,\mathbf{wrt}\, <]}
(
  {\color{Red}[N_1 \land i < n]}
  k := 1; 
  l := 0; 
  p := 1;
  {\color{Red}[N_1 \land i < n \land k = 1 \land l = 0 \land p = 1]}
    {\color{Green}\Downarrow}        // 3  
  {\color{Red}[N_2]}
  while  {\color{Red}[N_2]}  p < i do {\color{Red}[\mathbf{decr}\, \langle i {-} l, i {-} p \rangle \,\mathbf{in}\, {\,\mathbb{N}\,}^2 \,\mathbf{wrt}\, <_{\mbox{lex}}]}
  (
    
    ...
    
    )
  )
  {\color{Red}[N_2 \land p \geq i]}
    {\color{Green}\Downarrow}        // 4 
  {\color{Red}[N_1[i \mapsto i{+}1][s \mapsto s {+} 6 {\cdot} k {+} p {-} l]]}
  s := s + 6 * k + p - l;
  i := i + 1;
  {\color{Red}[N_1]}
) 
{\color{Red}[N_1 \land i \geq n]}
  {\color{Green}\Downarrow}        // 2 
{\color{Red}[s = n^3]}



Zadania domowe

Ćwiczenie 1

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


{\color{Red}[(\forall x. 1 \leq x < n \implies A[x] \leq A[x+1]) \land (\forall x. n{+}1 \leq x < 2 {\cdot} n \implies 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;
{\color{Red}[\forall x, y. 1 \leq x \leq n < y \leq 2 {\cdot} n \implies A[x] \geq A[y]]}