Semantyka i weryfikacja programów/Ćwiczenia 2: 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ść ==


Ćwiczymy dalej semantykę małych kroków.
== Zawarto¶æ ==
Uzupełnimy semantykę języka Tiny o semantykę operacyjną
 
wyrażeń boolowskich i arytmetycznych.
Æwiczymy dalej semantykê ma³ych kroków.
Następnie rozszerzymy nasz język o róznorodne konstrukcje iteracji.
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.
Na koniec zdefiniujemy operacje arytmetyczne liczb binarnych.




== Rozszerzenia semantyki języka Tiny ==
== Rozszerzenia semantyki jêzyka Tiny ==




{{cwiczenie|1|cw1|
{{cwiczenie|1|cw1|


Semantyka języka Tiny z wykładu używała funkcji semantycznych  
Semantyka jêzyka Tiny z wyk³adu u¿ywa³a funkcji semantycznych  
<math>
<math>
B, E : State \to State
B, E : State \to State
</math>
</math>
dla określenia znaczenia wyrażeń boolowskich i arytmetycznych.
dla okre¶lenia znaczenia wyra¿eñ boolowskich i arytmetycznych.
Zdefiniuj znaczenie wyrażeń za pomocą semantyki operacyjnej,
Zdefiniuj znaczenie wyra¿eñ za pomoc± semantyki operacyjnej,
w stylu małych kroków.
w stylu ma³ych kroków.
}}
}}


Linia 28: Linia 29:
<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">


Przypomnijmy składnię wyrażeń boolowskich i arytmetycznych:
Przypomnijmy sk³adniê wyra¿eñ boolowskich i arytmetycznych:


<math>
<math>
Linia 59: Linia 60:
</math>
</math>


Niech <math>\mathbf{BExp}</math>  oznacza zbiór wyrażeń boolowskich,
Niech <math>\mathbf{BExp}</math>  oznacza zbiór wyra¿eñ boolowskich,
<math>b \in \mathbf{BExp}</math>.
<math>b \in \mathbf{BExp}</math>.
Chcemy, aby tranzycje dla wyrażeń były postaci:
Chcemy, aby tranzycje dla wyra¿eñ by³y postaci:


<math>
<math>
Linia 67: Linia 68:
</math>
</math>


i podobnie dla wyrażeń boolowskich:
i podobnie dla wyra¿eñ boolowskich:


<math>
<math>
Linia 74: Linia 75:


gdzie <math>s \in \mathbf{State}</math>.
gdzie <math>s \in \mathbf{State}</math>.
Dodatkowo będziemy potrzebować również tranzycji postaci:
Dodatkowo bêdziemy potrzebowaæ równie¿ tranzycji postaci:


<math>
<math>
Linia 83: Linia 84:
b, s \,\Longrightarrow\, l
b, s \,\Longrightarrow\, l
</math>
</math>
gdzie <math>n \in</math> jest liczbą całkowitą,  
gdzie <math>n \in</math> jest liczb± ca³kowit±,  
<math>n \in \mathbf{Num}</math>, a <math>l \in \mathbf{Bool} = \{ \mathbf{true}, \mathbf{false} \}</math>.
<math>n \in \mathbf{Num}</math>, a <math>l \in \mathbf{Bool} = \{ \mathbf{true}, \mathbf{false} \}</math>.
Formalnie, zbiór konfiguracji dla semantyki całego języka Tiny to
Formalnie, zbiór konfiguracji dla semantyki ca³ego jêzyka Tiny to


<math>
<math>
Linia 92: Linia 93:
</math>
</math>


a konfiguracje końcowe to <math>\mathbf{State}</math>; aczkolwiek
a konfiguracje koñcowe to <math>\mathbf{State}</math>; aczkolwiek
konfiguracje ze zbioru <math>\mathbf{Num} \, \cup \, \mathbf{Bool}</math> pełnią podobną rolę
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
dla wyra¿eñ arytmetycznych i boolowskich jako konfiguracje koñcowe dla
instrukcji.
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>.


Zacznijmy od (chyba najprostszych) tranzycji dla stałych boolowskich i liczbowych:
Zacznijmy od (chyba najprostszych) tranzycji dla sta³ych boolowskich i liczbowych:


<math>
<math>
Linia 106: Linia 107:
</math>
</math>


Podobnie jak poprzednio, zakładamy tutaj dla wygody, że
Podobnie jak poprzednio, zak³adamy tutaj dla wygody, ¿e
<math>\mathbf{Num} \subseteq \mathbf{Exp}</math> oraz <math>\mathbf{Bool} \subseteq \mathbf{BExp}</math>.
<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
Pozwala nam to nie odró¿niaæ sta³ych wystêpuj±cych w wyra¿eniach
a zatem pojawiających się po lewej stonie tranzycji
a zatem pojawiaj±cych siê po lewej stonie tranzycji
od wartości im odpowiadających pojawiających się po prawej stronie.
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>.
Ponieważ opisujemy teraz pojedyncze (małe) kroki składające się na
Poniewa¿ opisujemy teraz pojedyncze (ma³e) kroki sk³adaj±ce siê na
wykonanie programu, musimy podać w jakiej kolejności będą się
wykonanie programu, musimy podaæ w jakiej kolejno¶ci bêd± siê
obliczać <math>b_1</math> i <math>b_2</math>. Zacznijmy od strategii lewostronnej:
obliczaæ <math>b_1</math> i <math>b_2</math>. Zacznijmy od strategii lewostronnej:


<math>
<math>
Linia 128: Linia 129:
</math>
</math>


Możemy zaniechać obliczania
Mo¿emy zaniechaæ obliczania
<math>b_2</math> jeśli <math>b_1</math> oblicza się do false.
<math>b_2</math> je¶li <math>b_1</math> oblicza siê do false.
Oto odpowiednio zmodyfikowane reguły:
Oto odpowiednio zmodyfikowane regu³y:


<math>
<math>
Linia 141: Linia 142:
</math>
</math>


Analogicznie reguły prawostronne to:
Analogicznie regu³y prawostronne to:


<math>
<math>
Linia 152: Linia 153:
</math>
</math>


Reguły ''równoległe'' otrzymujemy jako sumę reguł lewo- i
Regu³y ''równoleg³e'' otrzymujemy jako sumê regu³ lewo- i
prawostronnych (w sumie 6 reguł). Zauważmy, że obliczanie
prawostronnych (w sumie 6 regu³). Zauwa¿my, ¿e obliczanie
wyrażeń <math>b_1</math> i <math>b_2</math> odbywa się teraz
wyra¿eñ <math>b_1</math> i <math>b_2</math> odbywa siê teraz
w twz. \''przeplocie": Pojedynczy krok polega na wykonaniu
w twz. \''przeplocie": Pojedynczy krok polega na wykonaniu
jednego kroku obliczenia <math>b_1</math> albo jednego kroku
jednego kroku obliczenia <math>b_1</math> albo jednego kroku
obliczenia <math>b_2</math>.
obliczenia <math>b_2</math>.
Zwróćmy też uwagę, że nasze tranzycje nie posiadają teraz
Zwróæmy te¿ uwagê, ¿e nasze tranzycje nie posiadaj± teraz
własności ''determinizmu'': wyrażenie <math>b_1 \land b_2</math>
w³asno¶ci ''determinizmu'': wyra¿enie <math>b_1 \land b_2</math>
może wyewoluować w pojedyńczym kroku albo do
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>.
<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
Na szczê¶cie, koñcowy wynik, do jakiego oblicza siê wyra¿enie
jest zawsze taki sam, niezależnie od przeplotu.
jest zawsze taki sam, niezale¿nie od przeplotu.


Oto reguły dla negacji:
Oto regu³y dla negacji:


<math>
<math>
Linia 176: Linia 177:
</math>
</math>


Reguły dla <math>e_1 \leq e_2</math> są następujące:
Regu³y dla <math>e_1 \leq e_2</math> s± nastêpuj±ce:


<math>
<math>
Linia 192: Linia 193:
</math>
</math>


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
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>.
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.
Najpierw obliczamy wyrażenie po prawej stronie przypisania,
Najpierw obliczamy wyra¿enie po prawej stronie przypisania,
a gdy wyrażenie to wyewoluuje do stałej (obliczy się), modyfikujemy
a gdy wyra¿enie to wyewoluuje do sta³ej (obliczy siê), modyfikujemy
stan:
stan:


Linia 208: Linia 209:
</math>
</math>


Rozważmy teraz instrukcję warunkową i instrukcję pętli.
Rozwa¿my teraz instrukcjê warunkow± i instrukcjê pêtli.
Najpierw obliczamy wartość dozoru:
Najpierw obliczamy warto¶æ dozoru:


<math>
<math>
Linia 220: Linia 221:
</math>
</math>


a gdy dozór jest już obliczony, podejmujemy decyzję.
a gdy dozór jest ju¿ obliczony, podejmujemy decyzjê.
W przypadku instrukcji warunkowej reguły są oczywiste:
W przypadku instrukcji warunkowej regu³y s± oczywiste:


<math>
<math>
Linia 229: Linia 230:
</math>
</math>


Gorzej jest w przypadku instrukcji pętli. Reguła mogłaby wyglądać tak:
Gorzej jest w przypadku instrukcji pêtli. Regu³a mog³aby wygl±daæ tak:


<math>
<math>
Linia 236: Linia 237:
</math>
</math>


ale nie wiemy już, jaki był dozór pętli (widzimy tylko wynik
ale nie wiemy ju¿, jaki by³ dozór pêtli (widzimy tylko wynik
obliczenia tego dozoru w stanie s, czyli <math>\mathbf{true}</math>).
obliczenia tego dozoru w stanie s, czyli <math>\mathbf{true}</math>).
Możemy odwołać się do tranzytywnego domknięcia relacji
Mo¿emy odwo³aæ siê do tranzytywnego domkniêcia relacji
<math>\,\Longrightarrow\,</math> (czyli w zadadzie do semantyki dużych kroków):
<math>\,\Longrightarrow\,</math> (czyli w zadadzie do semantyki du¿ych kroków):


<math>
<math>
Linia 250: Linia 251:
</math>
</math>


Takie rozwiązanie nie jest zatem ''czystą'' semantyką
Takie rozwi±zanie nie jest zatem ''czyst±'' semantyk±
małych kroków.
ma³ych kroków.
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 ''rozwinąc'' pętlę
Jedno z nich oparte jest na pomy¶le, aby ''rozwin±c'' pêtlê
<math>\mathbf{while}\,</math>, zanim obliczymy wartość dozoru <math>b</math>.
<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:


<math>
<math>
Linia 261: Linia 262:
</math>
</math>


Dzięki temu obliczany warunek logiczny <math>b</math> jest zawsze  
Dziêki temu obliczany warunek logiczny <math>b</math> jest zawsze  
''jednorazowy''.
''jednorazowy''.
Znalezienie innych rozwiązań, np. opartych na rozszerzeniu składni,
Znalezienie innych rozwi±zañ, np. opartych na rozszerzeniu sk³adni,
pozostawiamy dociekliwemu Czytelnikowi.
pozostawiamy dociekliwemu Czytelnikowi.


Reguły dla operacji arytmetycznych również pozostawiamy do napisania Czytelnikowi.
Regu³y dla operacji arytmetycznych równie¿ pozostawiamy do napisania Czytelnikowi.


</div></div>
</div></div>
Linia 274: Linia 275:
{{cwiczenie|2|cw2|
{{cwiczenie|2|cw2|


Rozszerzmy język Tiny o następujące dobrze znane konstrukcje iteracji:
Rozszerzmy jêzyk Tiny o nastêpuj±ce dobrze znane konstrukcje iteracji:


<math>
<math>
Linia 284: Linia 285:
</math>
</math>


Napisz semantykę małych kroków dla powyższych konstrukcji.
Napisz semantykê ma³ych kroków dla powy¿szych konstrukcji.
}}
}}


Linia 295: Linia 296:
<br>
<br>


 
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
Przyjrzyjmy się dwóm podejściom, które zastosowaliśmy dla
pêtli <math>\mathbf{while}\,</math> w poprzednim zadaniu.
pętli <math>\mathbf{while}\,</math> w poprzednim zadaniu.
Po pierwsze rozwiniêcie:
Po pierwsze rozwinięcie:


<math>
<math>
Linia 305: Linia 305:
</math>
</math>


Po drugie, spróbujmy odwołać się do <math>\,\Longrightarrow\,^{*}</math> dla dozoru pętli <math>b</math>:
Po drugie, spróbujmy odwo³aæ siê do <math>\,\Longrightarrow\,^{*}</math> dla dozoru pêtli <math>b</math>:


<math>
<math>
Linia 320: Linia 320:
</math>
</math>


Okazuje się, że jest jeszcze gorzej niż w przypadku pętli <math>\mathbf{while}\,</math>:
Okazuje siê, ¿e jest jeszcze gorzej ni¿ w przypadku pêtli <math>\mathbf{while}\,</math>:
nie pamiętamy już, jaka była instrukcja wewnętrzna naszej pętli!
nie pamiêtamy ju¿, jaka by³a instrukcja wewnêtrzna naszej pêtli!
Czyli takie podejście jest teraz nieskuteczne.
Czyli takie podej¶cie jest teraz nieskuteczne.




Linia 329: Linia 329:
<br>
<br>


 
Pêtla <math>\,\mathbf{do}\, e \,\mathbf{times}\, I</math>, w stanie <math>s</math>, oznacza wykonianie instrukcji <math>I</math>
Pętla <math>\,\mathbf{do}\, e \,\mathbf{times}\, I</math>, w stanie <math>s</math>, oznacza wykonianie instrukcji <math>I</math>
<math>n</math> razy, gdzie <math>n</math> to warto¶æ, do której oblicza siê
<math>n</math> razy, gdzie <math>n</math> to wartość, do której oblicza się
<math>e</math> w stanie <math>s</math>.
<math>e</math> w stanie <math>s</math>.
Czyli najpierw obliczmy <math>e</math> przy pomocy reguły:
Czyli najpierw obliczmy <math>e</math> przy pomocy regu³y:


<math>
<math>
Linia 346: Linia 345:
</math>
</math>


Teraz jest juz łatwo:
Teraz jest juz ³atwo:


<math>
<math>
Linia 363: Linia 362:
<br>
<br>


 
W przypadku pêtli <math>\mathbf{for}\,</math> przyjmijmy, ¿e warto¶ci wyra¿eñ
W przypadku pętli <math>\mathbf{for}\,</math> przyjmijmy, że wartości wyrażeń
<math>e_1</math> i <math>e_2</math> obliczane s± przed pierwsz± iteracj±
<math>e_1</math> i <math>e_2</math> obliczane są przed pierwszą iteracją
pêtli.  
pętli.  
Dodatkowo ustalmy, ¿e <math>e_1</math> bêdzie obliczone jako pierwsze.
Dodatkowo ustalmy, że <math>e_1</math> będzie obliczone jako pierwsze.
Czyli:
Czyli:


Linia 380: Linia 378:
</math>
</math>


Zatem zakres zmiennej <math>x</math> mamy już obliczony, tzn. jesteśmy
Zatem zakres zmiennej <math>x</math> mamy ju¿ obliczony, tzn. jeste¶my
w konfiguracji
w konfiguracji


Linia 387: Linia 385:
</math>
</math>


Dalsze reguły mogą być podobne do reguł dla pętli <math>\,\mathbf{do}\, n \,\mathbf{times}\, I</math>:
Dalsze regu³y mog± byæ podobne do regu³ dla pêtli <math>\,\mathbf{do}\, n \,\mathbf{times}\, I</math>:


<math>
<math>
Linia 400: Linia 398:




Zauważmy, wartość zmiennej <math>x</math> po zakończeniu pętli
Zauwa¿my, warto¶æ zmiennej <math>x</math> po zakoñczeniu pêtli
wynosi albo <math>n_2</math> albo pozostaje niezmieniona.  
wynosi albo <math>n_2</math> albo pozostaje niezmieniona.  
Ponieważ nie zostało wyspecyfikowane jaka
Poniewa¿ nie zosta³o wyspecyfikowane jaka
powinna być wartość tej zmiennej, możemy taką semantykę uznać
powinna byæ warto¶æ tej zmiennej, mo¿emy tak± semantykê uznaæ
za poprawną.
za poprawn±.


'''Pytanie:'''
'''Pytanie:'''
A gdybyśmy jednak zażądali przywrócenia na koniec wartości zmiennej <math>x</math>  
A gdyby¶my jednak za¿±dali przywrócenia na koniec warto¶ci zmiennej <math>x</math>  
sprzed pętli?
sprzed pêtli?
Jak należałoby zmienić nasze reguły?
Jak nale¿a³oby zmieniæ nasze regu³y?




Semantykę dla <math>\,\mathbf{do}\, I \, \mathbf{while}\, b</math> pozostawiamy Czytelnikowi jako
Semantykê dla <math>\,\mathbf{do}\, I \, \mathbf{while}\, b</math> pozostawiamy Czytelnikowi jako
proste ćwiczenie.
proste æwiczenie.
Oczywiście minimalistyczne rozwiązanie to
Oczywi¶cie minimalistyczne rozwi±zanie to


<math>
<math>
Linia 429: Linia 427:
{{cwiczenie|3|cw3|
{{cwiczenie|3|cw3|


Rozważmy następujący język wyrażeń (liczby binarne z dodawaniem):
Rozwa¿my nastêpuj±cy jêzyk wyra¿eñ (liczby binarne z dodawaniem):


<math>
<math>
Linia 439: Linia 437:
</math>
</math>


<math>\epsilon</math> oznacza słowo puste, czyli np. <math>\epsilon 1 0 1 1</math>
<math>\epsilon</math> oznacza s³owo puste, czyli np. <math>\epsilon 1 0 1 1</math>
oznacza binarną liczbę 1011.
oznacza binarn± liczbê 1011.
Napisz semantykę operacyjną obliczającą wartość wyrażeń.
Napisz semantykê operacyjn± obliczaj±c± warto¶æ wyra¿eñ.
}}
}}


Linia 449: Linia 447:
<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 znaczącego
Sk³adnia wyra¿eñ pozwala na wygodny dostêp do najmniej znacz±cego
bitu liczby. Spróbujmy zatem zastosować metodę dodawania  
bitu liczby. Spróbujmy zatem zastosowaæ metodê dodawania  
pisemnego:
pisemnego:


Linia 465: Linia 463:
</math>
</math>


Ale co zrobić z przeniesieniem?  
Ale co zrobiæ z przeniesieniem?  


<math>
<math>
Linia 471: Linia 469:
</math>
</math>


Podstawowy pomysł polega na potraktowaniu przeniesienia jak dodatkowego składnika:
Podstawowy pomys³ polega na potraktowaniu przeniesienia jak dodatkowego sk³adnika:


<math>
<math>
Linia 477: Linia 475:
</math>
</math>


Zauważmy, że w składni dopuszcza się dowolne przeplatanie operatora dodawania
Zauwa¿my, ¿e w sk³adni dopuszcza siê dowolne przeplatanie operatora dodawania
i bitów <math>0, 1</math>. Tę dowolność wykorzystaliśmy właśnie w regułach
i bitów <math>0, 1</math>. Tê dowolno¶æ wykorzystali¶my w³a¶nie w regu³ach
powyżej. Gdyby nasz język ograniczyć tylko do składni
powy¿ej. Gdyby nasz jêzyk ograniczyæ tylko do sk³adni


<math>
<math>
Linia 494: Linia 492:
</math>
</math>


(nazwijmy ją ''składnią ograniczoną'') to powyższe reguły byłyby niepoprawne.
(nazwijmy j± ''sk³adni± ograniczon±'') to powy¿sze regu³y by³yby niepoprawne.


Zanim dopiszemy pozostałe reguły, określmy zbiór konfiguracji jako  
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
zbiór wyra¿eñ. Konfiguracje koñcowe to wyra¿enia bez operatora dodawania
(liczby binarne). Nasz pomysł jest taki, że tranzycje stopniowo przesuwają
(liczby binarne). Nasz pomys³ jest taki, ¿e tranzycje stopniowo przesuwaj±
operator dodawania w lewo, aż się go ostatecznie ''pozbędą''.
operator dodawania w lewo, a¿ siê go ostatecznie ''pozbêd±''.


Gdy obydwa składniki mają tyle samo cyfr, do zakończenia dodawania
Gdy obydwa sk³adniki maj± tyle samo cyfr, do zakoñczenia dodawania
potrzebujemy reguły:
potrzebujemy regu³y:


<math>
<math>
Linia 508: Linia 506:
</math>
</math>


Gdy jeden ze składników ma mniej cyfr niż drugi, potrzebujemy reguł:
Gdy jeden ze sk³adników ma mniej cyfr ni¿ drugi, potrzebujemy regu³:


<math>
<math>
Linia 524: Linia 522:
</math>
</math>


Niestety, nie możemy użyć reguły przemienności:
Niestety, nie mo¿emy u¿yæ regu³y przemienno¶ci:


<math>
<math>
Linia 530: Linia 528:
</math>
</math>


gdyż spowodowałaby ona możliwość ''pętlenia się'', a zatem braku wyniku obliczenia.
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
Na koniec dodajemy typowe regu³y opisuj±ce jak krok podwyra¿enia indukuje
krok całego wyrażenia:
krok ca³ego wyra¿enia:


<math>
<math>
Linia 556: Linia 554:
{{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'':
''przepe³nienie'':


<math>
<math>
Linia 568: Linia 566:
</math>
</math>


Na przykład <math>p 1 0 1</math> oznacza tę samą liczbę co <math>\epsilon 1 0 1
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
</math>, ale z dodatkow± informacj±, ¿e podczas jej obliczania nast±pi³o
''przepełnienie''.
''przepe³nienie''.
Rozumiemy przez to sytuację, gdy wynik ma więcej cyfr niż każdy z
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ż
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.
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ñ <math>e</math> w sk³adni
ograniczonej:
 
<math>
e \, ::= \,\,
      b  \,\,|\,\,
      e_1 + e_2
</math>


Napisz semantykę operacyjną obliczającą wyrażenie wraz z
<math>
informacja o ewentualnym przepełnieniu.
b \, ::= \,\,
Wynik powinien byc poprawny przynajmniej dla wyrażeń w składni
      \epsilon  \,\,|\,\,
ograniczonej.
      b 0  \,\,|\,\,
      b 1.
</math>
}}
}}


Linia 586: Linia 598:
<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">


Zadanie dotyczy w zasadzie składni ograniczonej, ale jako konfiguracji
Zadanie dotyczy w zasadzie sk³adni ograniczonej, ale jako konfiguracji
pośrednich będziemy zapewne potrzebować wyrażeń wykraczających poza
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  
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
zadaniu. Zatem mamy tu do czynienia z typowym zabiegiem rozszerzania
składni na użytek semantyki operacyjnej (z tym, że rozszerzenie jest
sk³adni na u¿ytek semantyki operacyjnej (z tym, ¿e rozszerzenie jest
dane z góry i nie musimy go wymyślać :)
dane z góry i nie musimy go wymy¶laæ :)


Przyjmijmy, że konfiguracjami są dowolne wyrażenia, a konfiguracjami
Przyjmijmy, ¿e konfiguracjami s± dowolne wyra¿enia, a konfiguracjami
końcowymi wyrażenia bez operatora dodawania (ale teraz mogą to być
koñcowymi wyra¿enia bez operatora dodawania (ale teraz mog± to byæ
np. wyrażenia postaci <math>p 1 0 0</math>).
np. wyra¿enia postaci <math>p 1 0 0</math>).
Spróbujmy pozostawić wszystkie reguły z poprzedniego zadania.
Spróbujmy pozostawiæ wszystkie regu³y z poprzedniego zadania.
Dodamy tylko kilka nowych reguł, odpowiedzialnych za przepełnienie.
Dodamy tylko kilka nowych regu³, odpowiedzialnych za przepe³nienie.


Zacznijmy od najprostszej sytuacji, gdy jeden ze składników ma mniej
Zacznijmy od najprostszej sytuacji, gdy jeden ze sk³adników ma mniej
cyfr, i to ten właśnie składnik odnotował przepełnienie:
cyfr, i to ten w³a¶nie sk³adnik odnotowa³ przepe³nienie:


<math>
<math>
Linia 612: Linia 624:
</math>
</math>


W takiej sytuacji oczywiście informacja o przepełnieniu zostaje
W takiej sytuacji oczywi¶cie informacja o przepe³nieniu zostaje
wymazana.
wymazana.
Jeśli przepełnienie zostało odnotowane w składniku o większej liczbie
Je¶li przepe³nienie zosta³o odnotowane w sk³adniku o wiêkszej liczbie
cyfr, to reguły
cyfr, to regu³y


<math>
<math>
Linia 627: Linia 639:
</math>
</math>


z poprzedniego zadania są wystarczające.
z poprzedniego zadania s± wystarczaj±ce.


Rozważmy teraz przypadek, gdy obydwa składniki mają tę samą liczbę
Rozwa¿my teraz przypadek, gdy obydwa sk³adniki maj± tê sam± liczbê
cyfr.
cyfr.
Jeśli obydwa odnotowały przepełnienie, to oczywiście informacja ta
Je¶li obydwa odnotowa³y przepe³nienie, to oczywi¶cie informacja ta
powinna zostać zachowana:
powinna zostaæ zachowana:


<math>
<math>
Linia 638: Linia 650:
</math>
</math>


Ale co należy zrobić, gdy tylko jeden ze składników odnotował
Ale co nale¿y zrobiæ, gdy tylko jeden ze sk³adników odnotowa³
przepełnienie? <math>p + \epsilon \,\Longrightarrow\, ?</math>
przepe³nienie? <math>p + \epsilon \,\Longrightarrow\, ?</math>
Oczywiście, w tej sytuacji żadnego przepełnienia nie ma, ponieważ
Oczywi¶cie, w tej sytuacji ¿adnego przepe³nienia nie ma, poniewa¿
drugi składnik ma wystarczająco dużo cyfr by je przesłonić.
drugi sk³adnik ma wystarczaj±co du¿o cyfr by je przes³oniæ.
Oto odpowiednie reguły:
Oto odpowiednie regu³y:


<math>
<math>
Linia 650: Linia 662:
</math>
</math>


Na koniec zostało najważniejsze: kiedy powinniśmy generować sygnał o
Na koniec zosta³o najwa¿niejsze: kiedy powinni¶my generowaæ sygna³ o
przepełnieniu?
przepe³nieniu?
Przypomnijmy sobie reguły dla dadawania pisemnego w poprzednim
Przypomnijmy sobie regu³y dla dadawania pisemnego w poprzednim
zadaniu.
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
Natomiast je¶li jest przeniesienie, to stanowi ono ''potencjalne
przepełnienie''.  
przepe³nienie''.  
Odpowiednia reguła to
Odpowiednia regu³a to


<math>
<math>
Linia 663: Linia 675:
</math>
</math>


Nowy sztuczny składnik <math>p 1</math> zawiera jakby na wszelki wypadek
Nowy sztuczny sk³adnik <math>p 1</math> zawiera jakby na wszelki wypadek
informacje o potencjalnym przepełnieniu.
informacje o potencjalnym przepe³nieniu.
Jeśli którykolwiek z pozostałych składników <math>e_1</math> i <math>e_2</math>  
Je¶li którykolwiek z pozosta³ych sk³adników <math>e_1</math> i <math>e_2</math>  
ma przynajmniej jedną cyfrę,
ma przynajmniej jedn± cyfrê,
to <math>p</math> zostanie usunięte. W przeciwnym wypadku symbol <math>p</math>  
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.
i przetrwa i bêdzie poprawnie informowa³ o sytuacji przepe³nienia.




Linia 678: Linia 690:




==== Zadanie 1 ====
{{cwiczenie|1|cw1.dom|


Podaj przykład wyrażenia boolowskiego, które nie policzy się
Podaj przyk³ad wyra¿enia boolowskiego, które nie policzy siê
ani przy użyciu strategii lewo- ani prawostronnej, a policzy się przy strategii
ani przy u¿yciu strategii lewo- ani prawostronnej, a policzy siê przy strategii
równoległej.
równoleg³ej.
}}




==== Zadanie 2 ====
{{cwiczenie|2|cw2.dom|


Zmodyfikuj semantykę wyrażeń następująco: dla każdego podwyrażenia niedeterministycznie
Zmodyfikuj semantykê wyra¿eñ nastêpuj±co: dla ka¿dego podwyra¿enia niedeterministycznie
wybierana jest albo strategia lewo- albo prawostronna, ale
wybierana jest albo strategia lewo- albo prawostronna, ale
niedozwolony jest ,,przeplot\''.
niedozwolony jest ,,przeplot".
}}




==== Zadanie 3 ====
{{cwiczenie|3|cw3.dom|


Rozważ inną semantykę pętli <math>\mathbf{for}\, x = e_1 \,\mathbf{to}\, e_2 \,\mathbf{do}\, I</math>,
Rozwa¿ inn± semantykê pêtli <math>\mathbf{for}\, x = e_1 \,\mathbf{to}\, e_2 \,\mathbf{do}\, I</math>,
w której wyrażenie <math>e_2</math> jest obliczane na nowo
w której wyra¿enie <math>e_2</math> jest obliczane na nowo
przed każdą iteracją pętli.
przed ka¿d± iteracj± pêtli.
Napisz reguły semantyczne dla tej instrukcji, nie odwołując
Napisz regu³y semantyczne dla tej instrukcji, nie odwo³uj±c
się do innych istrukcji pętli.
siê do innych istrukcji pêtli.
}}




==== Zadanie 4 ====
{{cwiczenie|4|cw4.dom|


Dodaj do wyrażeń binarnych operację odejmowania.
Dodaj do wyra¿eñ binarnych operacjê odejmowania.
}}




{{cwiczenie|5|cw15.dom|


==== Zadanie 5 ====
Zaproponuj semantykê przypisania równoleg³ego w jêzyku Tiny:
 
Zaproponuj semantykę przypisania równoległego


<math>
<math>
Linia 715: Linia 730:
</math>
</math>


polegającego na obliczeniu najpierw wartości wyrażeń
polegaj±cego na obliczeniu najpierw warto¶ci wyra¿eñ
<math>e_1, \ldots, e_n</math> a następnie na podstawieniu
<math>e_1, \ldots, e_n</math> a nastêpnie na podstawieniu
nowych wartości na zmienne <math>x_1, \ldots, x_n</math>.
tych warto¶ci na zmienne <math>x_1, \ldots, x_n</math>.
}}

Wersja z 07:58, 9 sie 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 B,E:State→State 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:

I::=𝐫𝐞𝐩𝐞𝐚𝐭I𝐮𝐧𝐭𝐢𝐥b|𝐟𝐨𝐫x:=e1𝐭𝐨e2𝐝𝐨I|𝐝𝐨e𝐭𝐢𝐦𝐞𝐬I|𝐝𝐨I𝐰𝐡𝐢𝐥𝐞b

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):

e::=ϵ|e0|e1|e1+e2

ϵ oznacza s³owo puste, czyli np. ϵ1011 oznacza binarn± liczbê 1011. Napisz semantykê operacyjn± obliczaj±c± warto¶æ wyra¿eñ.


Rozwiązanie

{{{3}}}


Ćwiczenie 4

Rozszerzmy sk³adniê o jeden symbol p oznaczaj±cy przepe³nienie:

e::=ϵ|p|e0|e1|e1+e2.

Na przyk³ad p101 oznacza tê sam± liczbê co ϵ101, 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ñ e w sk³adni ograniczonej:

e::=b|e1+e2

b::=ϵ|b0|b1.


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 albo strategia lewo- albo prawostronna, ale niedozwolony jest ,,przeplot".


Ćwiczenie 3

Rozwa¿ inn± semantykê pêtli 𝐟𝐨𝐫x=e1𝐭𝐨e2𝐝𝐨I, w której wyra¿enie e2 jest obliczane na nowo przed ka¿d± iteracj± pêtli. Napisz regu³y semantyczne dla tej instrukcji, nie odwo³uj±c siê do innych istrukcji pêtli.


Ćwiczenie 4

Dodaj do wyra¿eñ binarnych operacjê odejmowania.


Ćwiczenie 5

Zaproponuj semantykê przypisania równoleg³ego w jêzyku Tiny:

x1:=e1||…||xn:=en

polegaj±cego na obliczeniu najpierw warto¶ci wyra¿eñ e1,…,en a nastêpnie na podstawieniu tych warto¶ci na zmienne x1,…,xn.

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