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:

${\color {Red}\{n\geq 1\}}$
x := 1; y := 0;
while x <= n do
  y := y + x;
  x := x + 1
${\color {Red}\{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ę:

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

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

${\color {Red}\{n\geq 1\}}$
x := 1; 
y := 0;
${\color {Red}\{n\geq 0\land x=1\land y=0\}}$

${\color {Red}\{n\geq 0\land x=1\land y=0\}}$
while x <= n do
(
  y := y + x;
  x := x + 1
)
${\color {Red}\{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\geq 0\land x=1\land y=0\,\implies \,N$
• $N\land x>n\,\implies \,y={\frac {n{\cdot }(n+1)}{2}}$

oraz prawdziwa jest trójka:

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

Aby dowieść tej ostatniej, musimy pokazać:

${\color {Red}\{N\land x\leq n\}}$
y := y + x;
x := x + 1
${\color {Red}\{N\}}$

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

${\color {Red}\{N\land x\leq n\}}$
y := y + x;
${\color {Red}\{?\}}$
x := x + 1
${\color {Red}\{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:

${\color {Red}\{N\land x\leq n\}}$
y := y + x;
${\color {Red}\{N[x\mapsto x{+}1]\}}$
x := x + 1
${\color {Red}\{N\}}$

Teraz musimy tylko pokazać trójkę:

${\color {Red}\{N\land x\leq n\}}$
y := y + x;
${\color {Red}\{N[x\mapsto x{+}1]\}}$

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

${\color {Red}\{N\land x\leq n\}}$
    ${\color {Green}\Downarrow }$          // tę implikację należy udowodnić 
${\color {Red}\{N[x\mapsto x{+}1][y\mapsto y{+}x]\}}$
y := y + x;
${\color {Red}\{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:

${\color {Red}\{n\geq 1\}}$
x := 1; 
${\color {Red}\{n\geq 0\land x=1\}}$
y := 0;
${\color {Red}\{n\geq 0\land x=1\land y=0\}}$
    ${\color {Green}\Downarrow }$        // 1 
${\color {Red}\{N\}}$
while x <= n do
(
  ${\color {Red}\{N\land x\leq n\}}$
      ${\color {Green}\Downarrow }$        // 2 
  ${\color {Red}\{N[x\mapsto x{+}1][y\mapsto y{+}x]\}}$
  y := y + x;
  ${\color {Red}\{N[x\mapsto x{+}1]\}}$
  x := x + 1
  ${\color {Red}\{N\}}$
)
${\color {Red}\{N\land x>n\}}$
    ${\color {Green}\Downarrow }$        // 3 
${\color {Red}\{y={\frac {n{\cdot }(n+1)}{2}}\}}$

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

1. $n\geq 0\land x=1\land y=0\,\implies \,N$
2. $N\land x\leq n\,\implies \,N[x\mapsto x{+}1][y\mapsto y{+}x]$
3. $N\land x>n\,\implies \,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}}\land x\leq n{+}1$.

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

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

$N\,\equiv \,y=1{+}2{+}\ldots {+}(x{-}1)\land x\leq n{+}1.$

Pytanie: dlaczego nie potrzebowaliśmy warunku $x\geq 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:

${\color {Red}\{n\geq 1\}}$
x := 1; 
${\color {Red}\{n\geq 0\land x=1\}}$
y := 0;
${\color {Red}\{n\geq 0\land x=1\land y=0\}}$
    ${\color {Green}\Downarrow }$        // 1 
${\color {Red}\{N\}}$
while  ${\color {Red}\{N\}}$  x <= n do
(
  ${\color {Red}\{N\land x\leq n\}}$

  ...

Wariant:

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

${\color {Red}\{n\geq 0\land x=1\land 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ć:

${\color {Red}\{n\geq 1\}}$
x := 1; 
y := 0;
${\color {Red}\{N\}}$

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

${\color {Red}\{n\geq 1\}}$
    ${\color {Green}\Downarrow }$        // 1 
${\color {Red}\{N[y\mapsto 0][x\mapsto 1]\}}$
x := 1; 
${\color {Red}\{N[y\mapsto 0]\}}$
y := 0;
${\color {Red}\{N\}}$

Ostatecznie, anotacje programu wyglądałyby tak:

${\color {Red}\{n\geq 1\}}$
    ${\color {Green}\Downarrow }$        // 1 
${\color {Red}\{N[y\mapsto 0][x\mapsto 1]\}}$
x := 1; 
${\color {Red}\{N[y\mapsto 0]\}}$
y := 0;
while  ${\color {Red}\{N\}}$  x <= n do
(
  ${\color {Red}\{N\land x\leq n\}}$
      ${\color {Green}\Downarrow }$        // 2 
  ${\color {Red}\{N[x\mapsto x{+}1][y\mapsto y{+}x]\}}$
  y := y + x;
  ${\color {Red}\{N[x\mapsto x{+}1]\}}$
  x := x + 1
  ${\color {Red}\{N\}}$
)
${\color {Red}\{N\land x>n\}}$
    ${\color {Green}\Downarrow }$        // 3 
${\color {Red}\{y={\frac {n{\cdot }(n+1)}{2}}\}}$

a pierwsza z trzech implikacji to: $n\geq 1\,\implies \,N[y\mapsto 0][x\mapsto 1]$.

Ćwiczenie 2

Uzupełnij poniższe reguły:

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

${\frac {?}{{\color {Red}\{\alpha \}}\mathbf {while} \,b\,\mathbf {do} \,I{\color {Red}\{\beta \}}}}$

Rozwiązanie

${\frac {\alpha \,\implies \,\beta [x\mapsto e]}{{\color {Red}\{\alpha \}}x:=e{\color {Red}\{\beta \}}}}$

${\frac {\alpha \,\implies \,\gamma \quad {\color {Red}\{\gamma \land b\}}I{\color {Red}\{\gamma \}}\quad \gamma \land \neg b\,\implies \,\beta }{{\color {Red}\{\alpha \}}\mathbf {while} \,b\,\mathbf {do} \,I{\color {Red}\{\beta \}}}}$

Ćwiczenie 3 (potęgowanie binarne)

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

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

Wyrażenie odd(q) ma wartość $\mathbf {true}$ 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:

${\color {Red}\{y\geq 0\}}$
${\color {Red}\{N[q\mapsto y][p\mapsto x][z\mapsto 1]\}}$
z := 1; 
p := x; 
q := y;
while  ${\color {Red}\{N\}}$  q <> 0 do
(
  ${\color {Red}\{N\land q\neq 0\}}$
  if odd(q) then
  (
    ${\color {Red}\{N\land q\neq 0\land \,\mathrm {odd} (q)\}}$
    ${\color {Red}\{N[p\mapsto p{\cdot }p][q\mapsto q\,\mathrm {div} \,2][z\mapsto z{\cdot }p]\}}$
    z := z * p
    ${\color {Red}\{N[p\mapsto p{\cdot }p][q\mapsto q\,\mathrm {div} \,2]\}}$
  )
  else
  (
    ${\color {Red}\{N\land q\neq 0\land \neq \,\mathrm {odd} (q)\}}$
    ${\color {Red}\{N[p\mapsto p{\cdot }p][q\mapsto q\,\mathrm {div} \,2]\}}$
    skip
    ${\color {Red}\{N[p\mapsto p{\cdot }p][q\mapsto q\,\mathrm {div} \,2]\}}$
  )
  ${\color {Red}\{N[p\mapsto p{\cdot }p][q\mapsto q\,\mathrm {div} \,2]\}}$
  q := q div 2;
  ${\color {Red}\{N[p\mapsto p{\cdot }p]\}}$
  p := p * p
  ${\color {Red}\{N\}}$
)
${\color {Red}\{N\land q=0\}}$
${\color {Red}\{z=x^{y}\}}$

Po podstawieniu niezmiennika:

${\color {Red}\{y\geq 0\}}$
${\color {Red}\{1{\cdot }x^{y}=x^{y}\}}$
z := 1; 
p := x; 
q := y;
while  ${\color {Red}\{z{\cdot }p^{q}=x^{y}\}}$  q <> 0 do
(
  ${\color {Red}\{z{\cdot }p^{q}=x^{y}\land q\neq 0\}}$
  if odd(q) then
  (
    ${\color {Red}\{z{\cdot }p^{q}=x^{y}\land q\neq 0\land \,\mathrm {odd} (q)\}}$
    ${\color {Red}\{(z{\cdot }p){\cdot }(p{\cdot }p)^{(q\,\mathrm {div} \,2)}=x^{y}\}}$
    z := z * p
    ${\color {Red}\{z{\cdot }(p{\cdot }p)^{(q\,\mathrm {div} \,2)}=x^{y}\}}$
  )
  else
  (
    ${\color {Red}\{z{\cdot }p^{q}=x^{y}\land q\neq 0\land \neq \,\mathrm {odd} (q)\}}$
    ${\color {Red}\{z{\cdot }(p{\cdot }p)^{(q\,\mathrm {div} \,2)}=x^{y}\}}$
    skip
    ${\color {Red}\{z{\cdot }(p{\cdot }p)^{(q\,\mathrm {div} \,2)}=x^{y}\}}$
  )
  ${\color {Red}\{z{\cdot }(p{\cdot }p)^{(q\,\mathrm {div} \,2)}=x^{y}\}}$
  q := q div 2;
  ${\color {Red}\{z{\cdot }(p{\cdot }p)^{q}=x^{y}\}}$
  p := p * p
  ${\color {Red}\{z{\cdot }p^{q}=x^{y}\}}$
)
${\color {Red}\{z{\cdot }p^{q}=x^{y}\land q=0\}}$
${\color {Red}\{z=x^{y}\}}$

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

• $y\geq 0\,\implies \,1{\cdot }x^{y}=x^{y}$
• $z{\cdot }p^{q}=x^{y}\land q\neq 0\land \,\mathrm {odd} (q)\,\implies \,(z{\cdot }p){\cdot }(p{\cdot }p)^{(q\,\mathrm {div} \,2)}=x^{y}$
• $z{\cdot }p^{q}=x^{y}\land q\neq 0\land \neq \,\mathrm {odd} (q)\,\implies \,z{\cdot }(p{\cdot }p)^{(q\,\mathrm {div} \,2)}=x^{y}$
• $z{\cdot }p^{q}=x^{y}\land q=0\,\implies \,z=x^{y}$

Zauważmy, że w niezmienniku nie wymagamy, aby $q\geq 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 {div} \,2=m$ wtedy i tylko wtedy, gdy największą liczbą parzystą, nie większą od $q$, jest $2{\cdot }m$.

Uwaga

Warunek $q\geq 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 {repeat} \,I\,\mathbf {until} \,b$.

Rozwiązanie

$\mathbf {repeat} \,I\,\mathbf {until} \,b$ zachowuje się tak samo jak $I;\mathbf {while} \,\neg b\,\mathbf {do} \,I$. Stąd łatwo otrzymać regułę:

${\frac {{\color {Red}\{\alpha \}}I{\color {Red}\{\beta \}}\quad {\color {Red}\{\beta \land \neg b\}}I{\color {Red}\{\beta \}}}{{\color {Red}\{\alpha \}}\mathbf {repeat} \,I\,\mathbf {until} \,b{\color {Red}\{\beta \land 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 {{\color {Red}\{\beta \}}I{\color {Red}\{\beta \}}\quad {\color {Red}\{\beta \land \neg b\}}I{\color {Red}\{\beta \}}}{{\color {Red}\{\beta \}}\mathbf {repeat} \,I\,\mathbf {until} \,b{\color {Red}\{\beta \land b\}}}}$

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

${\frac {{\color {Red}\{\beta \}}I{\color {Red}\{\beta \}}}{{\color {Red}\{\beta \}}\mathbf {repeat} \,I\,\mathbf {until} \,b{\color {Red}\{\beta \land 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 {{\color {Red}\{\alpha \}}I{\color {Red}\{\beta \}}\quad \beta \land \neg b\implies \alpha }{{\color {Red}\{\alpha \}}\mathbf {repeat} \,I\,\mathbf {until} \,b{\color {Red}\{\beta \land b\}}}}$

Zadania domowe

Ćwiczenie 1

Wyprowadź ostatnią regułę dla pętli $\mathbf {repeat} \,$ 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:

${\color {Red}\{x\geq 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;
${\color {Red}\{(b-1)^{3}\leq x<b^{3}\}}$

Wskazówka

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