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


Tematem tych zajęć jest semantyka operacyjna wyrażeń (małe kroki).
== Zawarto¶æ ==


Tematem tych zajêæ jest semantyka operacyjna wyra¿eñ (ma³e kroki).


== Zadania z rozwiązaniami ==


== Semantyka operacyjna wyra¿eñ ==




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


Rozważmy bardzo prosty język wyrażeń, którego składnia opisana jest
Rozwa¿my bardzo prosty jêzyk wyra¿eñ, którego sk³adnia opisana jest
następującą gramatyką:
nastêpuj±c± gramatyk±:


<math>
<math>
Linia 30: Linia 30:
</math>
</math>


Wynikiem wyrażenienia warunkowego <math>\mathbf{if}\, e_1 \,\mathbf{then}\, e_2 \,\mathbf{else}\, e_3</math>
Wynikiem wyra¿enienia warunkowego <math>\mathbf{if}\, e_1 \,\mathbf{then}\, e_2 \,\mathbf{else}\, e_3</math>
jest wartość wyrażenia <math>e_2</math>, o ile wyrażenie
jest warto¶æ wyra¿enia <math>e_2</math>, o ile wyra¿enie
<math>e_1</math> oblicza się do wartości różnej od zera; w przeciwnym
<math>e_1</math> oblicza siê do warto¶ci ró¿nej od zera; w przeciwnym
przypadku wynikiem jest wartość wyrażenia <math>e_3</math>.
przypadku wynikiem jest warto¶æ wyra¿enia <math>e_3</math>.


Zaproponuj semantykę operacyjną (małe kroki) dla tego języka.
Zaproponuj semantykê operacyjn± (ma³e kroki) dla tego jêzyka.
}}
}}


Linia 44: Linia 44:


Zacznijmy od ustalenia notacji i dziedzin syntaktycznych.
Zacznijmy od ustalenia notacji i dziedzin syntaktycznych.
Niech <math>\mathbf{Num}</math> oznacza zbiór stałych liczbowych,  
Niech <math>\mathbf{Num}</math> oznacza zbiór sta³ych liczbowych,  
<math>n \in \mathbf{Num} = \{ 0, 1, \ldots \}</math>.
<math>n \in \mathbf{Num} = \{ 0, 1, \ldots \}</math>.
Podobnie, niech <math>\mathbf{Var}</math> oznacza zbiór identyfikatorów, które
Podobnie, niech <math>\mathbf{Var}</math> oznacza zbiór identyfikatorów, które
mogą być nazwami zmiennych; <math>x \in \mathbf{Var}</math>.
mog± byæ nazwami zmiennych; <math>x \in \mathbf{Var}</math>.
Wreszcie, niech <math>\mathbf{Exp}</math> oznacza zbiór wyrażeń;
Wreszcie, niech <math>\mathbf{Exp}</math> oznacza zbiór wyra¿eñ;
<math>e \in \mathbf{Exp}</math>.
<math>e \in \mathbf{Exp}</math>.
Dla ułatwienia zapisywania reguł zakładamy, ze stałe
Dla u³atwienia zapisywania regu³ zak³adamy, ze sta³e
liczbowe są wyrażeniami, czyli <math>\mathbf{Num} \subseteq \mathbf{Exp}</math>.
liczbowe s± wyra¿eniami, czyli <math>\mathbf{Num} \subseteq \mathbf{Exp}</math>.


Będziemy potrzebować zbioru ''stanów'', opisujących wartości
Bêdziemy potrzebowaæ zbioru ''stanów'', opisuj±cych warto¶ci
przypisane zmiennym.
przypisane zmiennym.
Najprostszym rozwiązaniem jest przyjąc, że stan to funkcja
Najprostszym rozwi±zaniem jest przyj±c, ¿e stan to funkcja
z <math>\mathbf{Var}</math> do <math>\mathbf{Num}</math>.
z <math>\mathbf{Var}</math> do <math>\mathbf{Num}</math>.
Oznaczmy przez <math>\mathbf{State}</math> zbiór wszystkich takich funkcji;
Oznaczmy przez <math>\mathbf{State}</math> zbiór wszystkich takich funkcji;
stany oznaczac będziemy przez <math>s, s_1, s', \ldots \in \mathbf{State}</math>.
stany oznaczac bêdziemy przez <math>s, s_1, s', \ldots \in \mathbf{State}</math>.


W naszej semantyce będziemy potrzebowac tranzycji dwóch postaci.
W naszej semantyce bêdziemy potrzebowac tranzycji dwóch postaci.
Po pierwsze, tranzycje postaci
Po pierwsze, tranzycje postaci


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


oznaczające mały krok w trakcie obliczania wyrażenia <math>e</math>
oznaczaj±ce ma³y krok w trakcie obliczania wyra¿enia <math>e</math>
w stanie <math>s</math>, w wyniku którego <math>e</math> wyewoluowało do
w stanie <math>s</math>, w wyniku którego <math>e</math> wyewoluowa³o do
<math>e'</math>. Stan nie ulega zmiania podczas obliczania wyrażenia
<math>e'</math>. Stan nie ulega zmiania podczas obliczania wyra¿enia
(nie ma tzw. ''efektów ubocznych''),
(nie ma tzw. ''efektów ubocznych''),
więc to samo <math>s</math> figuruje po lewej i prawej stronie strzałki.
wiêc to samo <math>s</math> figuruje po lewej i prawej stronie strza³ki.


Po drugie, tranzycje postaci
Po drugie, tranzycje postaci
Linia 78: Linia 78:
</math>
</math>


będą oznaczaczać, że wyrażenie <math>e</math> jest już policzone,
bêd± oznaczaczaæ, ¿e wyra¿enie <math>e</math> jest ju¿ policzone,
a jego wartością jest <math>n</math>.
a jego warto¶ci± jest <math>n</math>.


Zatem przyjmijmy, że zbiór konfiguracji to
Zatem przyjmijmy, ¿e zbiór konfiguracji to


<math>
<math>
Linia 87: Linia 87:
</math>
</math>


a konfiguracje końcowe to <math>\mathbf{Num}</math>.
a konfiguracje koñcowe to <math>\mathbf{Num}</math>.


{{
{{
uwaga||uwaga1|
uwaga||uwaga1|
Tak naprawdę to druga postać tranzycji nie jest
Tak naprawdê to druga postaæ tranzycji nie jest
niezbędna, gdyż moglibyśmy umówić się, że konfiguracje końcowe
niezbêdna, gdy¿ mogliby¶my umówiæ siê, ¿e konfiguracje koñcowe
to <math>\mathbf{Num} \times \mathbf{State}</math>.
to <math>\mathbf{Num} \times \mathbf{State}</math>.
}}
}}


Najprostsze są tranzycje prowadzące do konfiguracji końcowej:
Najprostsze s± tranzycje prowadz±ce do konfiguracji koñcowej:


<math>
<math>
Linia 102: Linia 102:
</math>
</math>


Symbol <math>n</math> po lewej stronie to wyrażenie składające się
Symbol <math>n</math> po lewej stronie to wyra¿enie sk³adaj±ce siê
ze stałej liczbowej, podczas gdy <math>n</math> po prawej stronie reprezentuje liczbę
ze sta³ej liczbowej, podczas gdy <math>n</math> po prawej stronie reprezentuje liczbê
będącą wartością wyrażenia.
bêd±c± warto¶ci± wyra¿enia.


Zmienna oblicza się do swojej wartości w bieżącym stanie:   
Zmienna oblicza siê do swojej warto¶ci w bie¿±cym stanie:   


<math>
<math>
Linia 112: Linia 112:
</math>
</math>


Teraz zajmiemy się dodawaniem <math>e_1 + e_2</math>. Ponieważ semantyka jest w stylu małych
Teraz zajmiemy siê dodawaniem <math>e_1 + e_2</math>. Poniewa¿ semantyka jest w stylu ma³ych
kroków, musimy zdecydować się czy najpierw obliczyć pierwszy (lewy) składnik
kroków, musimy zdecydowaæ siê czy najpierw obliczyæ pierwszy (lewy) sk³adnik
<math>e_1</math> czy drugi?
<math>e_1</math> czy drugi?
Jeśli wybierzemy lewy (strategia ''lewostronna''), otrzymamy regułę:
Je¶li wybierzemy lewy (strategia ''lewostronna''), otrzymamy regu³ê:


<math>
<math>
Linia 123: Linia 123:
</math>
</math>


Reguły tej postaci będziemy zapisywać tak:
Regu³y tej postaci bêdziemy zapisywaæ tak:


<math>
<math>
Linia 130: Linia 130:
</math>
</math>


Czyli mały krok w <math>e_1</math> stanowi też mały krok w <math>e_1 + e_2</math>.
Czyli ma³y krok w <math>e_1</math> stanowi te¿ ma³y krok w <math>e_1 + e_2</math>.
Po zakończeniu obliczania <math>e_1</math> przechodzimy do <math>e_2</math>:
Po zakoñczeniu obliczania <math>e_1</math> przechodzimy do <math>e_2</math>:


<math>
<math>
Linia 138: Linia 138:
</math>
</math>


A na końcu dodajemy:
A na koñcu dodajemy:


<math>
<math>
Linia 144: Linia 144:
</math>
</math>


Zwróćmy tutaj uwagę na pewną subtelność, dotyczącą dwóch wystąpień
Zwróæmy tutaj uwagê na pewn± subtelno¶æ, dotycz±c± dwóch wyst±pieñ
symbolu <math>+</math>: pierwsze wystąpienie oznacza jedną z konstrukcji składniowych
symbolu <math>+</math>: pierwsze wyst±pienie oznacza jedn± z konstrukcji sk³adniowych
języka, a drugie oznacza operację dodawania w zbiorze <math>\mathbf{Num}</math>.
jêzyka, a drugie oznacza operacjê dodawania w zbiorze <math>\mathbf{Num}</math>.
Pozwalamy sobie na taką kolizję oznaczeń, gdyż nie powinna ona
Pozwalamy sobie na tak± kolizjê oznaczeñ, gdy¿ nie powinna ona
prowadzić do niejednoznaczności. Pamiętajmy, że składnia języka jest
prowadziæ do niejednoznaczno¶ci. Pamiêtajmy, ¿e sk³adnia jêzyka jest
składnią abstrakcyjną, więc zamiast <math>e_1 + e_2</math> moglibyśmy równie
sk³adni± abstrakcyjn±, wiêc zamiast <math>e_1 + e_2</math> mogliby¶my równie
dobrze pisać np. <math>{\mathrm{add}}(e_1, e_2)</math> a wtedy reguła
dobrze pisaæ np. <math>{\mathrm{add}}(e_1, e_2)</math> a wtedy regu³a
wyglądałaby tak:
wygl±da³aby tak:


<math>
<math>
Linia 157: Linia 157:
</math>
</math>


Inną możliwą strategią obliczania <math>e_1 + e_2</math> jest strategia
Inn± mo¿liw± strategi± obliczania <math>e_1 + e_2</math> jest strategia
''prawostronna'', którą otrzymujemy zastępując pierwsze dwie z trzech
''prawostronna'', któr± otrzymujemy zastêpuj±c pierwsze dwie z trzech
powyższych reguł przez:
powy¿szych regu³ przez:


<math>
<math>
Linia 169: Linia 169:
</math>
</math>


Ponadto, jeśli przyjmiemy regułę pierwszą (dla <math>e_1</math>), trzecią
Ponadto, je¶li przyjmiemy regu³ê pierwsz± (dla <math>e_1</math>), trzeci±
i czwartą (dla <math>e_2</math>), otrzymamy strategię
i czwart± (dla <math>e_2</math>), otrzymamy strategiê
''równoległą'', polegającą na obliczaniu jednocześnie <math>e_1</math> i
''równoleg³±'', polegaj±c± na obliczaniu jednocze¶nie <math>e_1</math> i
<math>e_2</math>:
<math>e_2</math>:


Linia 184: Linia 184:
</math>
</math>


Bardziej precyzyjnie mówiąc, małe kroki obliczające
Bardziej precyzyjnie mówi±c, ma³e kroki obliczaj±ce
obydwa podwyrażenia przeplatają się, i to w dowolny sposób.
obydwa podwyra¿enia przeplataj± siê, i to w dowolny sposób.
Ta dowolność prowadzi do ''niedeterminizmu'', czyli do sytuacji, gdy
Ta dowolno¶æ prowadzi do ''niedeterminizmu'', czyli do sytuacji, gdy
kolejna (następna) konfiguracja nie jest wyznaczona jednoznacznie.
kolejna (nastêpna) konfiguracja nie jest wyznaczona jednoznacznie.
Jest tak, gdyż możemy mieć do wyboru dwie różne tranzycje
Jest tak, gdy¿ mo¿emy mieæ do wyboru dwie ró¿ne tranzycje


<math>
<math>
Linia 196: Linia 196:
</math>
</math>


Zauważmy natomiast, że kolejność przeplatania się małych kroków obliczających
Zauwa¿my natomiast, ¿e kolejno¶æ przeplatania siê ma³ych kroków obliczaj±cych
<math>e_1</math> i <math>e_2</math> nie wpływa w tym przypadku na końcową wartość
<math>e_1</math> i <math>e_2</math> nie wp³ywa w tym przypadku na koñcow± warto¶æ
całego wyrażenia.
ca³ego wyra¿enia.


Na koniec reguły dla wyrażenia warunkowego.
Na koniec regu³y dla wyra¿enia warunkowego.


<math>
<math>
Linia 221: Linia 221:
{{cwiczenie|2|cw2|
{{cwiczenie|2|cw2|


Rozszerzmy język wyrażeń z poprzedniego zadania o jedną konstrukcję
Rozszerzmy jêzyk wyra¿eñ z poprzedniego zadania o jedn± konstrukcjê


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


Wyrażenie <math>\mathbf{let}\, x = e_1 \,\mathbf{in}\, e_2</math> zawiera w sobie deklarację
Wyra¿enie <math>\mathbf{let}\, x = e_1 \,\mathbf{in}\, e_2</math> zawiera w sobie deklaracjê
<math>x = e_1</math>, która stanowi mechanizm wiązania
<math>x = e_1</math>, która stanowi mechanizm wi±zania
identyfikatorów w naszym języku.
identyfikatorów w naszym jêzyku.
Deklaracja <math>x = e_1</math> wprowadza nową zmienną <math>x</math>
Deklaracja <math>x = e_1</math> wprowadza now± zmienn± <math>x</math>
oraz przypisuje jej wartość.
oraz przypisuje jej warto¶æ.
Wartość wyrażenia <math>\mathbf{let}\, x = e_1 \,\mathbf{in}\, e_2</math> obliczamy następująco:
Warto¶æ wyra¿enia <math>\mathbf{let}\, x = e_1 \,\mathbf{in}\, e_2</math> obliczamy nastêpuj±co:
najpierw oblicza się wartość <math>e_1</math>, podstawia ją na zmienna
najpierw oblicza siê warto¶æ <math>e_1</math>, podstawia j± na zmienna
<math>x</math>, a następnie oblicza wyrażenie <math>e_2</math>.
<math>x</math>, a nastêpnie oblicza wyra¿enie <math>e_2</math>.
Zakresem zmiennej <math>x</math> jest wyrażenie <math>e_2</math>, czyli
Zakresem zmiennej <math>x</math> jest wyra¿enie <math>e_2</math>, czyli
wewnątrz <math>e_2</math> można odwoływać się (wielokrotnie) do zmiennej <math>x</math>;
wewn±trz <math>e_2</math> mo¿na odwo³ywaæ siê (wielokrotnie) do zmiennej <math>x</math>;
Ogólniej, odwołania do zmiennej w wyrażeniu odnoszą się do ''najbliższej''
Ogólniej, odwo³ania do zmiennej w wyra¿eniu odnosz± siê do ''najbli¿szej''
(najbardziej zagnieżdzonej) deklaracji tej zmiennej.
(najbardziej zagnie¿dzonej) deklaracji tej zmiennej.
Taki mechanizm wiązania identyfikatorów nazywamy ''wiązaniem
Taki mechanizm wi±zania identyfikatorów nazywamy ''wi±zaniem
statycznym''.
statycznym''.
Przyjmujemy zwykłe reguły przesłaniania zmiennych.
Przyjmujemy zwyk³e (statyczne) regu³y przes³aniania zmiennych, np.
Np., jeśli w <math>e_2</math> występuje podwyrażenie <math>\mathbf{let}\, x = \ldots \,\mathbf{in}\, e</math> to
je¶li w <math>e_2</math> wystêpuje podwyra¿enie <math>\mathbf{let}\, x = e \,\mathbf{in}\, e'</math> to
odwołania do <math>x</math> wewnątrz <math>e</math> odnoszą się do ''najbliższej''
deklaracja <math>x = e</math> ''przes³ania'' deklaracjê <math>x = e_1</math>
deklaracji zmiennej <math>x</math>.
w wyra¿eniu <math>e'</math>.


Zakładamy, że na początku wartości wszystkich zmiennych są
Zak³adamy, ¿e na pocz±tku warto¶ci wszystkich zmiennych s±
''nieokreślone'', czyli zmienne są niezainicjowane, a odwołanie do  
''nieokre¶lone'', czyli zmienne s± niezainicjowane, a odwo³anie do  
niezainicjowanej zmiennej jest uważane za niepoprawne.
niezainicjowanej zmiennej jest uwa¿ane za niepoprawne.
}}
}}


Linia 268: Linia 268:
<math>
<math>
\mathbf{let}\, z = 5 \,\mathbf{in}\, x+z
\mathbf{let}\, z = 5 \,\mathbf{in}\, x+z
\quad \quad \mapsto \quad \quad \mbox{brak wyniku; odwołanie do niezainicjowanej
\quad \quad \mapsto \quad \quad \mbox{brak wyniku; odwo³anie do niezainicjowanej
zmiennej}\, x
zmiennej}\, x
</math>
</math>
Linia 284: Linia 284:


Podobnie jak poprzednio,  
Podobnie jak poprzednio,  
stan powinien opisywać wartości przypisane zmiennym.
stan powinien opisywaæ warto¶ci przypisane zmiennym.
Tym razem jednak
Tym razem jednak
uwzględnimy niezainicjowane zmienne, czyli zmienne bez żadnej wartości.
uwzglêdnimy niezainicjowane zmienne, czyli zmienne bez ¿adnej warto¶ci.
Przyjmijmy zatem, że stan to skończona funkcja częściowa z <math>\mathbf{Var}</math> do <math>\mathbf{Num}</math>.
Przyjmijmy zatem, ¿e stan to skoñczona funkcja czê¶ciowa z <math>\mathbf{Var}</math> do <math>\mathbf{Num}</math>.
Oznaczmy symbolem <math>\mathbf{State}</math> zbiór wszystkich takich funkcji:
Oznaczmy symbolem <math>\mathbf{State}</math> zbiór wszystkich takich funkcji:
<math>
<math>
\mathbf{State} = \mathbf{Var} \to_{\mathrm{fin}} \mathbf{Num}
\mathbf{State} = \mathbf{Var} \to_{\mathrm{fin}} \mathbf{Num}
</math>.
</math>.
Naturalnym stanem początkowym jest stan ''pusty'', tzn.
Naturalnym stanem pocz±tkowym jest stan ''pusty'', tzn.
pusta funkcja częściowa, który będziemy oznaczać symbolem <math>\emptyset</math>.
pusta funkcja czê¶ciowa, który bêdziemy oznaczaæ symbolem <math>\emptyset</math>.
Wartość wyrażenia <math>e</math> w stanie początkowym wynosi <math>n</math>
Warto¶æ wyra¿enia <math>e</math> w stanie pocz±tkowym wynosi <math>n</math>
o ile zachodzi:
o ile zachodzi:


Linia 301: Linia 301:
</math>
</math>


Będziemy potrzebowac tranzycji dwóch postaci, podobnie jak poprzednio,
Bêdziemy potrzebowac tranzycji dwóch postaci, podobnie jak poprzednio,
ale pierwsza postać będzie trochę ogólniejsza:
ale pierwsza postaæ bêdzie trochê ogólniejsza:


<math>
<math>
Linia 308: Linia 308:
</math>
</math>


Tranzycja ta oznacza mały krok w trakcie obliczania wyrażenia <math>e</math>
Tranzycja ta oznacza ma³y krok w trakcie obliczania wyra¿enia <math>e</math>
w stanie <math>s</math>, w wyniku którego <math>e</math> wyewoluowało do
w stanie <math>s</math>, w wyniku którego <math>e</math> wyewoluowa³o do
<math>e'</math> a nowym stanem jest <math>s'</math>.
<math>e'</math> a nowym stanem jest <math>s'</math>.
Stan może się teraz zmienić na skutek deklaracji zmiennych.
Stan mo¿e siê teraz zmieniæ na skutek deklaracji zmiennych.


Spróbujmy rozszerzyc semantykę z poprzedniego zadania.
Spróbujmy rozszerzyc semantykê z poprzedniego zadania.
Ponieważ stan jest funkcją częściową, musimy zmienić niektóre reguły, np.
Poniewa¿ stan jest funkcj± czê¶ciow±, musimy zmieniæ niektóre regu³y, np.


<math>
<math>
x, s \,\Longrightarrow\, n, s \quad \mbox{ o ile } s(x) \mbox{ jest określone i } s(x) = n
x, s \,\Longrightarrow\, n, s \quad \mbox{ o ile } s(x) \mbox{ jest okre¶lone i } s(x) = n
</math>
</math>


Następnie dodajemy reguły dla wyrażenia
Nastêpnie dodajemy regu³y dla wyra¿enia
<math>\mathbf{let}\, x = e_1 \,\mathbf{in}\, e_2</math>.  
<math>\mathbf{let}\, x = e_1 \,\mathbf{in}\, e_2</math>.  
Gdy <math>e_1</math> jest już obliczne, wyatarczy reguła:
Gdy <math>e_1</math> jest ju¿ obliczne, wyatarczy regu³a:


<math>
<math>
Linia 329: Linia 329:


Notacja <math>s[x \mapsto n]</math> oznacza stan <math>s</math>, który zmodyfikowano
Notacja <math>s[x \mapsto n]</math> oznacza stan <math>s</math>, który zmodyfikowano
przypisując zmiennej <math>x</math> wartość <math>n</math>,
przypisuj±c zmiennej <math>x</math> warto¶æ <math>n</math>,
niezależnie od tego, czy <math>s(x)</math> było określone, czy nie,  
niezale¿nie od tego, czy <math>s(x)</math> by³o okre¶lone, czy nie,  
i pozostawiając niezmienione wartości dla pozostałych zmiennych.
i pozostawiaj±c niezmienione warto¶ci dla pozosta³ych zmiennych.
Formanie
Formanie


Linia 342: Linia 342:
</math>
</math>


W szczególności,
W szczególno¶ci,
dla <math>y \neq x</math>, <math>s[x \mapsto n](y)</math> jest określone wtedy i tylko
dla <math>y \neq x</math>, <math>s[x \mapsto n](y)</math> jest okre¶lone wtedy i tylko
wtedy, gdy <math>s(y)</math> jest określone.
wtedy, gdy <math>s(y)</math> jest okre¶lone.


Natomiast aby obliczyc <math>e_1</math> potrzebujemy reguły:
Natomiast aby obliczyc <math>e_1</math> potrzebujemy regu³y:


<math>
<math>
Linia 353: Linia 353:
</math>
</math>


Zwróćmy uwagę, że stan <math>s'</math> może być różny od <math>s</math>,
Zwróæmy uwagê, ¿e stan <math>s'</math> mo¿e byæ ró¿ny od <math>s</math>,
np. dlatego, że wewnątrz <math>e_1</math> znajduje się podwyrażenie
np. dlatego, ¿e wewn±trz <math>e_1</math> znajduje siê podwyra¿enie
<math>\mathbf{let}\, y = \ldots</math>.
<math>\mathbf{let}\, y = \ldots</math>.


'''Pytanie:''' czy taka semantyka jest poprawna?
'''Pytanie:''' czy taka semantyka jest poprawna?


Niestety nie, gdyż nie uwzględniamy ograniczonego zasięgu zmiennej.
Niestety nie, gdy¿ nie uwzglêdniamy ograniczonego zasiêgu zmiennej.
Rzućmy okiem na przykład:
Rzuæmy okiem na przyk³ad:


<math>
<math>
Linia 366: Linia 366:
</math>
</math>


Według naszych intencji to wyrażenie nie ma wartości, gdyż ostatnie
Wed³ug naszych intencji to wyra¿enie nie ma warto¶ci, gdy¿ ostatnie
odwołanie do <math>z</math> jest błędne.
odwo³anie do <math>z</math> jest b³êdne.
Natomiast według powyższych reguł mamy
Natomiast wed³ug powy¿szych regu³ mamy


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


Nasz błąd polega na tym, że po zakończeniu obliczania podwyrażenia
Nasz b³±d polega na tym, ¿e po zakoñczeniu obliczania podwyra¿enia
<math>\mathbf{let}\, z = 4 \,\mathbf{in}\, z+z+z</math> ''zapominamy'' przywrócić zmiennej <math>z</math>
<math>\mathbf{let}\, z = 4 \,\mathbf{in}\, z+z+z</math> ''zapominamy'' przywróciæ zmiennej <math>z</math>
poprzednią wartość (a właściwie brak wartości w przykładzie powyżej).
poprzedni± warto¶æ (a w³a¶ciwie brak warto¶ci w przyk³adzie powy¿ej).
Przedyskutujmy kilka wariantów.
Przedyskutujmy kilka wariantów.


Linia 388: Linia 388:
<br>
<br>


Wygodne i eleganckie rozwiązanie tego problemu jest możliwe, jeśli
Wygodne i eleganckie rozwi±zanie tego problemu jest mo¿liwe, je¶li
rozszerzymy składnię naszego języka.  
rozszerzymy sk³adniê naszego jêzyka.  
Intuicyjnie, reguła
Intuicyjnie, regu³a


<math>
<math>
Linia 396: Linia 396:
</math>
</math>


powinna zostać zastąpiona przez
powinna zostaæ zast±piona przez


<math>
<math>
\mathbf{let}\, x = n \,\mathbf{in}\, e_2, s \,\Longrightarrow\, e_2 \,\mathbf{then}\, \mbox{,,przywróć wartość zmiennej x''}, s[x \mapsto n].
\mathbf{let}\, x = n \,\mathbf{in}\, e_2, s \,\Longrightarrow\, e_2 \,\mathbf{then}\, \mbox{,,przywróæ warto¶æ zmiennej x''}, s[x \mapsto n].
</math>
</math>


czyli potrzebujemy konstrukcji składniowej, która polega na obliczeniu
czyli potrzebujemy konstrukcji sk³adniowej, która polega na obliczeniu
wyrażenia
wyra¿enia
<math>e_2</math> a następnie na przypisaniu zmiennej <math>x</math> danej wartości.
<math>e_2</math> a nastêpnie na przypisaniu zmiennej <math>x</math> danej warto¶ci.
Rozszerzmy zatem składnię następujaco:
Rozszerzmy zatem sk³adniê nastêpujaco:


<math>
<math>
Linia 413: Linia 413:
</math>
</math>


Wyrażenie <math>e \,\mathbf{then}\, x:= n</math> jest w pewnym sensie dualne
Wyra¿enie <math>e \,\mathbf{then}\, x:= n</math> jest w pewnym sensie dualne
do <math>\mathbf{let}\, x = n \,\mathbf{in}\, e</math>, gdyż jedyna (choc niewątpliwie istotna) różnica
do <math>\mathbf{let}\, x = n \,\mathbf{in}\, e</math>, gdy¿ jedyna (choc niew±tpliwie istotna) ró¿nica
między nimi to kolejność obliczenia <math>e</math> i przypisania wartości
miêdzy nimi to kolejno¶æ obliczenia <math>e</math> i przypisania warto¶ci
na zmienną <math>x</math>.  
na zmienn± <math>x</math>.  
Oto nowa reguła
Oto nowa regu³a


<math>
<math>
Linia 424: Linia 424:
</math>
</math>


Pewna trudność pojawia się w sytuacji, gdy <math>s(x)</math> jest
Pewna trudno¶æ pojawia siê w sytuacji, gdy <math>s(x)</math> jest
nieokreślone, czyli gdy zmienna <math>x</math> jest niezainicjowana -- reguła
nieokre¶lone, czyli gdy zmienna <math>x</math> jest niezainicjowana -- regu³a
powyższa nie obejmuje wogóle takiej sytuacji.
powy¿sza nie obejmuje wogóle takiej sytuacji.
Najprostszym sposobem rozwiązania tej trudności jest rozszerzenie
Najprostszym sposobem rozwi±zania tej trudno¶ci jest rozszerzenie
konstrukcji <math>e \,\mathbf{then}\, x := n</math>:
konstrukcji <math>e \,\mathbf{then}\, x := n</math>:


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


gdzie symbol <math>\bot</math> oznacza brak wartości.
gdzie symbol <math>\bot</math> oznacza brak warto¶ci.
Dodajemy również regułę:
Dodajemy równie¿ regu³ê:


<math>
<math>
\mathbf{let}\, x = n \,\mathbf{in}\, e_2, s \,\Longrightarrow\, e_2 \,\mathbf{then}\, x := \bot, s[x \mapsto n] \quad
\mathbf{let}\, x = n \,\mathbf{in}\, e_2, s \,\Longrightarrow\, e_2 \,\mathbf{then}\, x := \bot, s[x \mapsto n] \quad
\mbox{ o ile } s(x) \, \mbox{ jest nieokreślone}.
\mbox{ o ile } s(x) \, \mbox{ jest nieokre¶lone}.
</math>
</math>


Rozwiązanie to jest odrobinę nieeleganckie, gdyż prawie identyczne reguły
Rozwi±zanie to jest odrobinê nieeleganckie, gdy¿ prawie identyczne regu³y
musimy napisać dwukrotnie.
musimy napisaæ dwukrotnie.
Widać to np. w poniższych regułach, ''scalających'' semantykę dla <math>e \,\mathbf{then}\, x := n</math>
Widaæ to np. w poni¿szych regu³ach, ''scalaj±cych'' semantykê dla <math>e \,\mathbf{then}\, x := n</math>
z semantyką pozostałych wyrażeń:
z semantyk± pozosta³ych wyra¿eñ:


<math>
<math>
Linia 461: Linia 461:
<math>
<math>
n' \,\mathbf{then}\, x := \bot, s \,\Longrightarrow\, n', s' \quad \mbox{ o ile } s(x)  
n' \,\mathbf{then}\, x := \bot, s \,\Longrightarrow\, n', s' \quad \mbox{ o ile } s(x)  
\mbox{ jest określone i } s' = s \setminus \{ (x, s(x)) \}
\mbox{ jest okre¶lone i } s' = s \setminus \{ (x, s(x)) \}
</math>
</math>


Linia 469: Linia 469:
<br>
<br>


Zanim przejdziemy do kolejnego wariantu, zastanówmy się czy  
Zanim przejdziemy do kolejnego wariantu, zastanówmy siê czy  
istnieje inny sposób rozwiązania trudności związanej z <math>n =
istnieje inny sposób rozwi±zania trudno¶ci zwi±zanej z <math>n =
\bot</math>, który pozwalałby uniknąć wprowadzania dodatkowej konstrukcji
\bot</math>, który pozwala³by unikn±æ wprowadzania dodatkowej konstrukcji
<math>e \,\mathbf{then}\, x := \bot</math>.
<math>e \,\mathbf{then}\, x := \bot</math>.
Pomysł może polegać na rozszerzeniu
Pomys³ mo¿e polegaæ na rozszerzeniu
zbioru <math>\mathbf{Num}</math> o dodatkowy element <math>\bot</math>:
zbioru <math>\mathbf{Num}</math> o dodatkowy element <math>\bot</math>:


Linia 480: Linia 480:
</math>
</math>


Wtedy nie musimy pisać dwóch bardzo podobnych wariantów reguł.
Wtedy nie musimy pisaæ dwóch bardzo podobnych wariantów regu³.
Dodatkowo, w tym rozwiązaniu warto poczynić umowę, że
Dodatkowo, w tym rozwi±zaniu warto poczyniæ umowê, ¿e
<math>s(x) = \bot</math> reprezentuje brak wartości zmiennej <math>x</math>.
<math>s(x) = \bot</math> reprezentuje brak warto¶ci zmiennej <math>x</math>.
Wtedy stany są funkcjami całkowitymi z <math>\mathbf{Var}</math> w <math>\mathbf{Num}</math>
Wtedy stany s± funkcjami ca³kowitymi z <math>\mathbf{Var}</math> w <math>\mathbf{Num}</math>
przyjmującymi wartość różną od <math>\bot</math> tylko dla skończenie
przyjmuj±cymi warto¶æ ró¿n± od <math>\bot</math> tylko dla skoñczenie
wielu elementów.
wielu elementów.
Pewnym mankamentem jest to, że teraz
Pewnym mankamentem jest to, ¿e teraz
<math>n = \bot</math> może pojawiać sie w wyrażeniach podobnie jak stałe.
<math>n = \bot</math> mo¿e pojawiaæ sie w wyra¿eniach podobnie jak sta³e.
Tym niemniej nie musimy adaptować reguł dla stałych tak, aby radziły
Tym niemniej nie musimy adaptowaæ regu³ dla sta³ych tak, aby radzi³y
one sobie z <math>n = \bot</math>, ponieważ wyrażenia zawierające
one sobie z <math>n = \bot</math>, poniewa¿ wyra¿enia zawieraj±ce
<math>\bot</math> możemy również uważać za roszerzenie składni.
<math>\bot</math> mo¿emy równie¿ uwa¿aæ za roszerzenie sk³adni.


Jeśli jednak dopuścimy symbol <math>\bot</math> w wyrażeniach, to możemy
Je¶li jednak dopu¶cimy symbol <math>\bot</math> w wyra¿eniach, to mo¿emy
elegancko wybrnąć z sytuacji, rozszerzając operacje arytmetyczne
elegancko wybrn±æ z sytuacji, rozszerzaj±c operacje arytmetyczne
na zbiór <math>\mathbf{Num} \cup \{ \bot \}</math> tak, aby zachowywały one
na zbiór <math>\mathbf{Num} \cup \{ \bot \}</math> tak, aby zachowywa³y one
nieokreśloność:
nieokre¶lono¶æ:


<math>
<math>
Linia 501: Linia 501:
</math>
</math>


Trzeba jednak w takim razie zadbać o to, aby wyrażenie <math>\mathbf{let}\, x = e_1
Trzeba jednak w takim razie zadbaæ o to, aby wyra¿enie <math>\mathbf{let}\, x = e_1
\,\mathbf{in}\, e_2</math> obliczało się normalnie tylko wtedy, gdy wartość
\,\mathbf{in}\, e_2</math> oblicza³o siê normalnie tylko wtedy, gdy warto¶æ
wyrażenia <math>e_1</math> jest różna od <math>\bot</math>.
wyra¿enia <math>e_1</math> jest ró¿na od <math>\bot</math>.




Linia 510: Linia 510:
<br>
<br>


Zrewidujmy teraz podstawowe założenia, które dotychczas poczyniliśmy.
Zrewidujmy teraz podstawowe za³o¿enia, które dotychczas poczynili¶my.
Jednym z nich było przyjęcie ogólnej postaci tranzycji:
Jednym z nich by³o przyjêcie ogólnej postaci tranzycji:


<math>
<math>
Linia 517: Linia 517:
</math>
</math>


pozwalającej na zmianę stanu podczas obliczania wyrażenia.
pozwalaj±cej na zmianê stanu podczas obliczania wyra¿enia.
Czy faktycznie był to dobry pomysł? Czy moglibyśmy poradzić sobie
Czy faktycznie by³ to dobry pomys³? Czy mogliby¶my poradziæ sobie
przy pomocy tranzycji postaci
przy pomocy tranzycji postaci


Linia 525: Linia 525:
</math>
</math>


Spróbujmy! Oto nowa wersja jednej z reguł dla <math>\mathbf{let}\, x = e_1 \,\mathbf{in}\, e_2</math>
Spróbujmy! Oto nowa wersja jednej z regu³ dla <math>\mathbf{let}\, x = e_1 \,\mathbf{in}\, e_2</math>
dotycząca kroku wewnątrz <math>e_1</math>:
dotycz±ca kroku wewn±trz <math>e_1</math>:


<math>
<math>
Linia 533: Linia 533:
</math>
</math>


Dotychczas nie ma problemu: podwyrażenie <math>e_1</math> jest
Dotychczas nie ma problemu: podwyra¿enie <math>e_1</math> jest
prawidłowo obliczane w stanie <math>s</math>. Trudność pojawi się, gdy
prawid³owo obliczane w stanie <math>s</math>. Trudno¶æ pojawi siê, gdy
zakończymy obliczanie <math>e_1</math> i przejdziemy do <math>e_2</math>.
zakoñczymy obliczanie <math>e_1</math> i przejdziemy do <math>e_2</math>.
Oto możliwa reguła:
Oto mo¿liwa regu³a:


<math>
<math>
Linia 543: Linia 543:
</math>
</math>


Okazuje się, że wszystko jest w porządku. Wyrażenie <math>e</math>
Okazuje siê, ¿e wszystko jest w porz±dku. Wyra¿enie <math>e</math>
obliczamy w prawidłowym stanie, tzn. z wartością <math>n</math>
obliczamy w prawid³owym stanie, tzn. z warto¶ci± <math>n</math>
przypisaną zmiennej <math>x</math>.
przypisan± zmiennej <math>x</math>.
Mały krok w <math>e</math> daje przyczynek do małego kroku w całym
Ma³y krok w <math>e</math> daje przyczynek do ma³ego kroku w ca³ym
wyrażeniu, a przy tym stan pozostaje niezmieniony.
wyra¿eniu, a przy tym stan pozostaje niezmieniony.
Przy tym wogóle nie potrzebujemy przywracać poprzedniej wartości
Przy tym wogóle nie potrzebujemy przywracaæ poprzedniej warto¶ci
zmiennej <math>x</math>, ponieważ <math>x</math> zyskuje nową wartość
zmiennej <math>x</math>, poniewa¿ <math>x</math> zyskuje now± warto¶æ
''tylko'' na potrzeby obliczania podwyrażenia <math>e</math>!
''tylko'' na potrzeby obliczania podwyra¿enia <math>e</math>!
Można na to również spojrzeć inaczej: informacja o nowej wartości
Mo¿na na to równie¿ spojrzeæ inaczej: informacja o nowej warto¶ci
<math>n</math>  dla zmiennej <math>x</math> nie jest jawnie dodawana do stanu
<math>n</math>  dla zmiennej <math>x</math> nie jest jawnie dodawana do stanu
<math>s</math>, ale jest przechowywana w składni wyrażenia
<math>s</math>, ale jest przechowywana w sk³adni wyra¿enia
<math>\mathbf{let}\, x = n \,\mathbf{in}\, \ldots</math> jako deklaracja <math>x = n</math>.
<math>\mathbf{let}\, x = n \,\mathbf{in}\, \ldots</math> jako deklaracja <math>x = n</math>.
Na końcu musimy oczywiście pozbyć się tej deklaracji za pomocą
Na koñcu musimy oczywi¶cie pozbyæ siê tej deklaracji za pomoc±
następującej tranzycji:
nastêpuj±cej tranzycji:


<math>
<math>
Linia 562: Linia 562:
</math>
</math>


Podsumujmy. Okazuje się, że rozwiązanie nie było wcale łatwe,
Podsumujmy. Okazuje siê, ¿e rozwi±zanie nie by³o wcale ³atwe,
nawet dla tak prościutkiego języka. W przyszłości przekonamy się,
nawet dla tak pro¶ciutkiego jêzyka. W przysz³o¶ci przekonamy siê,
że łatwiej jest poradzić sobie z zagadnieniem wiązania identyfikatorów
¿e ³atwiej jest poradziæ sobie z zagadnieniem wi±zania identyfikatorów
w semantyce naturalnej (duże kroki).
w semantyce naturalnej (du¿e kroki).
W wariancie 1 i 2 wprowadziliśmy do języka dodatkowe elementy, tak,
W wariancie 1 i 2 wprowadzili¶my do jêzyka dodatkowe elementy, tak,
by łatwiej było pisać reguły. W przyszłości będziemy czasem stosować
by ³atwiej by³o pisaæ regu³y. W przysz³o¶ci bêdziemy czasem stosowaæ
takie podejście.
takie podej¶cie.
Niekiedy jednak rozszerzanie języka będzie zabronione.
Niekiedy jednak rozszerzanie jêzyka bêdzie zabronione.


</div></div>
</div></div>
Linia 578: Linia 578:




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


Zapisz wariant 2 semantyki z poprzedniego zadania.
Zapisz wariant 2 semantyki z poprzedniego zadania.
}}




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


Dotychczas wystąpienie błędu podczas obliczania wyrażenia,
Dotychczas wyst±pienie b³êdu podczas obliczania wyra¿enia,
np. odwołanie do niezainicjowanej zmiennej, powodowało, że
np. odwo³anie do niezainicjowanej zmiennej, powodowa³o, ¿e
wyrażenie nie posiadało wartości (nie było ciągu tranzycji
wyra¿enie nie posiada³o warto¶ci (nie by³o ci±gu tranzycji
prowadzących do konfiguracji końcowej). Zmodyfikuj którąś z semantyk
prowadz±cych do konfiguracji koñcowej). Zmodyfikuj któr±¶ z semantyk
z poprzednich zadań tak, aby błąd był komunikowany
z poprzednich zadañ tak, aby b³±d by³ komunikowany
jako jedna z konfiguracji końcowych. To znaczy: jeśli obliczenie
jako jedna z konfiguracji koñcowych. To znaczy: je¶li obliczenie
wyrażenia <math>e</math> w stanie <math>s</math> jest niemożliwe bo wystąpił
wyra¿enia <math>e</math> w stanie <math>s</math> jest niemo¿liwe bo wyst±pi³
błąd, to
b³±d, to


<math>
<math>
e, s \,\Longrightarrow^{*}\, \mathtt{Blad}
e, s \,\Longrightarrow^{*}\, \mathtt{Blad}.
</math>
</math>
}}




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


Rozważ rozszerzenie języka wyrażeń o wyrażenia boolowskie:
Rozwa¿ rozszerzenie jêzyka wyra¿eñ o wyra¿enia boolowskie:


<math>
<math>
Linia 630: Linia 632:
</math>
</math>


Zaproponuj semantykę małych kroków dla tego języka.
Zaproponuj semantykê ma³ych kroków dla tego jêzyka.
Rozważ różne strategie obliczania wyrażeń boolowskich, oraz podejście leniwe.
Rozwa¿ ró¿ne strategie obliczania wyra¿eñ boolowskich, oraz podej¶cie leniwe.
Na przykład w strategii lewostronnej dla <math>b_1 \land b_2</math>,
Na przyk³ad w strategii lewostronnej dla <math>b_1 \land b_2</math>,
gdy <math>b_1</math> zostało obliczone do <math>\mathbf{false}</math>, nie ma wogóle potrzeby
gdy <math>b_1</math> zosta³o obliczone do <math>\mathbf{false}</math>, w podej¶ciu leniwym nie ma wogóle potrzeby
obliczania <math>b_2</math>.
obliczania <math>b_2</math>.
}}

Wersja z 07:57, 9 sie 2006


Zawarto¶æ

Tematem tych zajêæ jest semantyka operacyjna wyra¿eñ (ma³e kroki).


Semantyka operacyjna wyra¿eñ

Ćwiczenie 1

Rozwa¿my bardzo prosty jêzyk wyra¿eñ, którego sk³adnia opisana jest nastêpuj±c± gramatyk±:

n::=0|1|…

x::=…(identyfikatory)…

e::=n|x|e1+e2|𝐢𝐟e1𝐭𝐡𝐞𝐧e2𝐞𝐥𝐬𝐞e3

Wynikiem wyra¿enienia warunkowego 𝐢𝐟e1𝐭𝐡𝐞𝐧e2𝐞𝐥𝐬𝐞e3 jest warto¶æ wyra¿enia e2, o ile wyra¿enie e1 oblicza siê do warto¶ci ró¿nej od zera; w przeciwnym przypadku wynikiem jest warto¶æ wyra¿enia e3.

Zaproponuj semantykê operacyjn± (ma³e kroki) dla tego jêzyka.


Rozwiązanie

{{{3}}}


Ćwiczenie 2

Rozszerzmy jêzyk wyra¿eñ z poprzedniego zadania o jedn± konstrukcjê

e::=…|𝐥𝐞𝐭x=e1𝐢𝐧e2

Wyra¿enie 𝐥𝐞𝐭x=e1𝐢𝐧e2 zawiera w sobie deklaracjê x=e1, która stanowi mechanizm wi±zania identyfikatorów w naszym jêzyku. Deklaracja x=e1 wprowadza now± zmienn± x oraz przypisuje jej warto¶æ. Warto¶æ wyra¿enia 𝐥𝐞𝐭x=e1𝐢𝐧e2 obliczamy nastêpuj±co: najpierw oblicza siê warto¶æ e1, podstawia j± na zmienna x, a nastêpnie oblicza wyra¿enie e2. Zakresem zmiennej x jest wyra¿enie e2, czyli wewn±trz e2 mo¿na odwo³ywaæ siê (wielokrotnie) do zmiennej x; Ogólniej, odwo³ania do zmiennej w wyra¿eniu odnosz± siê do najbli¿szej (najbardziej zagnie¿dzonej) deklaracji tej zmiennej. Taki mechanizm wi±zania identyfikatorów nazywamy wi±zaniem statycznym. Przyjmujemy zwyk³e (statyczne) regu³y przes³aniania zmiennych, np. je¶li w e2 wystêpuje podwyra¿enie 𝐥𝐞𝐭x=e𝐢𝐧e′ to deklaracja x=e przes³ania deklaracjê x=e1 w wyra¿eniu e′.

Zak³adamy, ¿e na pocz±tku warto¶ci wszystkich zmiennych s± nieokre¶lone, czyli zmienne s± niezainicjowane, a odwo³anie do niezainicjowanej zmiennej jest uwa¿ane za niepoprawne.


Przykład

𝐥𝐞𝐭x=0𝐢𝐧𝐥𝐞𝐭y=7𝐢𝐧𝐥𝐞𝐭x=y+3𝐢𝐧x+x+y↦wynik=24

𝐥𝐞𝐭y=5𝐢𝐧𝐥𝐞𝐭x=(𝐥𝐞𝐭y=3𝐢𝐧y+y)𝐢𝐧x+y↦wynik=11

Parser nie mógł rozpoznać (błąd składni): {\displaystyle \mathbf{let}\, z = 5 \,\mathbf{in}\, x+z \quad \quad \mapsto \quad \quad \mbox{brak wyniku; odwo³anie do niezainicjowanej zmiennej}\, x }

𝐥𝐞𝐭x=1𝐢𝐧𝐥𝐞𝐭x=x+x𝐢𝐧x+x↦wynik=4


Rozwiązanie

{{{3}}}


Zadania domowe

Ćwiczenie 1

Zapisz wariant 2 semantyki z poprzedniego zadania.


Ćwiczenie 2

Dotychczas wyst±pienie b³êdu podczas obliczania wyra¿enia, np. odwo³anie do niezainicjowanej zmiennej, powodowa³o, ¿e wyra¿enie nie posiada³o warto¶ci (nie by³o ci±gu tranzycji prowadz±cych do konfiguracji koñcowej). Zmodyfikuj któr±¶ z semantyk z poprzednich zadañ tak, aby b³±d by³ komunikowany jako jedna z konfiguracji koñcowych. To znaczy: je¶li obliczenie wyra¿enia e w stanie s jest niemo¿liwe bo wyst±pi³ b³±d, to

e,s⟹*Blad.


Ćwiczenie 3

Rozwa¿ rozszerzenie jêzyka wyra¿eñ o wyra¿enia boolowskie:

n::=0|1|…

x::=…(identyfikatory)…

b::=𝐭𝐫𝐮𝐞|𝐟𝐚𝐥𝐬𝐞|e1≤e2|¬b|b1∧b2

e::=n|x|e1+e2|𝐢𝐟b𝐭𝐡𝐞𝐧e2𝐞𝐥𝐬𝐞e3|𝐥𝐞𝐭x=e1𝐢𝐧e2

Zaproponuj semantykê ma³ych kroków dla tego jêzyka. Rozwa¿ ró¿ne strategie obliczania wyra¿eñ boolowskich, oraz podej¶cie leniwe. Na przyk³ad w strategii lewostronnej dla b1∧b2, gdy b1 zosta³o obliczone do 𝐟𝐚𝐥𝐬𝐞, w podej¶ciu leniwym nie ma wogóle potrzeby obliczania b2.

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