Semantyka i weryfikacja programów/Ćwiczenia 3: Różnice pomiędzy wersjami

Aktualna wersja na dzień 21:43, 11 wrz 2023

Zawartość

Kończymy semantykę małych kroków i rozpoczynamy semantykę naturalną (duże kroki). Uzupełnimy semantykę naturalną języka TINY o semantykę naturalną wyrażeń boolowskich i arytmetycznych oraz semantykę błędów wykonania. Wreszcie dodamy nową instrukcję pętli $𝐥 𝐨 𝐨 𝐩$ ,, pozwalającą na niestrukturalne przerwanie lub wznowienie iteracji (instrukcje $𝐞 𝐱 𝐢 𝐭$ i $𝐜 𝐨 𝐧 𝐭 𝐢 𝐧 𝐮 𝐞$ ).

Rozszerzenia semantyki języka Tiny

Ćwiczenie 1

Zdefiniuj znaczenie wyrażeń boolowskich i arytmetycznych w języku TINY w stylu dużych kroków (semantyka naturalna).

Rozwiązanie

Przypomnijmy składnię wyrażeń boolowskich i arytmetycznych języka TINY:

$b : : = l | e_{1} \leq e_{2} | \neg b | b_{1} \land b_{2} | \dots$

$l : : = 𝐭 𝐫 𝐮 𝐞 | 𝐟 𝐚 𝐥 𝐬 𝐞$

$e : : = n | x | e_{1} + e_{2} | \dots$

$n : : = 0 | 1 | \dots$

$x : : = \dots (i d e n t y f i k a t o r y) \dots$

Chcemy, aby tranzycje wyrażeń wyglądały następująco:

$e, s ⟶ n b, s ⟶ l$ ,

gdzie $s \in 𝐒 𝐭 𝐚 𝐭 𝐞$ , $n \in$ jest liczbą całkowitą, $n \in 𝐍 𝐮 𝐦$ , a $l \in 𝐁 𝐨 𝐨 𝐥 = {𝐭 𝐫 𝐮 𝐞, 𝐟 𝐚 𝐥 𝐬 𝐞}$ . Tranzycja taka oznacza, że wyrażenie $e$ w stanie $s$ wylicza się do wartości $n$ oraz analogicznie, wyrażenie logiczne $b$ w stanie $s$ wylicza się do $l$ . Zatem zbiór konfiguracji dla semantyki całego języka Tiny to znów

$((𝐄 𝐱 𝐩 \cup 𝐁 𝐄 𝐱 𝐩 \cup 𝐒 𝐭 𝐦 𝐭) \times 𝐒 𝐭 𝐚 𝐭 𝐞) ⋃ 𝐍 𝐮 𝐦 \cup 𝐁 𝐨 𝐨 𝐥 \cup 𝐒 𝐭 𝐚 𝐭 𝐞$ a konfiguracje końcowe to $𝐒 𝐭 𝐚 𝐭 𝐞$ tak jak poprzednio. Tranzycje dla instrukcji pozostają zasadniczo bez zmian, z tym że odwołania do funkcji semantycznych dla wyrażen zastępujemy przez odpowiednie tranzycje. Np. dla instrukcji pętli będziemy mieć następujące reguły:

$\frac{b, s ⟶ 𝐭 𝐫 𝐮 𝐞 I; 𝐰 𝐡 𝐢 𝐥 𝐞 b 𝐝 𝐨 I, s ⟶ s^{'}}{𝐰 𝐡 𝐢 𝐥 𝐞 b 𝐝 𝐨 I, s ⟶ s^{'}}$

$\frac{b, s ⟶ 𝐟 𝐚 𝐥 𝐬 𝐞}{𝐰 𝐡 𝐢 𝐥 𝐞 b 𝐝 𝐨 I, s ⟶ s}$

Podobnie dla instrukcji warunkowej. Teraz zajmiemy się tranzycjami dla wyrażeń. Zacznijmy od stałych arytmetycznych i boolowskich:

$n, s ⟶ n l, s ⟶ l$

Operatory arytmetyczne definiujemy następująco:

$\frac{e_{1}, s ⟶ n_{1} e_{2}, s ⟶ n_{2} n = n_{1} + n_{2}}{e_{1} + e_{2}, s ⟶ n}$

Czyli aby obliczyć sumę $e_{1} + e_{2}$ w stanie $s$ , trzeba najpierw obliczyć $e_{1}$ i $e_{2}$ w tym stanie, a następnie dodać obliczone wartości. Zauważmy, że nie specyfikujemy kolejności, w jakiej mają się obliczać obydwa podwyrażenia. I choć tutaj nie ma to żadnego znaczenia, w przyszłości będzie inaczej, gdy jezyk będzie umożliwiał efekty uboczne podczas obliczania wyrażeń.

Podobne reguły można napisać dla pozostałych operacji arytmetycznych, oraz dla spójników logicznych:

$\frac{b_{1}, s ⟶ l_{1} b_{2}, s ⟶ l_{2} l = l_{1} \land l_{2}}{b_{1} \land b_{2}, s ⟶ l}$

(strategia gorliwa). Reguły dla $\leq$ są następujące:

$\frac{e_{1}, s ⟶ n_{1} e_{2}, s ⟶ n_{2} n_{1} \leq n_{2}}{e_{1} \leq e_{2}, s ⟶ 𝐭 𝐫 𝐮 𝐞} \frac{e_{1}, s ⟶ n_{1} e_{2}, s ⟶ n_{2} n_{1} > n_{2}}{e_{1} \leq e_{2}, s ⟶ 𝐟 𝐚 𝐥 𝐬 𝐞}$

Oto inny wariant semantyki spójnika $\land$ , tzw. strategia lewostronna (ponieważ rozpoczynamy od lewego koniunktu):

$\frac{b_{1}, s ⟶ 𝐟 𝐚 𝐥 𝐬 𝐞}{b_{1} \land b_{2}, s ⟶ 𝐟 𝐚 𝐥 𝐬 𝐞} \frac{b_{1}, s ⟶ 𝐭 𝐫 𝐮 𝐞 b_{2}, s ⟶ l}{b_{1} \land b_{2}, s ⟶ l}$

Inny wariant to strategia prawostronna (najpierw $b_{2}$ , potem $b_{1}$ ). Wreszcie rozważmy kombinację obydwu semantyk (strategia równoległa lub leniwa):

$\frac{b_{1}, s ⟶ 𝐟 𝐚 𝐥 𝐬 𝐞}{b_{1} \land b_{2}, s ⟶ 𝐟 𝐚 𝐥 𝐬 𝐞} \frac{b_{2}, s ⟶ 𝐟 𝐚 𝐥 𝐬 𝐞}{b_{1} \land b_{2}, s ⟶ 𝐟 𝐚 𝐥 𝐬 𝐞}$

Czyli jeśli którekolwiek z podwyrażeń daje wynik $𝐟 𝐚 𝐥 𝐬 𝐞$ , to taki wynik zyskuje całe wyrażenie. Dodatkowo potrzebujemy jeszcze reguły:

$\frac{b_{1}, s ⟶ 𝐭 𝐫 𝐮 𝐞 b_{2}, s ⟶ 𝐭 𝐫 𝐮 𝐞}{b_{1} \land b_{2}, s ⟶ 𝐭 𝐫 𝐮 𝐞}$

Pytanie: czy w naszym prostym języku wszystkie cztery strategie obliczania spójnika $\land$ są równoważne?

Reguły dla negacji oraz dla instrukcji przypisania pozostawiamy jako proste ćwiczenie.

Ćwiczenie 2

Rozważ dodatkowo operację dzielenia:

$e : : = \dots | e_{1} / e_{2}$

i rozszerz semantykę z poprzedniego zadania. Dzielenie przez zero jest błędem i kończy natychmiast wykonanie programu. Oprócz stanu wynikiem programu powinna byc informacja o błędzie, jeśli błąd wystąpił.

Rozwiązanie

Dopóki nie wystąpi błąd dzielenia przez zero, semantyka programu powinna być identyczna jak w poprzednim zadaniu. Zatem pozostawiamy wszystkie reguły z poprzedniego zadania. Dodatkowo potrzebujemy reguł, które opiszą

kiedy powstaje błąd oraz
jak zachowuje się program po wystąpieniu błędu

Zaczynamy od pierwszego punktu. W tym celu dodajemy do konfiguracji jedną konfigurację końcową $B l a d$ . Reguła opisująca powstanie błędu może wyglądać np. tak (duże i małe kroki):

$\frac{e_{2}, s ⟶ 0}{e_{1} / e_{2}, s ⟶ B l a d} e_{1} / 0, s ⟹, B l a d$

Pomijamy tutaj reguły dla przypadku, gdy $e_{2}$ oblicza się do wartości różnej od zera. Ponadto dla czytelności przyjęliśmy, że wynikiem tranzycji jest wyłącznie informacja o błędzie, a stan jest zapominany. Bez trudu możnaby wszystkie reguły (zarówno te powyżej jak i te poniżej) zmodyfikować tak, by wraz z informacją o błędzie zwracany był też stan, w którym błąd się pojawił. Np. ostatnia reguła wyglądałaby następująco:

$\frac{e_{2}, s ⟶ 0}{e_{1} / e_{2}, s ⟶ B l a d, s} e_{1} / 0, s ⟹, B l a d, s$

i zamiast pojedyńczej konfiguracji końcowej $B l a d$ potrzebowalibyśmy oczywiście całego zbioru ${B l a d} \times 𝐒 𝐭 𝐚 𝐭 𝐞$ .

Przejdźmy teraz do drugiego punktu. Potrzebujemy dodatkowych reguł, które zagwarantują, że błąd, raz pojawiwszy się, propaguje się przez wszystkie konstrukcje składniowe, a normalne obliczenie wyrażenia jest wstrzymame.

$\frac{e_{1}, s ⟶ B l a d}{e_{1} \leq e_{2}, s ⟶ B l a d} \frac{e_{2}, s ⟶ B l a d}{e_{1} \leq e_{2}, s ⟶ B l a d}$

Następnie, błąd w wyrażeniu powinien wstrzymać normalne wykonanie instrukcji:

$\frac{b ⟶ B l a d}{𝐢 𝐟 b 𝐭 𝐡 𝐞 𝐧 I_{1} 𝐞 𝐥 𝐬 𝐞 I_{2}, s ⟶ B l a d}$

$\frac{b ⟶ B l a d}{𝐰 𝐡 𝐢 𝐥 𝐞 b 𝐝 𝐨 I, s ⟶ B l a d}$

$\frac{e, s ⟶ B l a d}{x : = e, s ⟶ B l a d}$

I wreszcie błąd powinien propagować się do kolejnych instrukcji:

$\frac{I_{1}, s ⟶ B l a d}{I_{1}; I_{2}, s ⟶ B l a d}$

$\frac{b, s ⟶ 𝐭 𝐫 𝐮 𝐞 I_{1}, s ⟶ B l a d}{𝐢 𝐟 b 𝐭 𝐡 𝐞 𝐧 I_{1} 𝐞 𝐥 𝐬 𝐞 I_{2}, s ⟶ B l a d} \frac{b, s ⟶ 𝐟 𝐚 𝐥 𝐬 𝐞 I_{2}, s ⟶ B l a d}{𝐢 𝐟 b 𝐭 𝐡 𝐞 𝐧 I_{1} 𝐞 𝐥 𝐬 𝐞 I_{2}, s ⟶ B l a d}$

$\frac{b, s ⟶ 𝐭 𝐫 𝐮 𝐞 I, s ⟶ B l a d}{𝐰 𝐡 𝐢 𝐥 𝐞 b 𝐝 𝐨 I, s ⟶ B l a d} \frac{b, s ⟶ 𝐭 𝐫 𝐮 𝐞 I, s ⟶ s^{'} 𝐰 𝐡 𝐢 𝐥 𝐞 b 𝐝 𝐨 I, s^{'} ⟶ B l a d}{𝐰 𝐡 𝐢 𝐥 𝐞 b 𝐝 𝐨 I, s ⟶ B l a d}$

Zwróćmy szczególnie uwagę na ostatnią regułę dla pętli $𝐰 𝐡 𝐢 𝐥 𝐞$ ,: wyraża ona przypadek, gdy błąd został wygenerowany nie w pierwszym obiegu pętli, ale w którymś z kolejnych. Musieliśmy rozważyc również ten przypadek, ponieważ wybraliśmy podejście dużych kroków; w podejściu małych kroków nie byłoby to zapewne konieczne.

Ćwiczenie 3

Rozszerzmy język TINY o następującą instrukcję pętli:

$I : : = 𝐥 𝐨 𝐨 𝐩 I | 𝐞 𝐱 𝐢 𝐭 | 𝐜 𝐨 𝐧 𝐭 𝐢 𝐧 𝐮 𝐞$

$𝐥 𝐨 𝐨 𝐩 I$ to instrukcja pętli, $I$ stanowi instrukcję wewnętrzną. Instrukcja $𝐞 𝐱 𝐢 𝐭$ wychodzi z nabliższej otaczającej pętli $𝐥 𝐨 𝐨 𝐩$ , i kontynuuje wykonanie programu od pierwszej instrukcji za tą pętlą. Instrukcja $𝐜 𝐨 𝐧 𝐭 𝐢 𝐧 𝐮 𝐞$ powraca na początek instrukcji wewnętrznej najbliższej otaczającej pętli $𝐥 𝐨 𝐨 𝐩$ ,.

Pozważ zarówno semantykę naturalną, jak i semantykę małych kroków.

Rozwiązanie

Dodamy do reguł semantyki naturalnej dla języka TINY kilka nowych reguł opisujących nową konstrukcję języka i jej "interakcję" z pozostałymi konstrukcjami.

Pomysł polega na dodaniu specjalnych konfiguracji zawierających informację o tym, że została wykonana instrukcja $𝐞 𝐱 𝐢 𝐭$ lub $𝐜 𝐨 𝐧 𝐭 𝐢 𝐧 𝐮 𝐞$ . Oto odpowiednie reguły:

$𝐞 𝐱 𝐢 𝐭, s ⟶ s, było- 𝐞 𝐱 𝐢 𝐭 𝐜 𝐨 𝐧 𝐭 𝐢 𝐧 𝐮 𝐞, s ⟶ s, było- 𝐜 𝐨 𝐧 𝐭 𝐢 𝐧 𝐮 𝐞$

Czyli instrukcje $𝐞 𝐱 𝐢 𝐭$ i $𝐜 𝐨 𝐧 𝐭 𝐢 𝐧 𝐮 𝐞$ nie modyfikują stanu $s$ , ale zostawiają po sobie "ślad". Zauważmy, że taki ślad zostaje pozostawiony tylko wtedy, jeśli nie było dotychczas innego śladu, to znaczy jeśli $𝐞 𝐱 𝐢 𝐭$ (lub $𝐜 𝐨 𝐧 𝐭 𝐢 𝐧 𝐮 𝐞$ ) zostało wykonane w zwykłym stanie $s$ . Oczywiście poszerzamy odpowiednio zbiór konfiguracji o:

$𝐒 𝐭 𝐚 𝐭 𝐞 \times {było- 𝐞 𝐱 𝐢 𝐭, było- 𝐜 𝐨 𝐧 𝐭 𝐢 𝐧 𝐮 𝐞}$

Pytanie: jakie powinno być zachowanie $𝐞 𝐱 𝐢 𝐭$ i $𝐜 𝐨 𝐧 𝐭 𝐢 𝐧 𝐮 𝐞$ w konfiguracji $s, było- 𝐞 𝐱 𝐢 𝐭$ lub $s, było- 𝐜 𝐨 𝐧 𝐭 𝐢 𝐧 𝐮 𝐞$ ? Czy instrukcje $𝐞 𝐱 𝐢 𝐭$ i $𝐜 𝐨 𝐧 𝐭 𝐢 𝐧 𝐮 𝐞$ będą faktycznie wykonywane w takich konfiguracjach?

Zapiszmy teraz, jak inne instrukcje korzystają z dodatkowej informacji (śladu) zawartej w konfiguracjach. Oczywiście "beneficjentem" korzystającym z tej informacji jest instrukcja $𝐥 𝐨 𝐨 𝐩$ ,:

$\frac{I, s ⟶ s^{'}, było- 𝐞 𝐱 𝐢 𝐭}{𝐥 𝐨 𝐨 𝐩 I, s ⟶ s^{'}} \frac{I, s ⟶ s^{'}, było- 𝐜 𝐨 𝐧 𝐭 𝐢 𝐧 𝐮 𝐞 𝐥 𝐨 𝐨 𝐩 I, s^{'} ⟶ s^{″}}{𝐥 𝐨 𝐨 𝐩 I, s ⟶ s^{″}}$

Czyli w zależności od tego, jaki ślad został zarejestrowany podczas wykonania $I$ , albo kończymy wykonanie pętli $𝐥 𝐨 𝐨 𝐩$ ,, albo rozpoczynamy kolejną iterację. Zauważmy, że stan $s^{'}$ może być różny od $s$ , ponieważ zanim wykonała się ktoraś z instrukcji $𝐞 𝐱 𝐢 𝐭$ lub $𝐜 𝐨 𝐧 𝐭 𝐢 𝐧 𝐮 𝐞$ mogły zostać zmienione wartości niektórych zmiennych.

Oczywiście, jeśli instrukcja wewnętrzna $I$ zakończyła się "normalnie", kontynuujemy wykonanie pętli podobnie jak w przypadku wywołania $𝐜 𝐨 𝐧 𝐭 𝐢 𝐧 𝐮 𝐞$ :

$\frac{I, s ⟶ s^{'} 𝐥 𝐨 𝐨 𝐩 I, s^{'} ⟶ s^{″}}{𝐥 𝐨 𝐨 𝐩 I, s ⟶ s^{″}}$

Pytanie: czy potrzebujemy dodatkowo reguł postaci:

$\frac{I, s ⟶ s^{'} 𝐥 𝐨 𝐨 𝐩 I, s^{'} ⟶ s^{″}, było- 𝐞 𝐱 𝐢 𝐭}{𝐥 𝐨 𝐨 𝐩 I, s ⟶ s^{″}, było- 𝐞 𝐱 𝐢 𝐭} \frac{I, s ⟶ s^{'}, było- 𝐜 𝐨 𝐧 𝐭 𝐢 𝐧 𝐮 𝐞 𝐥 𝐨 𝐨 𝐩 I, s^{'} ⟶ s^{″}, było- 𝐞 𝐱 𝐢 𝐭}{𝐥 𝐨 𝐨 𝐩 I, s ⟶ s^{″}, było- 𝐞 𝐱 𝐢 𝐭}$

Okazuje się że nie, ponieważ ślad powinien zostać zawsze "wymazany" przez pętlę $𝐥 𝐨 𝐨 𝐩$ ,.

Teraz musimy określić zachowanie wszystkich instrukcji w sytuacji, gdy bieżąca konfiguracja zawiera już ślad. Zasadniczo, powinniśmy zaniechać wykonania instrukcji (w przypadku pętli, powinniśmy zaniechać dalszego iterowania tej pętli). Oto odpowiednie reguły dla $było- 𝐞 𝐱 𝐢 𝐭$ :

$\frac{I_{1}, s ⟶ s^{'}, było- 𝐞 𝐱 𝐢 𝐭}{I_{1}; I_{2}, s ⟶ s^{'}, było- 𝐞 𝐱 𝐢 𝐭} \frac{I_{1}, s ⟶ s^{'} I_{2}, s^{'} ⟶ s^{″}, było- 𝐞 𝐱 𝐢 𝐭}{I_{1}; I_{2}, s ⟶ s^{″}, było- 𝐞 𝐱 𝐢 𝐭}$

$\frac{b, s ⟶ 𝐭 𝐫 𝐮 𝐞 I_{1}, s ⟶ s^{'}, było- 𝐞 𝐱 𝐢 𝐭}{𝐢 𝐟 b 𝐭 𝐡 𝐞 𝐧 I_{1} 𝐞 𝐥 𝐬 𝐞 I_{2}, s ⟶ s^{'}, było- 𝐞 𝐱 𝐢 𝐭} \frac{b, s ⟶ 𝐟 𝐚 𝐥 𝐬 𝐞 I_{2}, s ⟶ s^{'}, było- 𝐞 𝐱 𝐢 𝐭}{𝐢 𝐟 b 𝐭 𝐡 𝐞 𝐧 I_{1} 𝐞 𝐥 𝐬 𝐞 I_{2}, s ⟶ s^{'}, było- 𝐞 𝐱 𝐢 𝐭}$

$\frac{b, s ⟶ 𝐭 𝐫 𝐮 𝐞 I, s ⟶ s^{'}, było- 𝐞 𝐱 𝐢 𝐭}{𝐰 𝐡 𝐢 𝐥 𝐞 b 𝐝 𝐨 I, s ⟶ s^{'}, było- 𝐞 𝐱 𝐢 𝐭} \frac{b, s ⟶ 𝐭 𝐫 𝐮 𝐞 I, s ⟶ s^{'} 𝐰 𝐡 𝐢 𝐥 𝐞 b 𝐝 𝐨 I, s^{'} ⟶ s^{″}, było- 𝐞 𝐱 𝐢 𝐭}{𝐰 𝐡 𝐢 𝐥 𝐞 b 𝐝 𝐨 I, s ⟶ s^{'}, było- 𝐞 𝐱 𝐢 𝐭}$

Pominęliśmy zupełnie analogiczne reguły dla $było- 𝐜 𝐨 𝐧 𝐭 𝐢 𝐧 𝐮 𝐞$ . Zauważmy, że dla pętli $𝐰 𝐡 𝐢 𝐥 𝐞$ , nie rozpatrujemy przypadku, gdy dozór $b$ oblicza się do $𝐟 𝐚 𝐥 𝐬 𝐞$ , gdyż w tym przypadku nie ma możliwości wygenerowania śladu.

Zauważmy też, że nasze reguły nie pozwalają na dodanie drugiego (kolejnego) śladu!

Rozwiązanie

W semantyce naturalnej musieliśmy napisać wiele reguł, aby zapewnić pomijanie instrukcji w sytuacji, gdy został juz zarejestrowany jakiś ślad. Było to dość uciążliwe. Okazuje się, że podejście mało-krokowe oferuje możliwość bardziej eleganckiego rozwiązania.

Punktem startowym sę teraz reguły mało-krokowe dla języka TINY.

Podobnie jak poprzednio, rozszerzymy zbiór konfiguracji i podobnie opiszemy, jak powstaje ślad:

$𝐞 𝐱 𝐢 𝐭, s ⟹, s, było- 𝐞 𝐱 𝐢 𝐭 𝐜 𝐨 𝐧 𝐭 𝐢 𝐧 𝐮 𝐞, s ⟹, s, było- 𝐜 𝐨 𝐧 𝐭 𝐢 𝐧 𝐮 𝐞$

Ponadto musimy określić sposób, w jaki mały krok mniejszej instrukcji zostaje zamieniony na mały krok większej. Np.

$\frac{I_{1}, s ⟹, s^{'}, było- 𝐞 𝐱 𝐢 𝐭}{I_{1}; I_{2}, s ⟹, s^{'}, było- 𝐞 𝐱 𝐢 𝐭} i analogicznie dla było- 𝐜 𝐨 𝐧 𝐭 𝐢 𝐧 𝐮 𝐞$

Nie musimy zajmowac się przypadkiem, gdy ślad powstaje w $I_{2}$ , bo wybraliśmy podejście małokrokowe. Ponadto, nie musimy opisywać instrukcji warunkowej i pętli $𝐰 𝐡 𝐢 𝐥 𝐞$ ,, ponieważ ślad nie może powstać podczas obliczania dozoru!

Wreszcie zobaczmy jak zachowuje się pętla $𝐥 𝐨 𝐨 𝐩$ ,:

$\frac{I, s ⟹, s^{'}, było- 𝐞 𝐱 𝐢 𝐭}{𝐥 𝐨 𝐨 𝐩 I, s ⟹, s^{'}} \frac{I, s ⟹, s^{'}, było- 𝐜 𝐨 𝐧 𝐭 𝐢 𝐧 𝐮 𝐞}{𝐥 𝐨 𝐨 𝐩 I, s ⟹, 𝐥 𝐨 𝐨 𝐩 I, s^{'}}$

Reguły te są prawie identyczne z regułami semantyki naturalnej dla tej sytuacji! Natomiast korzystamy z tego, że w podejściu małokrokowym zmiana konfiguracji na $s^{'}, było- 𝐞 𝐱 𝐢 𝐭$ czy $s^{'}, było- 𝐜 𝐨 𝐧 𝐭 𝐢 𝐧 𝐮 𝐞$ jest natychmiast widoczna w instrukcji $𝐥 𝐨 𝐨 𝐩 I$ , nawet jeśli $𝐞 𝐱 𝐢 𝐭$ czy $𝐜 𝐨 𝐧 𝐭 𝐢 𝐧 𝐮 𝐞$ zostało wywołane głęboko wewnątrz $I$ !

Niestety powyższe reguły nie są poprawne! Dlaczego? Jak zwykle w semantyce małych kroków, wykonując instrukcję wewnętrzną "zapominamy" stopniowo, jaka była ona na początku. W związku z tym nie potrafimy poprawnie powrócić do wykonywania pętli $𝐥 𝐨 𝐨 𝐩$ , po wywołaniu $𝐜 𝐨 𝐧 𝐭 𝐢 𝐧 𝐮 𝐞$ .

Prostym sposobem poprawienia naszego błędu jest rozszerzenie składni tak, aby możliwe było jednorazowe rozwinięcie pętli $𝐥 𝐨 𝐨 𝐩$ ,:

$𝐥 𝐨 𝐨 𝐩 I, s ⟹, I 𝐭 𝐡 𝐞 𝐧 𝐥 𝐨 𝐨 𝐩 I, s$

Teraz możemy zapisać dwie powyższe reguły dla $𝐥 𝐨 𝐨 𝐩$ , w poprawnej wersji, pamiętając o tym, że $było- 𝐞 𝐱 𝐢 𝐭$ i $było- 𝐜 𝐨 𝐧 𝐭 𝐢 𝐧 𝐮 𝐞$ pojawią się nie w instrukcji wewnętrznej, ale w jej kopii umieszczonej przed $𝐭 𝐡 𝐞 𝐧$ ,:

$\frac{I^{'}, s ⟹, s^{'}, było- 𝐞 𝐱 𝐢 𝐭}{I^{'} 𝐭 𝐡 𝐞 𝐧 𝐥 𝐨 𝐨 𝐩 I, s ⟹, s^{'}} \frac{I^{'}, s ⟹, s^{'}, było- 𝐜 𝐨 𝐧 𝐭 𝐢 𝐧 𝐮 𝐞}{I^{'} 𝐭 𝐡 𝐞 𝐧 𝐥 𝐨 𝐨 𝐩 I, s ⟹, 𝐥 𝐨 𝐨 𝐩 I, s^{'}} \frac{I^{'}, s ⟹, s^{'}}{I^{'} 𝐭 𝐡 𝐞 𝐧 𝐥 𝐨 𝐨 𝐩 I, s ⟹, 𝐥 𝐨 𝐨 𝐩 I, s^{'}}$

Potrzebujemy też dodatkowej reguły dla obliczeń wewnątrz instrukcji stojącej przed $𝐭 𝐡 𝐞 𝐧$ , (w szczególności może ona zawierać zagnieżdzone pętle $𝐥 𝐨 𝐨 𝐩$ ,):

$\frac{I^{'}, s ⟹, I^{″}, s^{'}}{I^{'} 𝐭 𝐡 𝐞 𝐧 𝐥 𝐨 𝐨 𝐩 I, s ⟹, I^{″} 𝐭 𝐡 𝐞 𝐧 𝐥 𝐨 𝐨 𝐩 I, s^{'}}$

Na koniec zauważmy, że stan $s^{'}$ w pierwszych dwóch z powyższych reguł nigdy nie jest różny od $s$ . Zatem równoważnie moglibyśmy zamienić $s^{'}$ na $s$ w powyższych dwóch regułach. Ale wtedy okazuje się, $s$ w parze z $było- 𝐞 𝐱 𝐢 𝐭$ albo $było- 𝐜 𝐨 𝐧 𝐭 𝐢 𝐧 𝐮 𝐞$ jest nadmiarowe i może zostać wyeliminowane. Zatem ostatecznie nasze reguły mogą wyglądać tak:

$𝐞 𝐱 𝐢 𝐭, s ⟹, było- 𝐞 𝐱 𝐢 𝐭 𝐜 𝐨 𝐧 𝐭 𝐢 𝐧 𝐮 𝐞, s ⟹, było- 𝐜 𝐨 𝐧 𝐭 𝐢 𝐧 𝐮 𝐞$

$\frac{I_{1}, s ⟹, było- 𝐞 𝐱 𝐢 𝐭}{I_{1}; I_{2}, s ⟹, było- 𝐞 𝐱 𝐢 𝐭} \frac{I_{1}, s ⟹, było- 𝐜 𝐨 𝐧 𝐭 𝐢 𝐧 𝐮 𝐞}{I_{1}; I_{2}, s ⟹, było- 𝐜 𝐨 𝐧 𝐭 𝐢 𝐧 𝐮 𝐞}$

$𝐥 𝐨 𝐨 𝐩 I, s ⟹, I 𝐭 𝐡 𝐞 𝐧 𝐥 𝐨 𝐨 𝐩 I, s$

$\frac{I^{'}, s ⟹, było- 𝐞 𝐱 𝐢 𝐭}{I^{'} 𝐭 𝐡 𝐞 𝐧 𝐥 𝐨 𝐨 𝐩 I, s ⟹, s} \frac{I^{'}, s ⟹, było- 𝐜 𝐨 𝐧 𝐭 𝐢 𝐧 𝐮 𝐞}{I^{'} 𝐭 𝐡 𝐞 𝐧 𝐥 𝐨 𝐨 𝐩 I, s ⟹, 𝐥 𝐨 𝐨 𝐩 I, s} \frac{I^{'}, s ⟹, s^{'}}{I^{'} 𝐭 𝐡 𝐞 𝐧 𝐥 𝐨 𝐨 𝐩 I, s ⟹, 𝐥 𝐨 𝐨 𝐩 I, s}$

$\frac{I^{'}, s ⟹, I^{″}, s^{'}}{I^{'} 𝐭 𝐡 𝐞 𝐧 𝐥 𝐨 𝐨 𝐩 I, s ⟹, I^{″} 𝐭 𝐡 𝐞 𝐧 𝐥 𝐨 𝐨 𝐩 I, s^{'}}$

a zbiór konfiguracji poszerzamy tylko o dwie nowe konfiguracje ${było- 𝐞 𝐱 𝐢 𝐭, było- 𝐜 𝐨 𝐧 𝐭 𝐢 𝐧 𝐮 𝐞}$ .

Zadania domowe

Ćwiczenie 1

Zaproponuj semantykę małokrokową dla rozszerzeń języka Tiny, które studiowaliśmy powyżej.

Ćwiczenie 2

Napisz semantykę naturalną dla nieznacznie rozszerzonej wersji instrukcji $𝐥 𝐨 𝐨 𝐩$ ,:

$I : : = x : 𝐥 𝐨 𝐨 𝐩 I | 𝐞 𝐱 𝐢 𝐭 x | 𝐜 𝐨 𝐧 𝐭 𝐢 𝐧 𝐮 𝐞 x$

Identyfikator $x$ pełni tutaj rolę etykiety związanej z instrukcją $𝐥 𝐨 𝐨 𝐩$ ,, jest też parametrem dwóch pozostałych instrukcji. $𝐞 𝐱 𝐢 𝐭 x$ kończy teraz najbliższą otaczającą pętlę $𝐥 𝐨 𝐨 𝐩$ , o etykiecie $x$ . Podobnie $𝐜 𝐨 𝐧 𝐭 𝐢 𝐧 𝐮 𝐞 x$ wznawia najbliższą otaczającą pętlę o etykiecie $x$ .

Przykład

Program

x:  $𝐥 𝐨 𝐨 𝐩$ ,
  a := 1; 
  y:  $𝐥 𝐨 𝐨 𝐩$ ,
     $𝐞 𝐱 𝐢 𝐭$  x;
    a := a-10;
  a := a+1;
a := a+2;

kończy działanie z wartością zmiennej $a = 3$ . Za pomocą wcięć określiliśmy, do wnętrza której pętli $𝐥 𝐨 𝐨 𝐩$ , należy każda z trzech ostatnich instrukcji przypisania. Niejednoznaczność bierze się oczywiście stąd, że pracujemy ze składnią abstrakcyjną. Składnia konkretna zawierałaby prawdopodobnie jakąś konstukcję "zamykającą" pętlę $𝐥 𝐨 𝐨 𝐩$ ,, np. $𝐥 𝐨 𝐨 𝐩 I 𝐞 𝐧 𝐝 𝐥 𝐨 𝐨 𝐩$ ,.

Ćwiczenie 3

Napisz semantykę naturalną i małokrokową dla rozszerzenia języka TINY o wyrażenia z efektami ubocznymi:

$e : : = \dots | 𝐝 𝐨 I 𝐭 𝐡 𝐞 𝐧 e | x : = e | x + + | \dots$

Obliczenie wyrażenia $𝐝 𝐨 I 𝐭 𝐡 𝐞 𝐧 e$ polega na wykonaniu $I$ a potem na obliczeniu $e$ . Wartość wyrażenia $x : = e$ jest taka, jak wartość wyrażenia $e$ a efektem ubocznym jest podstawienie tej wartości na zmienną $x$ .

Semantyka i weryfikacja programów/Ćwiczenia 3: Różnice pomiędzy wersjami

Aktualna wersja na dzień 21:43, 11 wrz 2023

Zawartość

Rozszerzenia semantyki języka Tiny

Zadania domowe

Menu nawigacyjne

Działania na stronie

Opcje strony

Narzędzia osobiste

Nawigacja

Szukaj

Narzędzia

@@ Linia 1: / Linia 1: @@
+== Zawartość ==
-== Ćwiczenia 3: Dodawanie binarne (małe kroki) ==
+Kończymy semantykę małych kroków i rozpoczynamy semantykę naturalną (duże kroki).
+Uzupełnimy semantykę naturalną języka TINY o semantykę naturalną wyrażeń boolowskich i arytmetycznych oraz semantykę błędów wykonania.
+Wreszcie dodamy nową instrukcję pętli <math>\mathbf{loop}\ </math>,, pozwalającą na niestrukturalne przerwanie lub wznowienie iteracji (instrukcje <math>\mathbf{exit}</math> i <math>\mathbf{continue}</math>).
-== Zadania z rozwiązaniami ==
+== Rozszerzenia semantyki języka Tiny ==
-==== Zadanie 1 ====
+{{cwiczenie|1|cw1|
-Rozważmy następujący język wyrażeń (liczby binarne z dodawaniem):
+Zdefiniuj znaczenie wyrażeń boolowskich i arytmetycznych w języku TINY w stylu dużych kroków (semantyka naturalna).
+}}
+<div class="mw-collapsible mw-made=collapsible mw-collapsed">
+<span class="mw-collapsible-toogle mw-collapsible-toogle-default style="font-variant:small-caps">Rozwiązanie</span>
+<div class="mw-collapsible-content" style="display:none">
+Przypomnijmy składnię wyrażeń boolowskich i arytmetycznych języka TINY:
 <math>
-e \, ::= \,\,
+b \, ::= \,\,
-      \epsilon  \,\,|\,\,
+        l \,\,|\,\,
-      e 0  \,\,|\,\,
+        e_1 \leq e_2  \,\,|\,\,
-      e 1  \,\,|\,\,
+        \neg b  \,\,|\,\,
-      e_1 + e_2
+        b_1  \land  b_2   \,\,|\,\, \ldots
 </math>
-<math> \epsilon </math> oznacza słowo puste, czyli np. <math> \epsilon 1 0 1 </math>
+<math>
-oznacza binarną liczbę 101.
+l \, ::= \,\,
-Napisz semantykę operacyjną obliczającą wartość wyrażeń.
+        \mathbf{true}    \,\,|\,\,
+        \mathbf{false}
+</math>
+<math>
+e \,  ::= \,\,
+        n  \,\,|\,\,
+        x  \,\,|\,\,
+        e_1 + e_2  \,\,|\,\, \ldots
+</math>
-==== Rozwiązanie ====
+<math>
+n \, ::= \,\, 0 \,\,|\,\, 1 \,\,|\,\, \ldots
+</math>
-Składnia wyrażeń pozwala na wygodny dostęp do najmniej znaczącego
+<math>
-bitu liczby. Spróbujmy zatem zastosować metodę dodawania
+x \, ::= \,\, \ldots \, (identyfikatory) \, \ldots
-pisemnego:
+</math>
+Chcemy, aby tranzycje wyrażeń wyglądały następująco:
+<math>
+e, s \longrightarrow n
+\quad \quad \quad
+b, s \longrightarrow l</math>,
+gdzie <math>s \in \mathbf{State}</math>, <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>.
+Tranzycja taka oznacza, że wyrażenie <math>e</math> w stanie <math>s</math> wylicza się do wartości <math>n</math> oraz analogicznie, wyrażenie logiczne <math>b</math> w stanie <math>s</math> wylicza się do <math>l</math>.
+Zatem zbiór konfiguracji dla semantyki całego języka Tiny to znów
 <math>
-e_1 0 + e_2 0 \,\Longrightarrow\, (e_1 + e_2) 0
+( (\mathbf{Exp} \, \cup \, \mathbf{BExp} \, \cup \, \mathbf{Stmt}) \times \mathbf{State} ) \, \bigcup \,
+\mathbf{Num} \, \cup \, \mathbf{Bool} \, \cup \, \mathbf{State}
 </math>
+a konfiguracje końcowe to <math>\mathbf{State}</math> tak jak poprzednio.
+Tranzycje dla instrukcji pozostają zasadniczo bez zmian, z tym że odwołania do funkcji semantycznych dla wyrażen zastępujemy przez odpowiednie tranzycje.
+Np. dla instrukcji pętli będziemy mieć następujące reguły:
 <math>
-e_1 0 + e_2 1 \,\Longrightarrow\, (e_1 + e_2) 1
+\frac{b, s \,\longrightarrow\, \mathbf{true}  \quad \quad  I; \mathbf{while}\, b \,\mathbf{do}\, I, s \,\longrightarrow\, s'}
+      {\mathbf{while}\, b \,\mathbf{do}\, I, s \,\longrightarrow\, s'}
 </math>
 <math>
-e_1 1 + e_2 0 \,\Longrightarrow\, (e_1 + e_2) 1
+\frac{b, s \,\longrightarrow\, \mathbf{false}}
+     {\mathbf{while}\, b \,\mathbf{do}\, I, s \,\longrightarrow\, s}
 </math>
-Ale co zrobić z przeniesieniem?
+Podobnie dla instrukcji warunkowej.
+Teraz zajmiemy się tranzycjami dla wyrażeń.
+Zacznijmy od stałych arytmetycznych i boolowskich:
+<math>
+n, s \,\longrightarrow\, n
+\quad \quad
+l, s \,\longrightarrow\, l</math>
+Operatory arytmetyczne definiujemy następująco:
 <math>
-e_1 1 + e_2 1 \,\Longrightarrow\, ?
+\frac{e_1, s \,\longrightarrow\, n_1   \quad \quad
+      e_2, s \,\longrightarrow\, n_2 \quad \quad
+      n = n_1 + n_2    }
+     {e_1 + e_2,s \,\longrightarrow\, n}
 </math>
-Podstawowy pomysł to potraktować przeniesienie jak dodatkowy składnik:
+Czyli aby obliczyć sumę <math>e_1 + e_2</math> w stanie <math>s</math>, trzeba najpierw obliczyć <math>e_1</math> i <math>e_2</math> w tym stanie, a następnie dodać obliczone wartości.
+Zauważmy, że nie specyfikujemy kolejności, w jakiej mają się obliczać obydwa podwyrażenia.
+I choć tutaj nie ma to żadnego znaczenia, w przyszłości będzie inaczej, gdy jezyk będzie umożliwiał efekty uboczne podczas obliczania wyrażeń.
+Podobne reguły można napisać dla pozostałych operacji arytmetycznych, oraz dla spójników logicznych:
 <math>
-e_1 1 + e_2 1 \,\Longrightarrow\, ((e_1 + e_2) + 1) 0
+\frac{b_1, s \,\longrightarrow\, l_1  \quad \quad
+      b_2, s \,\longrightarrow\, l_2  \quad \quad
+      l = l_1 \land l_2}
+     {b_1  \land  b_2, s \,\longrightarrow\, l}
 </math>
-Zauważmy, że w składni dopuszcza się dowolne przeplatanie operatora dodawania
+(strategia gorliwa).
-i bitów <math> 0, 1 </math>. Tę dowolność wykorzystaliśmy właśnie w regułach
+Reguły dla <math>\leq</math> są następujące:
-powyżej. Gdyby nasz język ograniczyć tylko do składni
 <math>
-e \, ::= \,\,
+\frac{e_1, s \,\longrightarrow\, n_1 \quad \quad e_2, s \,\longrightarrow\, n_2 \quad \quad n_1 \leq n_2}
-      b  \,\,|\,\,
+     {e_1 \leq e_2, s \,\longrightarrow\, \mathbf{true}}
-      e_1 + e_2
+\quad \quad
+\frac{e_1, s \,\longrightarrow\, n_1 \quad \quad e_2, s \,\longrightarrow\, n_2 \quad \quad n_1 > n_2}
+     {e_1 \leq e_2, s \,\longrightarrow\, \mathbf{false}}
 </math>
+Oto inny wariant semantyki spójnika <math>\land</math>, tzw. strategia lewostronna (ponieważ rozpoczynamy od ''lewego'' koniunktu):
 <math>
-b \, ::= \,\,
+\frac{b_1, s \,\longrightarrow\, \mathbf{false}}
-       \epsilon  \,\,|\,\,
+     {b_1 \land b_2, s \,\longrightarrow\, \mathbf{false}}
-       b 0  \,\,|\,\,
+\quad \quad
-       b 1
+\frac{b_1, s \,\longrightarrow\, \mathbf{true}  \quad \quad
+      b_2, s \,\longrightarrow\, l}
+     {b_1 \land b_2, s \,\longrightarrow\, l}
+</math>
+Inny wariant to strategia prawostronna (najpierw <math>b_2</math>, potem <math>b_1</math>).
+Wreszcie rozważmy kombinację obydwu semantyk (strategia ''równoległa'' lub ''leniwa''):
+<math>
+\frac{b_1, s \,\longrightarrow\, \mathbf{false}}
+     {b_1 \land b_2, s \,\longrightarrow\, \mathbf{false}}
+\quad \quad \quad
+\frac{b_2, s \,\longrightarrow\, \mathbf{false}}
+      {b_1 \land b_2, s \,\longrightarrow\, \mathbf{false}}
+</math>
+Czyli jeśli którekolwiek z podwyrażeń daje wynik <math>\mathbf{false}</math>, to taki wynik zyskuje całe wyrażenie.
+Dodatkowo potrzebujemy jeszcze reguły:
+<math>
+\frac{b_1, s \,\longrightarrow\, \mathbf{true}  \quad \quad
+      b_2, s \,\longrightarrow\, \mathbf{true}}
+     {b_1 \land b_2,s \,\longrightarrow\, \mathbf{true}}
+</math>
+'''Pytanie:''' czy w naszym prostym języku wszystkie cztery strategie obliczania spójnika <math>\land</math> są równoważne?
+Reguły dla negacji oraz dla instrukcji przypisania pozostawiamy jako proste ćwiczenie.
+</div></div>
+{{cwiczenie|2|cw2|
+Rozważ dodatkowo operację dzielenia:
+<math>
+e \, ::= \,\,   \ldots   \,\,|\,\,
+        e_1 / e_2
+</math>
+i rozszerz semantykę z poprzedniego zadania.
+Dzielenie przez zero jest błędem i kończy natychmiast wykonanie programu.
+Oprócz stanu wynikiem programu powinna byc informacja o błędzie, jeśli błąd wystąpił.
+}}
+<div class="mw-collapsible mw-made=collapsible mw-collapsed">
+<span class="mw-collapsible-toogle mw-collapsible-toogle-default style="font-variant:small-caps">Rozwiązanie</span>
+<div class="mw-collapsible-content" style="display:none">
+Dopóki nie wystąpi błąd dzielenia przez zero, semantyka programu
+powinna być identyczna jak w poprzednim zadaniu. Zatem pozostawiamy wszystkie reguły z poprzedniego zadania.
+Dodatkowo potrzebujemy reguł, które opiszą
+* kiedy powstaje błąd oraz
+* jak zachowuje się program po wystąpieniu błędu
+Zaczynamy od pierwszego punktu.
+W tym celu dodajemy do konfiguracji jedną konfigurację końcową <math>\mathtt{Blad}</math>.
+Reguła opisująca powstanie błędu może wyglądać np. tak (duże i małe kroki):
+<math>
+\frac{e_2, s \,\longrightarrow\, 0}
+{e_1 / e_2, s \,\longrightarrow\, \mathtt{Blad}}
+\quad \quad
+e_1 / 0, s \,\Longrightarrow, \mathtt{Blad}</math>
+Pomijamy tutaj reguły dla przypadku, gdy <math>e_2</math> oblicza się do wartości różnej od zera.
+Ponadto dla czytelności przyjęliśmy, że wynikiem tranzycji jest wyłącznie informacja o błędzie, a stan jest zapominany.
+Bez trudu możnaby wszystkie reguły (zarówno te powyżej jak i te poniżej) zmodyfikować tak, by wraz z informacją o błędzie zwracany był też stan, w którym błąd się pojawił.
+Np. ostatnia reguła wyglądałaby następująco:
+<math>
+\frac{e_2, s \,\longrightarrow\, 0}
+{e_1 / e_2, s \,\longrightarrow\, \mathtt{Blad}, s}
+\quad \quad
+e_1 / 0, s \,\Longrightarrow, \mathtt{Blad}, s
+</math>
+i zamiast pojedyńczej konfiguracji końcowej <math>\mathtt{Blad}</math> potrzebowalibyśmy oczywiście całego zbioru <math>\{ \mathtt{Blad} \} \times \mathbf{State}</math>.
+Przejdźmy teraz do drugiego punktu. Potrzebujemy dodatkowych reguł, które zagwarantują, że błąd, raz pojawiwszy się, propaguje się przez wszystkie konstrukcje składniowe, a normalne obliczenie wyrażenia jest wstrzymame.
+<math>
+\frac{e_1, s \,\longrightarrow\, \mathtt{Blad}}
+     {e_1 \leq e_2, s \,\longrightarrow\, \mathtt{Blad}}
+\quad \quad \quad
+\frac{e_2, s \,\longrightarrow\, \mathtt{Blad}}
+       {e_1 \leq e_2, s \,\longrightarrow\, \mathtt{Blad}}
+</math>
+Następnie, błąd w wyrażeniu powinien wstrzymać normalne wykonanie instrukcji:
+<math>
+\frac{b \,\longrightarrow\, \mathtt{Blad}}
+{\mathbf{if}\, b \,\mathbf{then}\, I_1 \,\mathbf{else}\, I_2, s \,\longrightarrow\, \mathtt{Blad}}
+</math>
+<math>
+\frac{b \,\longrightarrow\, \mathtt{Blad}}
+{\mathbf{while}\, b \,\mathbf{do}\, I, s \,\longrightarrow\, \mathtt{Blad}}
+</math>
+<math>
+\frac{e, s \,\longrightarrow\, \mathtt{Blad}}
+     {x := e, s \,\longrightarrow\, \mathtt{Blad}}
+</math>
+I wreszcie błąd powinien propagować się do kolejnych instrukcji:
+<math>
+\frac{I_1, s \,\longrightarrow\, \mathtt{Blad}}
+     {I_1;\, I_2, s \,\longrightarrow\, \mathtt{Blad}}
+</math>
+<math>
+\frac{b, s \,\longrightarrow\, \mathbf{true} \quad \quad I_1, s \,\longrightarrow\, \mathtt{Blad}}
+     {\mathbf{if}\, b \,\mathbf{then}\, I_1 \,\mathbf{else}\, I_2, s \,\longrightarrow\, \mathtt{Blad}}
+\quad \quad \quad
+\frac{b, s \,\longrightarrow\, \mathbf{false} \quad \quad I_2, s \,\longrightarrow\, \mathtt{Blad}}
+     {\mathbf{if}\, b \,\mathbf{then}\, I_1 \,\mathbf{else}\, I_2, s \,\longrightarrow\, \mathtt{Blad}}
+</math>
+<math>
+\frac{b, s \,\longrightarrow\, \mathbf{true} \quad \quad I, s \,\longrightarrow\, \mathtt{Blad}}
+     {\mathbf{while}\, b \,\mathbf{do}\, I, s \,\longrightarrow\, \mathtt{Blad}}
+\quad \quad
+\frac{b, s \,\longrightarrow\, \mathbf{true} \quad \quad I, s \,\longrightarrow\, s' \quad \quad
+       \mathbf{while}\, b \,\mathbf{do}\, I, s' \,\longrightarrow\, \mathtt{Blad}}
+     {\mathbf{while}\, b \,\mathbf{do}\, I, s \,\longrightarrow\, \mathtt{Blad}}
+</math>
+Zwróćmy szczególnie uwagę na ostatnią regułę dla pętli <math>\mathbf{while}\ </math>,: wyraża ona przypadek, gdy błąd został wygenerowany nie w pierwszym obiegu pętli, ale w którymś z kolejnych.
+Musieliśmy rozważyc również ten przypadek, ponieważ wybraliśmy podejście dużych kroków; w podejściu małych kroków nie byłoby to zapewne konieczne.
+</div></div>
+{{cwiczenie|3|cw3|
+Rozszerzmy język TINY o następującą instrukcję pętli:
+<math>
+I \, ::= \,\,
+       \mathbf{loop}\, I \,\,|\,\,
+       \mathbf{exit} \,\,|\,\,
+       \mathbf{continue}
+</math>
+<math>\mathbf{loop}\, I</math> to instrukcja pętli, <math>I</math> stanowi instrukcję wewnętrzną.
+Instrukcja <math>\mathbf{exit}</math> wychodzi z nabliższej otaczającej pętli <math>\mathbf{loop}\ </math>, i kontynuuje wykonanie programu od pierwszej instrukcji za tą pętlą.
+Instrukcja <math>\mathbf{continue}</math> powraca na początek instrukcji wewnętrznej najbliższej otaczającej pętli <math>\mathbf{loop}\ </math>,.
+Pozważ zarówno semantykę naturalną, jak i semantykę małych kroków.
+}}
+<div class="mw-collapsible mw-made=collapsible mw-collapsed">
+<span class="mw-collapsible-toogle mw-collapsible-toogle-default style="font-variant:small-caps">Rozwiązanie</span>
+<div class="mw-collapsible-content" style="display:none">
+Dodamy do reguł semantyki naturalnej dla języka TINY kilka nowych reguł opisujących nową konstrukcję języka i jej "interakcję" z pozostałymi konstrukcjami.
+Pomysł polega na dodaniu specjalnych konfiguracji zawierających informację o tym, że została wykonana instrukcja <math>\mathbf{exit}</math> lub <math>\mathbf{continue}</math>. Oto odpowiednie reguły:
+<math>
+\mathbf{exit}, s \,\longrightarrow\, s, \mbox{było-}\mathbf{exit}
+\quad \quad
+\mathbf{continue}, s \,\longrightarrow\, s, \mbox{było-}\mathbf{continue}</math>
+Czyli instrukcje <math>\mathbf{exit}</math> i <math>\mathbf{continue}</math> nie modyfikują stanu <math>s</math>, ale zostawiają po sobie "ślad".
+Zauważmy, że taki ślad zostaje pozostawiony tylko wtedy, jeśli nie było dotychczas innego śladu, to znaczy jeśli <math>\mathbf{exit}</math> (lub <math>\mathbf{continue}</math>) zostało wykonane w zwykłym stanie <math>s</math>.
+Oczywiście poszerzamy odpowiednio zbiór konfiguracji o:
+<math>
+\mathbf{State} \times \{ \mbox{było-}\mathbf{exit}, \mbox{było-}\mathbf{continue} \}</math>
+'''Pytanie''': jakie powinno być zachowanie <math>\mathbf{exit}</math> i <math>\mathbf{continue}</math> w konfiguracji <math>s, \mbox{było-}\mathbf{exit}</math> lub <math>s, \mbox{było-}\mathbf{continue}</math>?
+Czy instrukcje <math>\mathbf{exit}</math> i <math>\mathbf{continue}</math> będą faktycznie wykonywane w takich konfiguracjach?
+Zapiszmy teraz, jak inne instrukcje korzystają z dodatkowej informacji (śladu) zawartej w konfiguracjach.
+Oczywiście "beneficjentem" korzystającym z tej informacji jest instrukcja <math>\mathbf{loop}\ </math>,:
+<math>
+\frac{I, s \,\longrightarrow\, s', \mbox{było-}\mathbf{exit}}
+     {\mathbf{loop}\, I, s \,\longrightarrow\, s'}
+\quad \quad
+\frac{I, s \,\longrightarrow\, s', \mbox{było-}\mathbf{continue} \quad \quad \mathbf{loop}\, I, s' \,\longrightarrow\, s''}
+     {\mathbf{loop}\, I, s \,\longrightarrow\, s''}
+</math>
+Czyli w zależności od tego, jaki ślad został zarejestrowany podczas wykonania <math>I</math>, albo kończymy wykonanie  pętli <math>\mathbf{loop}\ </math>,, albo rozpoczynamy kolejną iterację.
+Zauważmy, że stan <math>s'</math> może być różny od <math>s</math>, ponieważ zanim wykonała się ktoraś z instrukcji <math>\mathbf{exit}</math> lub
+<math>\mathbf{continue}</math> mogły zostać zmienione wartości niektórych zmiennych.
+Oczywiście, jeśli instrukcja wewnętrzna <math>I</math> zakończyła się "normalnie", kontynuujemy wykonanie pętli podobnie jak w przypadku wywołania <math>\mathbf{continue}</math>:
+<math>
+\frac{I, s \,\longrightarrow\, s' \quad \quad \mathbf{loop}\, I, s' \,\longrightarrow\, s''}
+     {\mathbf{loop}\, I, s \,\longrightarrow\, s''}
+</math>
+'''Pytanie:''' czy potrzebujemy dodatkowo reguł postaci:
+<math>
+\frac{I, s \,\longrightarrow\, s' \quad \quad \mathbf{loop}\, I, s' \,\longrightarrow\, s'', \mbox{było-}\mathbf{exit}}
+     {\mathbf{loop}\, I, s \,\longrightarrow\, s'', \mbox{było-}\mathbf{exit}}
+\quad \quad
+\frac{I, s \,\longrightarrow\, s', \mbox{było-}\mathbf{continue} \quad \quad \mathbf{loop}\, I, s' \,\longrightarrow\, s'', \mbox{było-}\mathbf{exit}}
+     {\mathbf{loop}\, I, s \,\longrightarrow\, s'', \mbox{było-}\mathbf{exit}}
+</math>
+Okazuje się że nie, ponieważ ślad powinien zostać zawsze "wymazany" przez pętlę <math>\mathbf{loop}\ </math>,.
+Teraz musimy określić zachowanie wszystkich instrukcji w sytuacji, gdy bieżąca konfiguracja zawiera już ślad. Zasadniczo, powinniśmy zaniechać wykonania instrukcji (w przypadku pętli, powinniśmy zaniechać dalszego iterowania tej pętli).
+Oto odpowiednie reguły dla <math>\mbox{było-}\mathbf{exit}</math>:
+<math>
+\frac{I_1, s \,\longrightarrow\, s', \mbox{było-}\mathbf{exit}}
+     {I_1;\, I_2, s \,\longrightarrow\, s', \mbox{było-}\mathbf{exit}}
+\quad \quad
+\frac{I_1, s \,\longrightarrow\, s' \quad \quad I_2, s' \,\longrightarrow\, s'', \mbox{było-}\mathbf{exit}}
+     {I_1;\, I_2, s \,\longrightarrow\, s'', \mbox{było-}\mathbf{exit}}
+</math>
+<math>
+\frac{b, s \,\longrightarrow\, \mathbf{true} \quad \quad I_1, s \,\longrightarrow\, s', \mbox{było-}\mathbf{exit}}
+     {\mathbf{if}\, b \,\mathbf{then}\, I_1 \,\mathbf{else}\, I_2, s \,\longrightarrow\, s', \mbox{było-}\mathbf{exit}}
+\quad \quad
+\frac{b, s \,\longrightarrow\, \mathbf{false} \quad \quad I_2, s \,\longrightarrow\, s', \mbox{było-}\mathbf{exit}}
+     {\mathbf{if}\, b \,\mathbf{then}\, I_1 \,\mathbf{else}\, I_2, s \,\longrightarrow\, s', \mbox{było-}\mathbf{exit}}
+</math>
+<math>
+\frac{b, s \,\longrightarrow\, \mathbf{true} \quad \quad I, s \,\longrightarrow\, s', \mbox{było-}\mathbf{exit}}
+     {\mathbf{while}\, b \,\mathbf{do}\, I, s \,\longrightarrow\, s', \mbox{było-}\mathbf{exit}}
+\quad \quad
+\frac{b, s \,\longrightarrow\, \mathbf{true} \quad \quad I, s \,\longrightarrow\, s' \quad \quad
+       \mathbf{while}\, b \,\mathbf{do}\, I, s' \,\longrightarrow\, s'', \mbox{było-}\mathbf{exit}}
+     {\mathbf{while}\, b \,\mathbf{do}\, I, s \,\longrightarrow\, s', \mbox{było-}\mathbf{exit}}
+</math>
+Pominęliśmy zupełnie analogiczne reguły dla <math>\mbox{było-}\mathbf{continue}</math>.
+Zauważmy, że dla pętli <math>\mathbf{while}\ </math>, nie rozpatrujemy przypadku, gdy dozór <math>b</math> oblicza się do <math>\mathbf{false}</math>, gdyż w tym przypadku nie ma możliwości wygenerowania śladu.
+Zauważmy też, że nasze reguły nie pozwalają na dodanie drugiego (kolejnego) śladu!
+</div></div>
+<div class="mw-collapsible mw-made=collapsible mw-collapsed">
+<span class="mw-collapsible-toogle mw-collapsible-toogle-default style="font-variant:small-caps">Rozwiązanie</span>
+<div class="mw-collapsible-content" style="display:none">
+W semantyce naturalnej musieliśmy napisać wiele reguł, aby zapewnić pomijanie instrukcji w sytuacji, gdy został juz zarejestrowany jakiś ślad. Było to dość uciążliwe.
+Okazuje się, że podejście mało-krokowe oferuje możliwość bardziej eleganckiego rozwiązania.
+Punktem startowym sę teraz reguły mało-krokowe dla języka TINY.
+Podobnie jak poprzednio, rozszerzymy zbiór konfiguracji i podobnie opiszemy, jak powstaje ślad:
+<math>
+\mathbf{exit}, s \,\Longrightarrow, s, \mbox{było-}\mathbf{exit}
+\quad \quad
+\mathbf{continue}, s \,\Longrightarrow, s, \mbox{było-}\mathbf{continue}</math>
+Ponadto musimy określić sposób, w jaki mały krok mniejszej instrukcji zostaje zamieniony na mały krok większej. Np.
+<math>
+\frac{I_1, s \,\Longrightarrow, s', \mbox{było-}\mathbf{exit}}
+     {I_1;\, I_2, s \,\Longrightarrow, s', \mbox{było-}\mathbf{exit}}
+\quad \quad
+\mbox{ i analogicznie dla } \mbox{było-}\mathbf{continue}</math>
+Nie musimy zajmowac się przypadkiem, gdy ślad powstaje w <math>I_2</math>, bo wybraliśmy podejście małokrokowe.
+Ponadto, nie musimy opisywać instrukcji warunkowej i pętli <math>\mathbf{while}\ </math>,, ponieważ ślad nie może powstać podczas obliczania dozoru!
+Wreszcie zobaczmy jak zachowuje się pętla <math>\mathbf{loop}\ </math>,:
+<math>
+\frac{I, s \,\Longrightarrow, s', \mbox{było-}\mathbf{exit}}
+     {\mathbf{loop}\, I, s \,\Longrightarrow, s'}
+\quad \quad
+\frac{I, s \,\Longrightarrow, s', \mbox{było-}\mathbf{continue}}
+     {\mathbf{loop}\, I, s \,\Longrightarrow, \mathbf{loop}\, I, s'}
+</math>
+Reguły te są prawie identyczne z regułami semantyki naturalnej dla tej sytuacji!
+Natomiast korzystamy z tego, że w podejściu małokrokowym zmiana konfiguracji na <math>s', \mbox{było-}\mathbf{exit}</math> czy <math>s', \mbox{było-}\mathbf{continue}</math> jest ''natychmiast'' widoczna w instrukcji <math>\mathbf{loop}\, I</math>, nawet jeśli <math>\mathbf{exit}</math> czy <math>\mathbf{continue}</math> zostało wywołane głęboko wewnątrz <math>I</math>!
+Niestety powyższe reguły '''nie są poprawne'''!
+Dlaczego? Jak zwykle w semantyce małych kroków, wykonując instrukcję wewnętrzną "zapominamy" stopniowo, jaka była ona na początku.
+W związku z tym nie potrafimy poprawnie powrócić do wykonywania pętli <math>\mathbf{loop}\ </math>, po wywołaniu <math>\mathbf{continue}</math>.
+Prostym sposobem poprawienia naszego błędu jest rozszerzenie składni tak, aby możliwe było jednorazowe rozwinięcie pętli <math>\mathbf{loop}\ </math>,:
+<math>
+\mathbf{loop}\, I, s \,\Longrightarrow, I \,\mathbf{then}\, \mathbf{loop}\, I, s</math>
+Teraz możemy zapisać dwie powyższe reguły dla <math>\mathbf{loop}\ </math>, w poprawnej wersji, pamiętając o tym, że <math>\mbox{było-}\mathbf{exit}</math> i <math>\mbox{było-}\mathbf{continue}</math> pojawią się nie w instrukcji wewnętrznej, ale w jej ''kopii'' umieszczonej przed <math>\,\mathbf{then}\ </math>,:
+<math>
+\frac{I', s \,\Longrightarrow, s', \mbox{było-}\mathbf{exit}}
+     {I' \,\mathbf{then}\, \mathbf{loop}\, I, s \,\Longrightarrow, s'}
+\quad \quad
+\frac{I', s \,\Longrightarrow, s', \mbox{było-}\mathbf{continue}}
+     {I' \,\mathbf{then}\, \mathbf{loop}\, I, s \,\Longrightarrow, \mathbf{loop}\, I, s'}
+\quad \quad
+\frac{I', s \,\Longrightarrow, s'}
+     {I' \,\mathbf{then}\, \mathbf{loop}\, I, s \,\Longrightarrow, \mathbf{loop}\, I, s'}
+</math>
+Potrzebujemy też dodatkowej reguły dla obliczeń wewnątrz instrukcji stojącej przed <math>\,\mathbf{then}\ </math>, (w szczególności może ona zawierać zagnieżdzone pętle <math>\mathbf{loop}\ </math>,):
+<math>
+\frac{I', s \,\Longrightarrow, I'', s'}
+     {I' \,\mathbf{then}\, \mathbf{loop}\, I, s \,\Longrightarrow, I'' \,\mathbf{then}\, \mathbf{loop}\, I, s'}
+</math>
+Na koniec zauważmy, że stan <math>s'</math> w pierwszych dwóch z powyższych reguł nigdy nie jest różny od <math>s</math>. Zatem równoważnie moglibyśmy zamienić <math>s'</math> na <math>s</math> w powyższych dwóch regułach. Ale wtedy okazuje się, <math>s</math> w parze z <math>\mbox{było-}\mathbf{exit}</math> albo <math>\mbox{było-}\mathbf{continue}</math> jest nadmiarowe i może zostać wyeliminowane.
+Zatem ostatecznie nasze reguły mogą wyglądać tak:
+<math>
+\mathbf{exit}, s \,\Longrightarrow, \mbox{było-}\mathbf{exit}
+\quad \quad
+\mathbf{continue}, s \,\Longrightarrow, \mbox{było-}\mathbf{continue}
+</math>
+<math>
+\frac{I_1, s \,\Longrightarrow, \mbox{było-}\mathbf{exit}}
+     {I_1;\, I_2, s \,\Longrightarrow, \mbox{było-}\mathbf{exit}}
+\quad \quad
+\frac{I_1, s \,\Longrightarrow, \mbox{było-}\mathbf{continue}}
+     {I_1;\, I_2, s \,\Longrightarrow, \mbox{było-}\mathbf{continue}}
+</math>
+<math>
+\mathbf{loop}\, I, s \,\Longrightarrow, I \,\mathbf{then}\, \mathbf{loop}\, I, s</math>
+<math>
+\frac{I', s \,\Longrightarrow, \mbox{było-}\mathbf{exit}}
+     {I' \,\mathbf{then}\, \mathbf{loop}\, I, s \,\Longrightarrow, s}
+\quad \quad
+\frac{I', s \,\Longrightarrow, \mbox{było-}\mathbf{continue}}
+     {I' \,\mathbf{then}\, \mathbf{loop}\, I, s \,\Longrightarrow, \mathbf{loop}\, I, s}
+\quad \quad
+\frac{I', s \,\Longrightarrow, s'}
+     {I' \,\mathbf{then}\, \mathbf{loop}\, I, s \,\Longrightarrow, \mathbf{loop}\, I, s}
+</math>
+<math>
+\frac{I', s \,\Longrightarrow, I'', s'}
+     {I' \,\mathbf{then}\, \mathbf{loop}\, I, s \,\Longrightarrow, I'' \,\mathbf{then}\, \mathbf{loop}\, I, s'}
+</math>
+a zbiór konfiguracji poszerzamy tylko o dwie nowe konfiguracje <math>\{ \mbox{było-}\mathbf{exit}, \mbox{było-}\mathbf{continue} \}</math>.
+</div></div>
+== Zadania domowe ==
+{{cwiczenie|1|cw1.dom|
+Zaproponuj semantykę małokrokową dla rozszerzeń języka Tiny, które
+studiowaliśmy powyżej.
+}}
+{{cwiczenie|2|cw2.dom|
+Napisz semantykę naturalną dla nieznacznie rozszerzonej wersji instrukcji <math>\mathbf{loop}\ </math>,:
+<math>
+I \, ::= \,\,
+       x: \mathbf{loop}\, I \,\,|\,\,
+       \mathbf{exit}\, x \,\,|\,\,
+       \mathbf{continue}\, x
 </math>
-(nazwijmy ją ''składnią ograniczoną'') to powyższe reguły byłyby niepoprawne.
+Identyfikator <math>x</math> pełni tutaj rolę etykiety związanej z instrukcją <math>\mathbf{loop}\ </math>,, jest też parametrem dwóch pozostałych instrukcji.
+<math>\mathbf{exit} x</math> kończy teraz najbliższą otaczającą pętlę <math>\mathbf{loop}\ </math>, o etykiecie <math>x</math>. Podobnie <math>\mathbf{continue} x</math> wznawia najbliższą otaczającą pętlę o etykiecie <math>x</math>.
+}}
+{{przyklad|||
+}}
+Program
+ x: <math>\mathbf{loop}\ </math>,
+   a := 1;
+   y: <math>\mathbf{loop}\ </math>,
+     <math>\mathbf{exit}</math> x;
+     a := a-10;
+   a := a+1;
+ a := a+2;
+kończy działanie z wartością zmiennej <math>a = 3</math>.
+Za pomocą wcięć określiliśmy, do wnętrza której pętli <math>\mathbf{loop}\ </math>, należy każda z trzech ostatnich instrukcji przypisania.
+Niejednoznaczność bierze się oczywiście stąd, że pracujemy ze składnią abstrakcyjną. Składnia konkretna zawierałaby prawdopodobnie jakąś konstukcję "zamykającą" pętlę <math>\mathbf{loop}\ </math>,, np. <math>\mathbf{loop}\, I \,\mathbf{end}\mathbf{loop}\ </math>,.
-Zanim dopiszemy pozostałe reguły, określmy zbiór konfiguracji jako
-zbiór wyrażeń. Konfiguracje końcowe to wyrażenia bez operatora dodawania
-(liczby binarne). Nasz pomysł jest taki, że tranzycje stopniowo przesuwają
-operator dodawania w lewo, aż się go ostatecznie <pre>''pozbędą''</pre>.
+{{cwiczenie|3|cw3.dom|
-....
+Napisz semantykę naturalną i małokrokową dla rozszerzenia
+języka TINY o wyrażenia z efektami ubocznymi:
+<math>
+e \,  ::= \,\,
+        \ldots  \,\,|\,\,
+        \,\mathbf{do}\, I \,\mathbf{then}\, e  \,\,|\,\,
+        x := e  \,\,|\,\,
+        x++  \,\,|\,\,   \ldots
+</math>
-==== Zadanie 2 ====
+Obliczenie wyrażenia <math>\,\mathbf{do}\, I \,\mathbf{then}\, e</math> polega na wykonaniu <math>I</math> a potem na obliczeniu <math>e</math>.
+Wartość wyrażenia <math>x:= e</math> jest taka, jak wartość wyrażenia <math>e</math> a efektem ubocznym jest podstawienie tej wartości na zmienną <math>x</math>.
+}}