Semantyka i weryfikacja programów/Ćwiczenia 2: Różnice pomiędzy wersjami
Z Studia Informatyczne
Przejdź do nawigacjiPrzejdź do wyszukiwania
Nie podano opisu zmian |
Nie podano opisu zmian |
||
| Linia 1: | Linia 1: | ||
== Zawartość == | == Zawartość == | ||
| Linia 89: | Linia 88: | ||
</math> | </math> | ||
a konfiguracje końcowe to <math>\mathbf{State}</math> | a konfiguracje końcowe to <math>\mathbf{State}</math>, aczkolwiek konfiguracje ze zbioru <math>\mathbf{Num} \, \cup \, \mathbf{Bool}</math> pełnią podobną rolę dla wyrażeń arytmetycznych i boolowskich jako konfiguracje końcowe dla instrukcji. | ||
Przypomnijmy, że <math>\mathbf{Stmt}</math> oznacza zbiór instrukcji, <math>I \in \mathbf{Stmt}</math>. | Przypomnijmy, że <math>\mathbf{Stmt}</math> oznacza zbiór instrukcji, <math>I \in \mathbf{Stmt}</math>. | ||
| Linia 101: | Linia 100: | ||
Podobnie jak poprzednio, zakładamy tutaj dla wygody, że <math>\mathbf{Num} \subseteq \mathbf{Exp}</math> oraz <math>\mathbf{Bool} \subseteq \mathbf{BExp}</math>. | Podobnie jak poprzednio, zakładamy tutaj dla wygody, że <math>\mathbf{Num} \subseteq \mathbf{Exp}</math> oraz <math>\mathbf{Bool} \subseteq \mathbf{BExp}</math>. | ||
Pozwala nam to nie odróżniać stałych występujących w wyrażeniach a zatem pojawiających się po lewej stonie tranzycji od wartości im odpowiadających pojawiających się po prawej stronie. | Pozwala nam to nie odróżniać stałych występujących w wyrażeniach, a zatem pojawiających się po lewej stonie tranzycji od wartości im odpowiadających, pojawiających się po prawej stronie. | ||
Przejdźmy do spójników logicznych, powiedzmy <math>b_1 \land b_2</math>. | Przejdźmy do spójników logicznych, powiedzmy <math>b_1 \land b_2</math>. | ||
| Linia 140: | Linia 139: | ||
</math> | </math> | ||
Reguły ''równoległe'' otrzymujemy jako sumę reguł lewo- i prawostronnych (w sumie 6 reguł). Zauważmy, że obliczanie wyrażeń <math>b_1</math> i <math>b_2</math> odbywa się teraz w tzw. | Reguły ''równoległe'' otrzymujemy jako sumę reguł lewo- i prawostronnych (w sumie 6 reguł). Zauważmy, że obliczanie wyrażeń <math>b_1</math> i <math>b_2</math> odbywa się teraz w tzw. "przeplocie": Pojedynczy krok polega na wykonaniu jednego kroku obliczenia <math>b_1</math> albo jednego kroku obliczenia <math>b_2</math>. | ||
Zwróćmy też uwagę, że nasze tranzycje nie posiadają teraz własności ''determinizmu'': wyrażenie <math>b_1 \land b_2</math> może wyewoluować w pojedyńczym kroku albo do <math>b'_1 \land b_2</math> albo do <math>b_1 \land b'_2</math>. | Zwróćmy też uwagę, że nasze tranzycje nie posiadają teraz własności ''determinizmu'': wyrażenie <math>b_1 \land b_2</math> może wyewoluować w pojedyńczym kroku albo do <math>b'_1 \land b_2</math> albo do <math>b_1 \land b'_2</math>. | ||
Na szczęście końcowy wynik, do jakiego oblicza się wyrażenie jest zawsze taki sam, niezależnie od przeplotu. | Na szczęście końcowy wynik, do jakiego oblicza się wyrażenie, jest zawsze taki sam, niezależnie od przeplotu. | ||
Oto reguły dla negacji: | Oto reguły dla negacji: | ||
| Linia 172: | Linia 171: | ||
Reguły powyższe zależą od semantyki wyrażen arytmetycznych. | Reguły powyższe zależą od semantyki wyrażen arytmetycznych. | ||
Zauważmy, że ponownie pozostawiliśmy dowolność jeśli chodzi o kolejność obliczania wyrażeń arytmetycznych <math>e_1</math> i <math>e_2</math>. | Zauważmy, że ponownie pozostawiliśmy dowolność, jeśli chodzi o kolejność obliczania wyrażeń arytmetycznych <math>e_1</math> i <math>e_2</math>. | ||
Jako pierwszą z instrukcji rozważmy przypisanie. | Jako pierwszą z instrukcji rozważmy przypisanie. | ||
| Linia 225: | Linia 224: | ||
Istnieją inne możliwe rozwiązania w stylu małych kroków. | Istnieją inne możliwe rozwiązania w stylu małych kroków. | ||
Jedno z nich oparte jest na pomyśle, aby | Jedno z nich oparte jest na pomyśle, aby "rozwinąć" pętlę <math>\mathbf{while}\,</math> zanim obliczymy wartość dozoru <math>b</math>. | ||
Jedyną reguła dla pętli <math>\mathbf{while}\,</math> byłaby wtedy reguła: | Jedyną reguła dla pętli <math>\mathbf{while}\,</math> byłaby wtedy reguła: | ||
| Linia 266: | Linia 265: | ||
Zacznijmy od pętli <math>\mathbf{repeat}\, I \,\mathbf{until}\, b</math>. | Zacznijmy od pętli <math>\mathbf{repeat}\, I \,\mathbf{until}\, b</math>. | ||
Przyjrzyjmy się dwóm podejściom, które zastosowaliśmy dla pętli <math>\mathbf{while}\,</math> w poprzednim zadaniu. | Przyjrzyjmy się dwóm podejściom, które zastosowaliśmy dla pętli <math>\mathbf{while}\,</math> w poprzednim zadaniu. | ||
Po pierwsze rozwinięcie: | Po pierwsze, rozwinięcie: | ||
<math> | <math> | ||
| Linia 308: | Linia 307: | ||
</math> | </math> | ||
Teraz jest | Teraz jest już łatwo: | ||
<math> | <math> | ||
| Linia 357: | Linia 356: | ||
</math> | </math> | ||
Zauważmy, wartość zmiennej <math>x</math> po zakończeniu pętli wynosi albo <math>n_2</math> albo pozostaje niezmieniona, o ile nie była ona zmieniana wewnątrz instrukcji <math>I</math>. | Zauważmy, wartość zmiennej <math>x</math> po zakończeniu pętli wynosi albo <math>n_2</math>, albo pozostaje niezmieniona, o ile nie była ona zmieniana wewnątrz instrukcji <math>I</math>. | ||
Ponieważ nie zostało wyspecyfikowane jaka powinna być wartość tej zmiennej, możemy taką semantykę uznać za poprawną. | Ponieważ nie zostało wyspecyfikowane, jaka powinna być wartość tej zmiennej, możemy taką semantykę uznać za poprawną. | ||
'''Pytanie:''' oto inna wersja jednej z powyższych reguł: | '''Pytanie:''' oto inna wersja jednej z powyższych reguł: | ||
| Linia 407: | Linia 406: | ||
<div class="mw-collapsible mw-made=collapsible mw-collapsed"><div class="mw-collapsible-content" style="display:none"> | <div class="mw-collapsible mw-made=collapsible mw-collapsed"><div class="mw-collapsible-content" style="display:none"> | ||
Składnia wyrażeń pozwala na wygodny dostęp do najmniej | Składnia wyrażeń pozwala na wygodny dostęp do najmniej znaczącego bitu liczby. Spróbujmy zatem zastosować metodę dodawania pisemnego: | ||
<math> | <math> | ||
| Linia 452: | Linia 451: | ||
Zanim dopiszemy pozostałe reguły, określmy zbiór konfiguracji jako zbiór wyrażeń. Konfiguracje końcowe to wyrażenia bez operatora dodawania (liczby binarne). | Zanim dopiszemy pozostałe reguły, określmy zbiór konfiguracji jako zbiór wyrażeń. Konfiguracje końcowe to wyrażenia bez operatora dodawania (liczby binarne). | ||
Nasz pomysł jest taki, że tranzycje stopniowo przesuwają operator dodawania w lewo, aż się go ostatecznie | Nasz pomysł jest taki, że tranzycje stopniowo przesuwają operator dodawania w lewo, aż się go ostatecznie pozbędą. | ||
Gdy obydwa składniki mają tyle samo cyfr, do zakończenia dodawania potrzebujemy reguły: | Gdy obydwa składniki mają tyle samo cyfr, do zakończenia dodawania potrzebujemy reguły: | ||
| Linia 482: | Linia 481: | ||
</math> | </math> | ||
gdyż spowodowałaby ona możliwość | gdyż spowodowałaby ona możliwość "pętlenia się", a zatem braku wyniku obliczenia. | ||
Na koniec dodajemy typowe reguły opisujące jak krok podwyrażenia indukuje krok całego wyrażenia: | Na koniec dodajemy typowe reguły opisujące jak krok podwyrażenia indukuje krok całego wyrażenia: | ||
| Linia 507: | Linia 506: | ||
{{cwiczenie|4|cw4| | {{cwiczenie|4|cw4| | ||
Rozszerzmy składnię o jeden symbol <math>p</math> oznaczający | Rozszerzmy składnię o jeden symbol <math>p</math> oznaczający "przepełnienie": | ||
<math> | <math> | ||
| Linia 518: | Linia 517: | ||
</math> | </math> | ||
Na przykład <math>p 1 0 1</math> oznacza tę samą liczbę co <math>\epsilon 1 0 1</math>, ale z dodatkową informacją, że podczas jej obliczania nastąpiło | Na przykład <math>p 1 0 1</math> oznacza tę samą liczbę, co <math>\epsilon 1 0 1</math>, ale z dodatkową informacją, że podczas jej obliczania nastąpiło "przepełnienie". | ||
Rozumiemy przez to sytuację, gdy wynik ma więcej cyfr niż każdy z argumentów. | Rozumiemy przez to sytuację, gdy wynik ma więcej cyfr niż każdy z argumentów. | ||
Cyfry zero z lewej strony (najbardziej znaczące) również uważamy za pełnoprawne cyfry, nie należy ich usuwać ani dodawać nowych. | Cyfry zero z lewej strony (najbardziej znaczące) również uważamy za pełnoprawne cyfry, nie należy ich usuwać ani dodawać nowych. | ||
| Linia 547: | Linia 546: | ||
Zadanie dotyczy w zasadzie składni ograniczonej, ale jako konfiguracji pośrednich będziemy zapewne potrzebować wyrażeń wykraczających poza tę składnię, np. <math>(e_1 + e_2) 0</math>, podobnie jak w poprzednim zadaniu. | Zadanie dotyczy w zasadzie składni ograniczonej, ale jako konfiguracji pośrednich będziemy zapewne potrzebować wyrażeń wykraczających poza tę składnię, np. <math>(e_1 + e_2) 0</math>, podobnie jak w poprzednim zadaniu. | ||
Zatem mamy tu do czynienia z typowym zabiegiem rozszerzania składni na użytek semantyki operacyjnej (z tym | Zatem mamy tu do czynienia z typowym zabiegiem rozszerzania składni na użytek semantyki operacyjnej (z tym że rozszerzenie jest dane z góry i nie musimy go wymyślać :) | ||
Przyjmijmy, że konfiguracjami są dowolne wyrażenia, a konfiguracjami końcowymi wyrażenia bez operatora dodawania (ale teraz mogą to być np. wyrażenia postaci <math>p 1 0 0</math>). | Przyjmijmy, że konfiguracjami są dowolne wyrażenia, a konfiguracjami końcowymi wyrażenia bez operatora dodawania (ale teraz mogą to być np. wyrażenia postaci <math>p 1 0 0</math>). | ||
| Linia 588: | Linia 587: | ||
Ale co należy zrobić, gdy tylko jeden ze składników odnotował przepełnienie? <math>p + \epsilon \,\Longrightarrow\, ?</math> | Ale co należy zrobić, gdy tylko jeden ze składników odnotował przepełnienie? <math>p + \epsilon \,\Longrightarrow\, ?</math> | ||
Oczywiście, w tej sytuacji żadnego przepełnienia nie ma, ponieważ drugi składnik ma wystarczająco dużo cyfr by je przesłonić. | Oczywiście, w tej sytuacji żadnego przepełnienia nie ma, ponieważ drugi składnik ma wystarczająco dużo cyfr, by je przesłonić. | ||
Oto odpowiednie reguły: | Oto odpowiednie reguły: | ||
| Linia 598: | Linia 597: | ||
Na koniec zostało najważniejsze: kiedy powinniśmy generować sygnał o przepełnieniu? | Na koniec zostało najważniejsze: kiedy powinniśmy generować sygnał o przepełnieniu? | ||
Przypomnijmy sobie reguły dla | Przypomnijmy sobie reguły dla dodawania pisemnego w poprzednim zadaniu. | ||
Jeśli nie ma przeniesienia, to przepełnienie nie może powstać. | Jeśli nie ma przeniesienia, to przepełnienie nie może powstać. | ||
Natomiast jeśli jest przeniesienie, to stanowi ono ''potencjalne przepełnienie''. | Natomiast jeśli jest przeniesienie, to stanowi ono ''potencjalne przepełnienie''. | ||
| Linia 609: | Linia 608: | ||
Nowy sztuczny składnik <math>p 1</math> zawiera jakby na wszelki wypadek informacje o potencjalnym przepełnieniu. | Nowy sztuczny składnik <math>p 1</math> zawiera jakby na wszelki wypadek informacje o potencjalnym przepełnieniu. | ||
Jeśli którykolwiek z pozostałych składników <math>e_1</math> i <math>e_2</math> ma przynajmniej jedną cyfrę, | Jeśli którykolwiek z pozostałych składników <math>e_1</math> i <math>e_2</math> ma przynajmniej jedną cyfrę, | ||
to <math>p</math> zostanie usunięte. W przeciwnym wypadku symbol <math>p</math> i przetrwa i będzie poprawnie informował o sytuacji przepełnienia. | to <math>p</math> zostanie usunięte. W przeciwnym wypadku symbol <math>p</math> i przetrwa,i będzie poprawnie informował o sytuacji przepełnienia. | ||
</div></div> | </div></div> | ||
| Linia 620: | Linia 619: | ||
{{cwiczenie|1|cw1.dom| | {{cwiczenie|1|cw1.dom| | ||
Podaj przykład wyrażenia boolowskiego, które nie policzy się ani przy użyciu strategii lewo- ani prawostronnej, a policzy się przy strategii równoległej. | Podaj przykład wyrażenia boolowskiego, które nie policzy się ani przy użyciu strategii lewo-, ani prawostronnej, a policzy się przy strategii równoległej. | ||
}} | }} | ||
| Linia 626: | Linia 625: | ||
{{cwiczenie|2|cw2.dom| | {{cwiczenie|2|cw2.dom| | ||
Zmodyfikuj semantykę wyrażeń następująco: dla każdego podwyrażenia niedeterministycznie wybierana jest | Zmodyfikuj semantykę wyrażeń następująco: dla każdego podwyrażenia niedeterministycznie wybierana jest strategia lewo- albo prawostronna, ale niedozwolony jest "przeplot". | ||
}} | }} | ||
| Linia 644: | Linia 643: | ||
{{cwiczenie|5|cw15.dom| | {{cwiczenie|5|cw15.dom| | ||
Zaproponuj semantykę przypisania równoległego w języku | Zaproponuj semantykę przypisania równoległego w języku TINY: | ||
<math> | <math> | ||
| Linia 650: | Linia 649: | ||
</math> | </math> | ||
polegającego na obliczeniu najpierw wartości wyrażeń <math>e_1, \ldots, e_n</math> a następnie na podstawieniu tych wartości na zmienne <math>x_1, \ldots, x_n</math>. | polegającego na obliczeniu najpierw wartości wyrażeń <math>e_1, \ldots, e_n</math>, a następnie na podstawieniu tych wartości na zmienne <math>x_1, \ldots, x_n</math>. | ||
}} | }} | ||
Wersja z 10:39, 29 wrz 2006
Zawartość
Ćwiczymy dalej semantykę małych kroków. Uzupełnimy semantykę języka Tiny o semantykę operacyjną wyrażeń boolowskich i arytmetycznych. Następnie rozszerzymy nasz język o róznorodne konstrukcje iteracji. Na koniec zdefiniujemy operacje arytmetyczne liczb binarnych.
Rozszerzenia semantyki języka Tiny
Ćwiczenie 1
Semantyka języka Tiny z wykładu używała funkcji semantycznych dla określenia znaczenia wyrażeń boolowskich i arytmetycznych. Zdefiniuj znaczenie wyrażeń za pomocą semantyki operacyjnej, w stylu małych kroków.
Rozwiązanie
{{{3}}}
Ćwiczenie 2
Rozszerzmy język Tiny o następujące dobrze znane konstrukcje iteracji:
Napisz semantykę małych kroków dla powyższych konstrukcji.
Rozwiązanie
{{{3}}}
Kalkulator binarny
Ćwiczenie 3
Rozważmy następujący język wyrażeń (liczby binarne z dodawaniem):
oznacza słowo puste, czyli np. oznacza binarną liczbę 1011. Napisz semantykę operacyjną obliczającą wartość wyrażeń.
Rozwiązanie
{{{3}}}
Ćwiczenie 4
Rozszerzmy składnię o jeden symbol oznaczający "przepełnienie":
Na przykład oznacza tę samą liczbę, co , ale z dodatkową informacją, że podczas jej obliczania nastąpiło "przepełnienie". Rozumiemy przez to sytuację, gdy wynik ma więcej cyfr niż każdy z argumentów. Cyfry zero z lewej strony (najbardziej znaczące) również uważamy za pełnoprawne cyfry, nie należy ich usuwać ani dodawać nowych.
Napisz semantykę operacyjną obliczającą wartość wyrażenia wraz z informacja o ewentualnym przepełnieniu. Wynik powinien byc poprawny przynajmniej dla wyrażeń w składni ograniczonej:
reprezentujących sumę liczb binarnych.
Rozwiązanie
{{{3}}}
Zadania domowe
Ćwiczenie 1
Podaj przykład wyrażenia boolowskiego, które nie policzy się ani przy użyciu strategii lewo-, ani prawostronnej, a policzy się przy strategii równoległej.
Ćwiczenie 2
Zmodyfikuj semantykę wyrażeń następująco: dla każdego podwyrażenia niedeterministycznie wybierana jest strategia lewo- albo prawostronna, ale niedozwolony jest "przeplot".
Ćwiczenie 3
Rozważ inną semantykę pętli , w której wyrażenie jest obliczane na nowo przed każdą iteracją pętli.
Ćwiczenie 4
Dodaj do wyrażeń binarnych operację odejmowania.
Ćwiczenie 5
Zaproponuj semantykę przypisania równoległego w języku TINY:
polegającego na obliczeniu najpierw wartości wyrażeń , a następnie na podstawieniu tych wartości na zmienne .
