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\ge 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\ge 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^{\prime }(l)\equiv z\cdot p^q=x^y\wedge q=l$.

Formalnie rzecz biorąc, wykażemy:

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

i dodatkowo dwie implikacje:

• $y\ge 0⟹\mathrm{\exists }l\ge 0.N^{\prime }(l)$
• $N^{\prime }(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\wedge N^{\prime }(l)⟹b[l>0\wedge N^{\prime }(l)]I[N^{\prime }(l\mathrm{d}\mathrm{i}\mathrm{v}2)]N^{\prime }(0)⟹\mathrm{\neg }b}{[\mathrm{\exists }l.l\ge 0\wedge N^{\prime }(l)]\mathbf{𝐰}\mathbf{𝐡}\mathbf{𝐢}\mathbf{𝐥}\mathbf{𝐞}b\mathbf{𝐝}\mathbf{𝐨}I[N^{\prime }(0)]}$

Wystarczy zatem dowieść:

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

oraz kolejnych dwóch łatwych implikacji:

• $l\mathrm{d}\mathrm{i}\mathrm{v}2\ge 0\wedge N^{\prime }(l)⟹q\ne 0$
• $N^{\prime }(0)⟹q=0$.

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

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

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

$l>0\wedge z\cdot p^q=x^y\wedge q=l\wedge \mathrm{\neg }\mathrm{o}\mathrm{d}\mathrm{d}(q)⟹z\cdot (p\cdot p{)}^{(q\mathrm{d}\mathrm{i}\mathrm{v}2)}=x^y\wedge q\mathrm{d}\mathrm{i}\mathrm{v}2=l\mathrm{d}\mathrm{i}\mathrm{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 $[\mathbf{𝐝}\mathbf{𝐞}\mathbf{𝐜}\mathbf{𝐫}q\mathbf{𝐢}\mathbf{𝐧}\mathbb{\mathbb{N}}\mathbf{𝐰}\mathbf{𝐫}\mathbf{𝐭}<]$
(
  if odd(q) then
    z := z * p;
  q := q div 2;
  p := p * p
)
$[N\wedge q=0]$

...

Ćwiczenie 2

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

$\{n\ge 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$

${\mathrm{\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\wedge 1\le i\le n$.

$\{n\ge 1\}$
  $\Downarrow$        // 1 
$\{N_1[i\mapsto 1][s\mapsto 1]\}$
s := 1; 
i := 1;
while  $\{N_1\}$  i < n do
(
  $\{N_1\wedge i<n\}$
  k := 1; 
  l := 0; 
  p := 1;
  $\{N_1\wedge i<n\wedge k=1\wedge l=0\wedge 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\wedge i\ge n\}$
  $\Downarrow$        // 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\wedge \dots$

Pozostaje jeszcze ustalić ograniczenia górne lub dolne zmiennych p, l. Po pierwsze, zawsze zachodzi $p\le 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\wedge 1\le p\le l+1\le i.$

Oto odpowiednie anotacje całego programu:

$\{n\ge 1\}$
  $\Downarrow$        // 1 
$\{N_1[i\mapsto 1][s\mapsto 1]\}$
s := 1; 
i := 1;
while  $\{N_1\}$  i < n do
(
  $\{N_1\wedge i<n\}$
  k := 1; 
  l := 0; 
  p := 1;
  $\{N_1\wedge i<n\wedge k=1\wedge l=0\wedge p=1\}$
    $\Downarrow$        // 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\wedge p\ge i\}$
    $\Downarrow$        // 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\wedge i\ge n\}$
  $\Downarrow$        // 2 
$\{s=n^3\}$

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

• $N_1\wedge i<n\wedge k=1\wedge l=0\wedge p=1⟹N_2$
• $N_2\wedge p\ge 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\wedge k=(1+2+\dots +l)+p\wedge 1\le p\le l+1\le i$

i wróćmy do ostatniej z implikacji powyżej. Wciąż brakuje nam pewnych informacji! Tym razem nie potrafimy pokazać, że zachodzi $i+1\le 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\wedge i<n\wedge k=(1+2+\dots +l)+p\wedge 1\le p\le l+1\le i.$

Teraz dowód ostatniej implikacji jest możliwy. Zauważmy w szczególności, że warunek $p\ge i$ w połączeniu z warunkiem $p\le l+1\le 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\wedge 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\wedge p<i$, czyli zastąpić je przez $k=(1+2+\dots l)+p+1$. Oznaczmmy przez $N^{\prime }$ asercję, którą otrzymujemy w ten sposób z $N_2$:

$N^{\prime }\equiv s=i^3\wedge i<n\wedge k=(1+2+\dots l)+p+1\wedge 1\le p\le l+1\le i.$

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

    ...
    
    $\{N_2\wedge p<i\}$
      $\Downarrow$        // 5 
    $\{N^{\prime }[k\mapsto k+1]\wedge p<i\}$
    k := k + 1;
    $\{N^{\prime }\wedge p<i\}$
    if l < p then
    (
      $\{N^{\prime }\wedge l<p\}$
        $\Downarrow$        // 6 
      $\{N_2[p\mapsto 1][l\mapsto l+1]\}$
      l := l + 1;
      p := 1
      $\{N_2\}$
    )
    else
    (
      $\{N^{\prime }\wedge l\ge p\}$
        $\Downarrow$        // 7 
      $\{N_2[p\mapsto p+1]\}$
      p := p + 1;
      $\{N_2\}$
    )
    $\{N_2\}$
    
    ...

oraz implikacje niezbędne dla dokończenia dowodu:

• $N_2\wedge p<i⟹N^{\prime }[k\mapsto k+1]\wedge p<i$
• $N^{\prime }\wedge l<p<i⟹N_2[p\mapsto 1][l\mapsto l+1]$
• $N^{\prime }\wedge l\ge 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\ge 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\ge 1]$
  $\Downarrow$        // 1 
$[N_1[i\mapsto 1][s\mapsto 1]]$
s := 1; 
i := 1;
while  $[N_1]$  i < n do $[\mathbf{𝐝}\mathbf{𝐞}\mathbf{𝐜}\mathbf{𝐫}n-i\mathbf{𝐢}\mathbf{𝐧}\mathbb{\mathbb{N}}\mathbf{𝐰}\mathbf{𝐫}\mathbf{𝐭}<]$
(
  $[N_1\wedge i<n]$
  k := 1; 
  l := 0; 
  p := 1;
  $[N_1\wedge i<n\wedge k=1\wedge l=0\wedge p=1]$
    $\Downarrow$        // 3  
  $[N_2]$
  while  $[N_2]$  p < i do $[\mathbf{𝐝}\mathbf{𝐞}\mathbf{𝐜}\mathbf{𝐫}⟨i-l,i-p⟩\mathbf{𝐢}\mathbf{𝐧}{\mathbb{\mathbb{N}}}^2\mathbf{𝐰}\mathbf{𝐫}\mathbf{𝐭}{<}_{\text{lex}}]$
  (
    
    ...
    
    )
  )
  $[N_2\wedge p\ge i]$
    $\Downarrow$        // 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\wedge i\ge n]$
  $\Downarrow$        // 2 
$[s=n^3]$

Zadania domowe

Ćwiczenie 1

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

$[(\mathrm{\forall }x.1\le x<n⟹A[x]\le A[x+1])\wedge (\mathrm{\forall }x.n+1\le x<2\cdot n⟹A[x]\le 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;
$[\mathrm{\forall }x,y.1\le x\le n<y\le 2\cdot n⟹A[x]\ge A[y]]$