Semantyka i weryfikacja programów/Ćwiczenia 13

Zawartość

Poprawność częściowa prostych programów w języku TINY.

Poprawność częściowa

Ćwiczenie 1

Przeprowadź dowód poprawności częściowej poniższego programu:

$\{n\ge 1\}$
x := 1; y := 0;
while x <= n do
  y := y + x;
  x := x + 1
$\{y=\frac{n\cdot (n+1)}{2}\}$

Rozwiązanie

Najpierw musimy odgadnąć asercję, którą można wpisać pomiędzy początkowe przypisania a pętlę:

$\{n\ge 1\}$
x := 1; 
y := 0;
$\{?\}$
while x <= n do
(
  y := y + x;
  x := x + 1
)
$\{y=\frac{n\cdot (n+1)}{2}\}$

Możemy na przykład "przeciągnąć" asercję początkową wprzód, otrzymując $\{n\ge 0\wedge x=1\wedge y=0\}$. Teraz wystarczy dowieść następujące dwie trójki Hoare'a:

$\{n\ge 1\}$
x := 1; 
y := 0;
$\{n\ge 0\wedge x=1\wedge y=0\}$

$\{n\ge 0\wedge x=1\wedge y=0\}$
while x <= n do
(
  y := y + x;
  x := x + 1
)
$\{y=\frac{n\cdot (n+1)}{2}\}$

Zajmijmy się tą ostatnią. Naszym zadaniem jest teraz odkrycie niezmiennika $N$ takiego, że zachodzą poniższe dwie implikacje:

• $n\ge 0\wedge x=1\wedge y=0⟹N$
• $N\wedge x>n⟹y=\frac{n\cdot (n+1)}{2}$

oraz prawdziwa jest trójka:

$\{N\}$
while x <= n do
(
  y := y + x;
  x := x + 1
)
$\{N\wedge x>n\}$

Aby dowieść tej ostatniej, musimy pokazać:

$\{N\wedge x\le n\}$
y := y + x;
x := x + 1
$\{N\}$

Formalnie rzecz biorąc, powinniśmy teraz zgadnąć asercję, która może być wpisana pomiędzy dwie instrukcje przypisania:

$\{N\wedge x\le n\}$
y := y + x;
$\{?\}$
x := x + 1
$\{N\}$

a następnie niezależnie dowieść poprawność każdej z dwóch nstrukcji. Ale w "odgadnięciu" pomoże nam reguła dla przypisania, która, intuicyjnie mówiąc, daje sposób na "przeciągnięcie" asercji w tył. Jeśli zastosujemy ją do drugiego przypisania "x := x + 1", otrzymamy:

$\{N\wedge x\le n\}$
y := y + x;
$\{N[x\mapsto x+1]\}$
x := x + 1
$\{N\}$

Teraz musimy tylko pokazać trójkę:

$\{N\wedge x\le n\}$
y := y + x;
$\{N[x\mapsto x+1]\}$

Użyjmy więc ponownie reguły dla przypisania, otrzymując:

$\{N\wedge x\le n\}$
    $\Downarrow$          // tę implikację należy udowodnić 
$\{N[x\mapsto x+1][y\mapsto y+x]\}$
y := y + x;
$\{N[x\mapsto x+1]\}$

Skoro dwie asercje spotkały się, wystarczy teraz udowodnić implikację.

I tak dalej. To znaczy, podobnie postępujemy z pozostałymi przypisaniami. A wszędzie, gdzie spotykają się dwie asercje, dowodzimy implikacji. Podsumowując, poniższe anotacje całego programu powinny stanowić dowód poprawności częściowej:

$\{n\ge 1\}$
x := 1; 
$\{n\ge 0\wedge x=1\}$
y := 0;
$\{n\ge 0\wedge x=1\wedge y=0\}$
    $\Downarrow$        // 1 
$\{N\}$
while x <= n do
(
  $\{N\wedge x\le n\}$
      $\Downarrow$        // 2 
  $\{N[x\mapsto x+1][y\mapsto y+x]\}$
  y := y + x;
  $\{N[x\mapsto x+1]\}$
  x := x + 1
  $\{N\}$
)
$\{N\wedge x>n\}$
    $\Downarrow$        // 3 
$\{y=\frac{n\cdot (n+1)}{2}\}$

A jedyne co pozostaje do zrobienia to tylko udowodnienie następujących implikacji:

1. $n\ge 0\wedge x=1\wedge y=0⟹N$
2. $N\wedge x\le n⟹N[x\mapsto x+1][y\mapsto y+x]$
3. $N\wedge x>n⟹y=\frac{n\cdot (n+1)}{2}$

Co ciekawe, to wszystko uczyniliśmy nie wiedząc wogóle, jaki jest niezmiennik pętli! Ale nadszedł wreszcie moment, w którym powinniśmy taki niezmiennik podać. Musimy go odgadnąć poprzez staranną obserwację tego, co dzieje się wewnątrz pętli. Należy oczywiście uwzględnić również implikacje, które wypisaliśmy powyżej.

Spróbujmy $N\equiv y=\frac{x\cdot (x-1)}{2}\wedge x\le n+1$.

Nierówność $x\le n+1$ jest niezbędna. Potrzebujemy jej po to, aby z $N\wedge x>n$ wywnioskować $x=n+1$. Implikacje są prawdziwe, więc niezmiennik został wybrany poprawnie.

Zauważmy, że niezmiennik nie zawiera wymagania $x\ge 1$. Moglibyśmy je jednak dodać, otrzymując $N^{\prime }\equiv y=\frac{x\cdot (x-1)}{2}\wedge 1\le x\le n+1$. Wszystkie implikacje pozostają prawdziwe, więc jest to też poprawny wybór. Ponadto wiedząc, że $x\ge 1$ możemy, dla czytelności, zapisywać niezmiennik w meta-notacji:

$N\equiv y=1+2+\dots +(x-1)\wedge x\le n+1$

Pytanie: dlaczego nie potrzebowaliśmy warunku $x\ge 0$? Jak będzie działał nasz program, jeśli zmienną x zainicjujemy wartością ujemną (zamiast x := 1), np. x := -2, y := 3?

Notacja:

Niezmiennik pętli będziemy zwykle wpisywać pomiędzy słowem kluczowym while a dozorem pętli. W naszym przypadku otrzymamy następujące anotacje:

$\{n\ge 1\}$
x := 1; 
$\{n\ge 0\wedge x=1\}$
y := 0;
$\{n\ge 0\wedge x=1\wedge y=0\}$
    $\Downarrow$        // 1 
$\{N\}$
while  $\{N\}$  x <= n do
(
  $\{N\wedge x\le n\}$

  ...

Wariant:

Wróćmy na chwilę do naszej pierwszej decyzji, polegającej na wpisaniu następującej asercji

$\{n\ge 0\wedge x=1\wedge y=0\}$

pomiędzy początkowe przypisania a pętlę. Mogliśmy uczynić inaczej i wpisać w to miejsce po prostu niezmiennik $N$. Wtedy należałoby wykazać:

$\{n\ge 1\}$
x := 1; 
y := 0;
$\{N\}$

co można, za pomocą znanego nam już "przepychania w tył", zredukować do udowodnienia implikacji:

$\{n\ge 1\}$
    $\Downarrow$        // 1 
$\{N[y\mapsto 0][x\mapsto 1]\}$
x := 1; 
$\{N[y\mapsto 0]\}$
y := 0;
$\{N\}$

Ostatecznie, anotacje programu wyglądałyby tak:

$\{n\ge 1\}$
    $\Downarrow$        // 1 
$\{N[y\mapsto 0][x\mapsto 1]\}$
x := 1; 
$\{N[y\mapsto 0]\}$
y := 0;
while  $\{N\}$  x <= n do
(
  $\{N\wedge x\le n\}$
      $\Downarrow$        // 2 
  $\{N[x\mapsto x+1][y\mapsto y+x]\}$
  y := y + x;
  $\{N[x\mapsto x+1]\}$
  x := x + 1
  $\{N\}$
)
$\{N\wedge x>n\}$
    $\Downarrow$        // 3 
$\{y=\frac{n\cdot (n+1)}{2}\}$

a pierwsza z trzech implikacji to: $n\ge 1⟹N[y\mapsto 0][x\mapsto 1]$.

Ćwiczenie 2

Uzupełnij poniższe reguły:

$\frac{?}{\{\alpha \}x:=e\{\beta \}}$

$\frac{?}{\{\alpha \}\mathbf{𝐰}\mathbf{𝐡}\mathbf{𝐢}\mathbf{𝐥}\mathbf{𝐞}b\mathbf{𝐝}\mathbf{𝐨}I\{\beta \}}$

Rozwiązanie

$\frac{\alpha ⟹\beta [x\mapsto e]}{\{\alpha \}x:=e\{\beta \}}$

$\frac{\alpha ⟹\gamma \{\gamma \wedge b\}I\{\gamma \}\gamma \wedge \mathrm{\neg }b⟹\beta }{\{\alpha \}\mathbf{𝐰}\mathbf{𝐡}\mathbf{𝐢}\mathbf{𝐥}\mathbf{𝐞}b\mathbf{𝐝}\mathbf{𝐨}I\{\beta \}}$

Ćwiczenie 3 (potęgowanie binarne)

Dowiedź poprawności częściowej poniższego programu:

$\{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\}$

Wyrażenie odd(q) ma wartość $\mathbf{𝐭}\mathbf{𝐫}\mathbf{𝐮}\mathbf{𝐞}$ wtedy i tylko wtedy, gdy q jest nieparzyste.

Rozwiązanie

Jako niezmiennik pętli przyjmijmy $N\equiv z\cdot p^q=x^y$. Oto odpowiednie anotacje naszego programu:

$\{y\ge 0\}$
$\{N[q\mapsto y][p\mapsto x][z\mapsto 1]\}$
z := 1; 
p := x; 
q := y;
while  $\{N\}$  q <> 0 do
(
  $\{N\wedge q\ne 0\}$
  if odd(q) then
  (
    $\{N\wedge q\ne 0\wedge \mathrm{o}\mathrm{d}\mathrm{d}(q)\}$
    $\{N[p\mapsto p\cdot p][q\mapsto q\mathrm{d}\mathrm{i}\mathrm{v}2][z\mapsto z\cdot p]\}$
    z := z * p
    $\{N[p\mapsto p\cdot p][q\mapsto q\mathrm{d}\mathrm{i}\mathrm{v}2]\}$
  )
  else
  (
    $\{N\wedge q\ne 0\wedge \ne \mathrm{o}\mathrm{d}\mathrm{d}(q)\}$
    $\{N[p\mapsto p\cdot p][q\mapsto q\mathrm{d}\mathrm{i}\mathrm{v}2]\}$
    skip
    $\{N[p\mapsto p\cdot p][q\mapsto q\mathrm{d}\mathrm{i}\mathrm{v}2]\}$
  )
  $\{N[p\mapsto p\cdot p][q\mapsto q\mathrm{d}\mathrm{i}\mathrm{v}2]\}$
  q := q div 2;
  $\{N[p\mapsto p\cdot p]\}$
  p := p * p
  $\{N\}$
)
$\{N\wedge q=0\}$
$\{z=x^y\}$

Po podstawieniu niezmiennika:

$\{y\ge 0\}$
$\{1\cdot x^y=x^y\}$
z := 1; 
p := x; 
q := y;
while  $\{z\cdot p^q=x^y\}$  q <> 0 do
(
  $\{z\cdot p^q=x^y\wedge q\ne 0\}$
  if odd(q) then
  (
    $\{z\cdot p^q=x^y\wedge q\ne 0\wedge \mathrm{o}\mathrm{d}\mathrm{d}(q)\}$
    $\{(z\cdot p)\cdot (p\cdot p{)}^{(q\mathrm{d}\mathrm{i}\mathrm{v}2)}=x^y\}$
    z := z * p
    $\{z\cdot (p\cdot p{)}^{(q\mathrm{d}\mathrm{i}\mathrm{v}2)}=x^y\}$
  )
  else
  (
    $\{z\cdot p^q=x^y\wedge q\ne 0\wedge \ne \mathrm{o}\mathrm{d}\mathrm{d}(q)\}$
    $\{z\cdot (p\cdot p{)}^{(q\mathrm{d}\mathrm{i}\mathrm{v}2)}=x^y\}$
    skip
    $\{z\cdot (p\cdot p{)}^{(q\mathrm{d}\mathrm{i}\mathrm{v}2)}=x^y\}$
  )
  $\{z\cdot (p\cdot p{)}^{(q\mathrm{d}\mathrm{i}\mathrm{v}2)}=x^y\}$
  q := q div 2;
  $\{z\cdot (p\cdot p{)}^q=x^y\}$
  p := p * p
  $\{z\cdot p^q=x^y\}$
)
$\{z\cdot p^q=x^y\wedge q=0\}$
$\{z=x^y\}$

Teraz pozostaje tylko pokazać następujące implikacje:

• $y\ge 0⟹1\cdot x^y=x^y$
• $z\cdot p^q=x^y\wedge q\ne 0\wedge \mathrm{o}\mathrm{d}\mathrm{d}(q)⟹(z\cdot p)\cdot (p\cdot p{)}^{(q\mathrm{d}\mathrm{i}\mathrm{v}2)}=x^y$
• $z\cdot p^q=x^y\wedge q\ne 0\wedge \ne \mathrm{o}\mathrm{d}\mathrm{d}(q)⟹z\cdot (p\cdot p{)}^{(q\mathrm{d}\mathrm{i}\mathrm{v}2)}=x^y$
• $z\cdot p^q=x^y\wedge q=0⟹z=x^y$

Zauważmy, że w niezmienniku nie wymagamy, aby $q\ge 0$, ponieważ nie jest to potrzebne do udowodnienia powyższych implikacji. Musimy tylko umówić się, na wszelki wypadek, jak działa operacja div, gdy jej argument jest ujemny. Przyjmijmy, że $q\mathrm{d}\mathrm{i}\mathrm{v}2=m$ wtedy i tylko wtedy, gdy największą liczbą parzystą, nie większą od $q$, jest $2\cdot m$.

Uwaga

Warunek $q\ge 0$ gwarantuje, że program się kończy. Fakt, że go nie potrzebujemy, wiąże się z tym, że dowodzimy tylko poprawność częściową: wynik będzie poprawny, o ile program się zakończy, ale wcale zakończyć się nie musi!

Pytanie: czy niezmiennik pętli jest napewno prawdziwy, gdy zmienna q ma wartość ujemną?

Ćwiczenie 4

Zaproponuj regułę dla instrukcji $\mathbf{𝐫}\mathbf{𝐞}\mathbf{𝐩}\mathbf{𝐞}\mathbf{𝐚}\mathbf{𝐭}I\mathbf{𝐮}\mathbf{𝐧}\mathbf{𝐭}\mathbf{𝐢}\mathbf{𝐥}b$.

Rozwiązanie

$\mathbf{𝐫}\mathbf{𝐞}\mathbf{𝐩}\mathbf{𝐞}\mathbf{𝐚}\mathbf{𝐭}I\mathbf{𝐮}\mathbf{𝐧}\mathbf{𝐭}\mathbf{𝐢}\mathbf{𝐥}b$ zachowuje się tak samo jak $I;\mathbf{𝐰}\mathbf{𝐡}\mathbf{𝐢}\mathbf{𝐥}\mathbf{𝐞}\mathrm{\neg }b\mathbf{𝐝}\mathbf{𝐨}I$. Stąd łatwo otrzymać regułę:

$\frac{\{\alpha \}I\{\beta \}\{\beta \wedge \mathrm{\neg }b\}I\{\beta \}}{\{\alpha \}\mathbf{𝐫}\mathbf{𝐞}\mathbf{𝐩}\mathbf{𝐞}\mathbf{𝐚}\mathbf{𝐭}I\mathbf{𝐮}\mathbf{𝐧}\mathbf{𝐭}\mathbf{𝐢}\mathbf{𝐥}b\{\beta \wedge b\}}$

Dwukrotnie odwołujemy się do poprawności częściowej instrukcji $I$ względem różnych asercji początkowych. Gdybyśmy chcieli tego uniknąć, moglibyśmy rozważyć $\alpha =\beta$, otrzymując regułę:

$\frac{\{\beta \}I\{\beta \}\{\beta \wedge \mathrm{\neg }b\}I\{\beta \}}{\{\beta \}\mathbf{𝐫}\mathbf{𝐞}\mathbf{𝐩}\mathbf{𝐞}\mathbf{𝐚}\mathbf{𝐭}I\mathbf{𝐮}\mathbf{𝐧}\mathbf{𝐭}\mathbf{𝐢}\mathbf{𝐥}b\{\beta \wedge b\}}$

Jeśli $\{\beta \}I\{\beta \}$ to $\{\beta \wedge \mathrm{\neg }b\}I\{\beta \}$. Zatem powyzszą regułę można uprościć:

$\frac{\{\beta \}I\{\beta \}}{\{\beta \}\mathbf{𝐫}\mathbf{𝐞}\mathbf{𝐩}\mathbf{𝐞}\mathbf{𝐚}\mathbf{𝐭}I\mathbf{𝐮}\mathbf{𝐧}\mathbf{𝐭}\mathbf{𝐢}\mathbf{𝐥}b\{\beta \wedge b\}}$

otrzymując regułę prostszą, ale słabszą: we wnętrzu pętli nie możemy korzystać z tego, że począwszy od drugiej iteracji nie zachodzi $b$!

Jeszcze inna możliwość to:

$\frac{\{\alpha \}I\{\beta \}\beta \wedge \mathrm{\neg }b⟹\alpha }{\{\alpha \}\mathbf{𝐫}\mathbf{𝐞}\mathbf{𝐩}\mathbf{𝐞}\mathbf{𝐚}\mathbf{𝐭}I\mathbf{𝐮}\mathbf{𝐧}\mathbf{𝐭}\mathbf{𝐢}\mathbf{𝐥}b\{\beta \wedge b\}}$

Zadania domowe

Ćwiczenie 1

Wyprowadź ostatnią regułę dla pętli $\mathbf{𝐫}\mathbf{𝐞}\mathbf{𝐩}\mathbf{𝐞}\mathbf{𝐚}\mathbf{𝐭}$, z pierwszej reguły.

Ćwiczenie 2

Napisz program obliczający największy wspólny dzielnik dwóch liczb i przeprowadź dowód poprawności częściowej.

Ćwiczenie 3

Przeprowadź dowód poprawności częściowej:

$\{x\ge 0\}$
a = 1; b := 1; y := 1;
while y <= x do
  y := y + 3*a + 3*b + 1;
  a = a + 2*b + 1;
  b := b + 1;
$\{(b-1{)}^3\le x<b^3\}$

Wskazówka

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