Semantyka i weryfikacja programów/Ćwiczenia 13

From Studia Informatyczne

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