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¶æ ==
== Zawartość ==


Æwiczymy dalej semantykê ma³ych kroków.
Ćwiczymy dalej semantykę małych kroków.
Uzupe³nimy semantykê jêzyka Tiny o semantykê operacyjn±
Uzupełnimy semantykę języka Tiny o semantykę operacyjną
wyra¿eñ boolowskich i arytmetycznych.
wyrażeń boolowskich i arytmetycznych.
Nastêpnie rozszerzymy nasz jêzyk o róznorodne konstrukcje iteracji.
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 29: 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 60: 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 68: Linia 68:
</math>
</math>


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


<math>
<math>
Linia 75: 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 84: 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 93: 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 107: 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 129: 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 142: Linia 142:
</math>
</math>


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


<math>
<math>
Linia 153: 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 177: 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 193: 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 209: 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 221: 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 230: 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 237: 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 251: 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 262: 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 275: 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 285: 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 296: 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 345: Linia 345:
</math>
</math>


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


<math>
<math>
Linia 362: 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 378: 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 385: 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 398: 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 427: 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 437: 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 447: 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 463: Linia 463:
</math>
</math>


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


<math>
<math>
Linia 469: 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 475: 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 492: 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 506: 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 522: 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 528: 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 554: 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 566: 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æ
uważamy za pełnoprawne cyfry, nie należy ich usuwać ani dodawać
nowych.
nowych.


Napisz semantykê operacyjn± obliczaj±c± warto¶æ wyra¿enia wraz z
Napisz semantykę operacyjną obliczającą wartość wyrażenia wraz z
informacja o ewentualnym przepe³nieniu.
informacja o ewentualnym przepełnieniu.
Wynik powinien byc poprawny przynajmniej dla wyra¿eñ <math>e</math> w sk³adni
Wynik powinien byc poprawny przynajmniej dla wyrażeń <math>e</math> w składni
ograniczonej:
ograniczonej:


Linia 598: 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 624: 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 639: 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 650: 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 662: 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 675: 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 692: Linia 692:
{{cwiczenie|1|cw1.dom|
{{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.
}}
}}


Linia 700: Linia 700:
{{cwiczenie|2|cw2.dom|
{{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".
Linia 708: Linia 708:
{{cwiczenie|3|cw3.dom|
{{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.
}}
}}


Linia 718: Linia 718:
{{cwiczenie|4|cw4.dom|
{{cwiczenie|4|cw4.dom|


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


Linia 724: Linia 724:
{{cwiczenie|5|cw15.dom|
{{cwiczenie|5|cw15.dom|


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


<math>
<math>
Linia 730: 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
tych 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 08:04, 10 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=12803”