Semantyka i weryfikacja programów/Ćwiczenia 15: Różnice pomiędzy wersjami

Z Studia Informatyczne
Przejdź do nawigacjiPrzejdź do wyszukiwania
← poprzednia edycjanastępna edycja →
WizualnieWikikod
Sl (dyskusja | edycje)
101 edycji
Nie podano opisu zmian
Sl (dyskusja | edycje)
101 edycji
Nie podano opisu zmian
Linia 1: Linia 1:


== Zawartość ==
Ostatnie ćwiczenia poświęcone będa dowodzeniu poprawności całkowitej programów.
== Poprawność całkowita ==
{{cwiczenie|1 (potęgowanie binarne)|cw1|
Przeprowadź dowód poprawności całkowitej (poprawność częściowa plus własność stopu) potęgowania binarnego:
}}
<math>{\color{Red}[y \geq 0]}</math>
z := 1; p := x; q := y;
while q <> 0 do
  if odd(q) then
    z := z * p;
  q := q div 2;
  p := p * p
<math>{\color{Red}[z = x^y]}</math>
{{rozwiazanie||roz1|
<div class="mw-collapsible mw-made=collapsible mw-collapsed"><div class="mw-collapsible-content" style="display:none">
Intuicyjnie, pownniśmy wskazać wrażenie, którego wartość maleje w każdym obrocie pętli i jest zawsze nieujemna.
Naturalnym kandydatem jest wyrażenie <math>q</math>.
W dowodzie poprawności częściowej używaliśmy niezmiennika <math>N \, \equiv \, z \cdot p^q = x^y</math>.
Dla własności stopu potrzebujemy dodatkowo własności <math>q \geq 0</math>, więc naturalnym kandydatem jest niezmiennik
<math>N' \, \equiv \, z \cdot p^q = x^y \land q \leq 0</math>.
Dla formalnego dowodu lepiej, jeśli <math>N'</math> będzie miał parametr:
<math>N'(l) \, \equiv \, z \cdot p^q = x^y \land q = l</math>.
Formalnie rzecz biorąc, wykażemy:
<math>{\color{Red}[\exists l \geq 0. N'(l)]}</math>
while q <> 0 do
  if odd(q) then
    z := z * p;
  q := q div 2;
  p := p * p
<math>{\color{Red}[N'(0)]}</math>
i dodatkowo dwie implikacje:
* <math>y \geq 0 \, \implies \, \exists l \geq 0. N'(l)</math>
* <math>N'(0) \, \implies \, z = x^y</math>.
Stosując następującą regułe dla pętli (jest to odmiana reguły zaprezentowanej na wykładzie wygodna w tym zadaniu :)
<math>
\frac{l \div 2 \geq 0 \land N'(l) \implies b \quad {\color{Red}[l \div 2 \geq 0 \land N'(l)]} I {\color{Red}[N'(l \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)]}}
</math>
wystarczy dowieść:
  <math>{\color{Red}[l \div 2 \geq 0 \land N'(l)]}</math>
  if odd(q) then
    z := z * p;
  q := q div 2;
  p := p * p
  <math>{\color{Red}[N'(l \div 2)]}</math>
oraz kolejnych dwóch łatwych implikacji:
* <math>l \div 2 \geq 0 \land N'(l) \, \implies \, q \neq 0</math>
* <math>N'(0) \implies q = 0</math>.
Stosując teraz zwykłe reguły ,,przeciągamy" niezmiennik <math>N'(l \div 2)</math> w tył:
  <math>{\color{Red}[l \div 2 \geq 0 \land z \cdot p^q = x^y \land q = l]}</math>
  if odd(q) then
  (
    <math>{\color{Red}[l \div 2 \geq 0 \land z \cdot p^q = x^y \land q = l \land \odd(q)]}</math>
        <math>{\color{Green}\Downarrow}</math>
    <math>{\color{Red}[(z \cdot p) \cdot (p \cdot p)^(q \div 2) = x^y \land q \div 2 = l \div 2]}</math>
    z := z * p;
    <math>{\color{Red}[z \cdot (p \cdot p)^(q \div 2) = x^y \land q \div 2 = l \div 2]}</math>
  )
  <math>{\color{Red}[z \cdot (p \cdot p)^(q \div 2) = x^y \land q \div 2 = l \div 2]}</math>
  q := q div 2;
  <math>{\color{Red}[z \cdot (p \cdot p)^q = x^y \land q = l \div 2]}</math>
  p := p * p
  <math>{\color{Red}[z \cdot p^q = x^y \land q = l \div 2]}</math>
W przyszlości będziemy pomijać formalny dowód własności stpu 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  <math>{\color{Red}[N]}</math>  q <> 0 do <math>{\color{Red}[\mathbf{decr}\, q \,\mathbf{in}\, \nat \,\mathbf{wrt}\, >]}</math>
(
  if odd(q) then
    z := z * p;
  q := q div 2;
  p := p * p
)
<math>{\color{Red}[N \land \neg \odd(q)]}</math>
...
</div></div>
}}
{{cwiczenie|2|cw2|
Przeprowadź dowód poprawności całkowitej poniższego programu.
}}
<math>{\color{Red}\{n \geq 0\}}</math>
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;
 
<math>{\color{Red}\{s = n^3\}}</math>
{{wskazowka|||
<math>
(m + 1)^3 \, = \, m^3 + 3 \cdot m^2 + 3 \cdot m + 1
</math>
<math>
\Sigma_{j = 1}^m \, = \, \frac{m \cdot (m+1)}{2}
</math>
}}
{{rozwiazanie| (poprawność częściowa)|roz1.1|
<div class="mw-collapsible mw-made=collapsible mw-collapsed"><div class="mw-collapsible-content" style="display:none">
Zacznijmy od niezmiennika dla pętli zewnętrznej: <math>N_1 \, \equiv \, s = i^3 \land 1 \leq i \leq n</math>.
<math>{\color{Red}\{n \geq 1\}}</math>
  <math>{\color{Green}\Downarrow}</math>        <span style="color:brown">// 1 </span>
<math>{\color{Red}\{N_1[i \mapsto 1][s \mapsto 1]\}}</math>
s := 1;
i := 1;
while  <math>{\color{Red}\{N_1\}}</math>  i < n do
(
  <math>{\color{Red}\{N_1 \land i < n\}}</math>
  k := 1;
  l := 0;
  p := 1;
  <math>{\color{Red}\{N_1 \land i < n \land k = 1 \land l = 0 \land p = 1\}}</math>
  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;
  <math>{\color{Red}\{N_1\}}</math>
)
<math>{\color{Red}\{N_1 \land i \geq n\}}</math>
  <math>{\color{Green}\Downarrow}</math>        <span style="color:brown">// 2 </span>
<math>{\color{Red}\{s = n^3\}}</math>
Dwie zaznaczone implikacja są łatwe do udowodnienia.
Trudniej jest znależć niezmiennik dla pętli wewnętrznej.
Przede wszystkim zauważmy, że jeśli <math>N_1</math> ma się ,,odnawiać" po każdym obrocie zewnętrznej pętli, to wartość dodawana do zmiennej <math>s</math> powinna wynosić:
<math>
(i+1)^3 - i^3 = 3 \cdot n^2 + 3 \cdot n = 3 \cdot (i^2 + i) = 3 \cdot i \cdot (i+1).
</math>
Zatem pętla wewnętrzna powinna prawdopodobnie obliczać na zmiennej <math>k</math> wartość <math>\frac{i \cdot (i+1)}{2} = 1 + 2 + \ldots + i</math>.
Jeśli uważnie przyjrzymy się pętli wewnętrznej, to zaobserwujemy, że zmienna <math>k</math> przechowuje wartość
<math>1 + 2 + \ldots + l</math> plus ,,zaczęte" l+1, czyli plus <math>p</math>.
Spróbujmy niezmiennik postaci:
<math>
N_2 \, \equiv \, k = (1 + 2 + \ldots l) + p \land \ldots
</math>
Pozostaje jeszcze ustalić ograniczenia górne lub dolne zmiennych p, l.
Po pierwsze, zawsze zachodzi <math>p \leq l+1</math>.
Po drugie, oczekujemy, że spełniony będzie warunek <math>l < i</math>.
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:
<math>
N_2 \, \equiv \, k = (1 + 2 + \ldots l) + p \land 1 \leq p \leq l+1 \leq i.
</math>
Oto odpowiednie anotacje całego programu:
<math>{\color{Red}\{n \geq 1\}}</math>
  <math>{\color{Green}\Downarrow}</math>        <span style="color:brown">// 1 </span>
<math>{\color{Red}\{N_1[i \mapsto 1][s \mapsto 1]\}}</math>
s := 1;
i := 1;
while  <math>{\color{Red}\{N_1\}}</math>  i < n do
(
  <math>{\color{Red}\{N_1 \land i < n\}}</math>
  k := 1;
  l := 0;
  p := 1;
  <math>{\color{Red}\{N_1 \land i < n \land k = 1 \land l = 0 \land p = 1\}}</math>
    <math>{\color{Green}\Downarrow}</math>        <span style="color:brown">// 3 </span>
  <math>{\color{Red}\{N_2\}}</math>
  while  <math>{\color{Red}\{N_2\}}</math>  p < i do
  (
    k := k + 1;
    if l < p then
    (
      l := l + 1;
      p := 1
    )
    else
    (
      p := p + 1;
    )
  )
  <math>{\color{Red}\{N_2 \land p \geq i\}}</math>
    <math>{\color{Green}\Downarrow}</math>        <span style="color:brown">// 4 </span>
  <math>{\color{Red}\{N_1[i \mapsto i{+}1][s \mapsto s {+} 6 \cdot k {+} p {-} l]\}}</math>
  s := s + 6 * k + p - l;
  i := i + 1;
  <math>{\color{Red}\{N_1\}}</math>
)
<math>{\color{Red}\{N_1 \land i \geq n\}}</math>
  <math>{\color{Green}\Downarrow}</math>        <span style="color:brown">// 2 </span>
<math>{\color{Red}\{s = n^3\}}</math>
Musimy teraz udowodnić dwie kolejne zaznaczone powyżej implikacje:
* <math>N_1 \land i < n \land k = 1 \land l = 0 \land p = 1 \, \implies \, N_2</math>
* <math>N_2 \land p \geq i \, \implies \, N_1[i \mapsto i{+}1][s \mapsto s {+} 6 \cdot k {+} p {-} l]</math>
Pierwsza z nich jest oczywista, natomiast nie jesteśmy w stanie dowieść drugiej!
Jest tak dlatego, że w <math>N_2</math> nie mamy informacji o tym, że przed wejściem do pętli wewnętrznej
zachodziło <math>s = i^3</math>, a jest to niezbędne w dowodzie.
Zmodyfikujmy <math>N_2</math> następująco:
<math>
N_2 \, \equiv \, s = i^3 \land k = (1 + 2 + \ldots l) + p \land 1 \leq p \leq l+1 \leq i
</math>
i wróćmy do ostatniej z implikacji powyżej.
Wciąż brakuje nam pewnych informacji!
Tym razem nie potrafimy pokazac, że zachodzi <math>i{+}1 \leq n</math>, co stanowi część formuły
<math>N_1[i \mapsto i{+}1][s \mapsto s {+} 6 \cdot k {+} p {-} l]</math>.
Powinniśmy dodać do <math>N_2</math> warunek <math>i < n</math>, który zachodzi zawsze po wejściu do pętli zewnętrznej.
Otrzymujemy ostatecznie:
<math>
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.
</math>
Teraz dowód ostatniej implikacji jest możliwy.
Zauważmy w szczególności, że warunek <math>p \geq i</math> w połączeniu z warunkiem <math>p \leq l{+}1 \leq i</math> obecnym w <math>N_2</math>
daje nam <math>p = l{+}1</math>. Stąd faktycznie zachodzi:
<math>
s {+} 6 \cdot k {+} p {-} l \, = \, s + (1 + 2 + \ldots + l) + 1
</math>
a ponieważ <math>p = i</math>, otrzymujemy:
<math>
s {+} 6 \cdot k {+} p {-} l \, = \, s + 6 \cdot (1 + 2 + \ldots + l) + 1 \, = \, s + 6 \cdot (1 + 2 + \ldots + i) + 1 \, = \, s + 6 \cdot \frac{i \cdot (i+1)}{2} + 1 \, = \,
s + 3 \cdot i^2 + 4 \cdot i + 1 = (i+1)^3.
</math>
Na koniec pozostał nam dowód poprawności instrukcji wewnętrznej w wewnętrznej pętli:
    ...
   
    <math>{\color{Red}\{N_2 \land p < i\}}</math>
    k := k + 1;
    <math>{\color{Red}\{?\}}</math>
    if l < p then
    (
      l := l + 1;
      p := 1
    )
    else
    (
      p := p + 1;
    )
    <math>{\color{Red}\{N_2\}}</math>
   
    ...
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 <math>k = (1 + 2 + \ldots l) + p</math> w <math>N_2 \land p < i</math>,
czyli zastąpić je przez <math>k = (1 + 2 + \ldots l) + p + 1</math>.
Oznaczmmy przez <math>N'</math> asercję, którą otrzymujemy w ten sposób z <math>N_2</math>:
<math>
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.
</math>
Oto szczegółowa anotacja rozważanego fragmentu programu:
    ...
   
    <math>{\color{Red}\{N_2 \land p < i\}}</math>
      <math>{\color{Green}\Downarrow}</math>        <span style="color:brown">// 5 </span>
    <math>{\color{Red}\{N'[k \mapsto k{+}1] \land p < i\}}</math>
    k := k + 1;
    <math>{\color{Red}\{N' \land p < i\}}</math>
    if l < p then
    (
      <math>{\color{Red}\{N' \land l < p\}}</math>
        <math>{\color{Green}\Downarrow}</math>        <span style="color:brown">// 6 </span>
      <math>{\color{Red}\{N_2[p \mapsto 1][l mapsto l{+}1]\}}</math>
      l := l + 1;
      p := 1
      <math>{\color{Red}\{N_2\}}</math>
    )
    else
    (
      <math>{\color{Red}\{N' \land l \geq p\}}</math>
        <math>{\color{Green}\Downarrow}</math>        <span style="color:brown">// 7 </span>
      <math>{\color{Red}\{N_2[p \mapsto p{+}1]\}}</math>
      p := p + 1;
      <math>{\color{Red}\{N_2\}}</math>
    )
    <math>{\color{Red}\{N_2\}}</math>
   
    ...
oraz implikacje niezbędne dla dokończenia dowodu:
* <math>N_2 \land p < i \, \implies \, N'[k \mapsto k{+}1] \land p < i</math>
* <math>N' \land l < p < i \, \implies \, N_2[p \mapsto 1][l mapsto l{+}1]</math>
* <math>N' \land l \geq p < i \, \implies \, N_2[p \mapsto p{+}1]</math>.
</div></div>
}}
{{rozwiazanie| (poprawność calkowita)|roz1.2|
<div class="mw-collapsible mw-made=collapsible mw-collapsed"><div class="mw-collapsible-content" style="display:none">
Własność stopu pętli zewnętrznej łatwo jest pokazać, gdyż w każdym obiegu rośnie wartość zmiennej i, czyli maleje wartość wyrażeni <math>n - i</math>.
Dodatkowo <math>n - i \geq 0</math> zagwarantowane jest przez niezmiennik <math>N_1</math>.
Trudniej jest pokazać własność stopu pętli wewnętrznej.
Choć dozór tej pętli to <math>p < i</math>, 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 <math>i - l</math> nie maleje po każdym obiegu pętli!
Może ono pozostać niezmienione, ale wtedy rośnie na pewno wartość zmiennej p, czyli maleje <math>i - p</math>.
Widać zatem, że warto tutaj wziąc pod uwagę porządek leksykograficzny par liczb: para wartości wyrażeń <math>\langle i - l, i - p \rangle</math>
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 <math>N_2</math>.
Odpowiednie anotacje całego programu to:
<math>{\color{Red}[n \geq 1]}</math>
  <math>{\color{Green}\Downarrow}</math>        <span style="color:brown">// 1 </span>
<math>{\color{Red}[N_1[i \mapsto 1][s \mapsto 1]]}</math>
s := 1;
i := 1;
while  <math>{\color{Red}[N_1]}</math>  i < n do <math>{\color{Red}[\mathbf{decr}\, n{-}i \,\mathbf{in}\, \nat \,\mathbf{wrt}\, >]}</math>
(
  <math>{\color{Red}[N_1 \land i < n]}</math>
  k := 1;
  l := 0;
  p := 1;
  <math>{\color{Red}[N_1 \land i < n \land k = 1 \land l = 0 \land p = 1]}</math>
    <math>{\color{Green}\Downarrow}</math>        <span style="color:brown">// 3 </span>
  <math>{\color{Red}[N_2]}</math>
  while  <math>{\color{Red}[N_2]}</math>  p < i do <math>{\color{Red}[\mathbf{decr}\, \langle i {-} l, i {-} p \rangle \,\mathbf{in}\, {\nat}^2 \,\mathbf{wrt}\, <_{\mbox{lex}}]}</math>
  (
    ...
    if l < p then
    (
      l := l + 1;
      p := 1
    )
    else
    (
      p := p + 1;
    )
  )
  <math>{\color{Red}[N_2 \land p \geq i]}</math>
    <math>{\color{Green}\Downarrow}</math>        <span style="color:brown">// 4 </span>
  <math>{\color{Red}[N_1[i \mapsto i{+}1][s \mapsto s {+} 6 \cdot k {+} p {-} l]]}</math>
  s := s + 6 * k + p - l;
  i := i + 1;
  <math>{\color{Red}[N_1]}</math>
)
<math>{\color{Red}[N_1 \land i \geq n]}</math>
  <math>{\color{Green}\Downarrow}</math>        <span style="color:brown">// 2 </span>
<math>{\color{Red}[s = n^3]}</math>
</div></div>
}}
 
== Zadania domowe ==
{{cwiczenie|1|cw1.dom|
Przeprowadź dowód poprawności całkowitej poniższego programu.
}}
<math>{\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])\}}</math>
i := 1; j := 2 * n;
while A[i] < A[j] do
  ,,zamień A[i] i A[j]";
  i := i + 1;
  j := j - 1;
<math>{\color{Red}\{forall x, y. 1 \leq x \leq n < y \leq 2 \cdot n \implies A[x] \geq A[y]\}}</math>

Wersja z 08:30, 14 sie 2006


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≥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=xy]


Rozwiązanie

{{{3}}}


Ćwiczenie 2

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


{n≥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=n3}


Wskazówka

(m+1)3=m3+3⋅m2+3⋅m+1 Σj=1m=m⋅(m+1)2


Rozwiązanie (poprawność częściowa)

{{{3}}}

Rozwiązanie (poprawność calkowita)

{{{3}}}


Zadania domowe

Ćwiczenie 1

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


{(forallx.1≤x<n⟹A[x]≤A[x+1])∧(forallx.n+1≤x<2⋅n⟹A[x]≤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;
{forallx,y.1≤x≤n<y≤2⋅n⟹A[x]≥A[y]}
Źródło: „https://wazniak.mimuw.edu.pl/index.php?title=Semantyka_i_weryfikacja_programów/Ćwiczenia_15&oldid=16135”