Semantyka i weryfikacja programów/Ćwiczenia 13: 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
Dorota (dyskusja | edycje)
376 edycji
Nie podano opisu zmian
Linia 1: Linia 1:


== Zawartość ==
== Zawartość ==


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




Linia 41: Linia 40:




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


Linia 98: Linia 97:


a następnie niezależnie dowieść poprawność każdej z dwóch nstrukcji.
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ł.
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:
Jeśli zastosujemy ją do drugiego przypisania "x := x + 1", otrzymamy:




Linia 127: Linia 126:




Skoro dwie asercje ,,spotkały się", wystarczy teraz udowodnić implikację.
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.  
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:
Podsumowując, poniższe anotacje całego programu powinny stanowić dowód poprawności częściowej:


Linia 155: Linia 154:




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


# <math>n \geq 0 \land x = 1 \land y = 0 \, \implies \, N</math>
# <math>n \geq 0 \land x = 1 \land y = 0 \, \implies \, N</math>
Linia 163: Linia 162:
Co ciekawe, to wszystko uczyniliśmy nie wiedząc wogóle, jaki jest niezmiennik pętli!
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ć.
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.
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.
Należy oczywiście uwzględnić również implikacje, które wypisaliśmy powyżej.


Linia 169: Linia 168:


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


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


Linia 218: Linia 217:




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




Linia 398: Linia 397:
* <math>z {\cdot} p^q = x^y \land q=0 \, \implies \, z = x^y</math>
* <math>z {\cdot} p^q = x^y \land q=0 \, \implies \, z = x^y</math>


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


{{uwaga|||
{{uwaga|||
Warunek <math>q \geq 0</math> gwarantuje, że program się kończy.
Warunek <math>q \geq 0</math> gwarantuje, że program się kończy.
Fakt, że go nie potrzebujemy wiąże się z tym, że dowodzimy tylko poprawność częściową:
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!
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ą?
'''Pytanie:''' czy niezmiennik pętli jest napewno prawdziwy, gdy zmienna q ma wartość ujemną?


</div></div>
</div></div>
Linia 435: Linia 434:
</math>
</math>


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


Linia 452: Linia 451:
</math>
</math>


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 <math>b</math>!  
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 <math>b</math>!  


Jeszcze inna możliwość to:
Jeszcze inna możliwość to:

Wersja z 15:09, 29 wrz 2006

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≥1}
x := 1; y := 0;
while x <= n do
  y := y + x;
  x := x + 1
{y=n⋅(n+1)2}


Rozwiązanie

{{{3}}}


Ćwiczenie 2

Uzupełnij poniższe reguły:

?{α}x:=e{β}

?{α}𝐰𝐡𝐢𝐥𝐞b𝐝𝐨I{β}


Rozwiązanie

{{{3}}}


Ćwiczenie 3 (potęgowanie binarne)

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


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


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

Rozwiązanie

{{{3}}}


Ćwiczenie 4

Zaproponuj regułę dla instrukcji 𝐫𝐞𝐩𝐞𝐚𝐭I𝐮𝐧𝐭𝐢𝐥b.


Rozwiązanie

{{{3}}}


Zadania domowe

Ćwiczenie 1

Wyprowadź ostatnią regułę dla pętli 𝐫𝐞𝐩𝐞𝐚𝐭 z pierwszej reguły.


Ćwiczenie 2

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


Ćwiczenie 3

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


{x≥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≤x<b3}


Wskazówka

(m+1)3=m3+3⋅m2+3⋅m+1

Źródło: „https://wazniak.mimuw.edu.pl/index.php?title=Semantyka_i_weryfikacja_programów/Ćwiczenia_13&oldid=59866”