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ść ==
 Kończymy semantykę małych kroków i rozpoczynamy semantykę naturalną (duże kroki).
-Uzupełnimy semantykę naturalną języka Tiny o semantykę naturalną dla
+Uzupełnimy semantykę naturalną języka TINY o semantykę naturalną wyrażeń boolowskich i arytmetycznych oraz semantykę błędów wykonania.
-wyrażeń boolowskich i arytmetycznych i semantykę dla
+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>).
-błędów wykonania.
-Wreszcie dodamy instrukcję pętli <math> \mathbf{loop}\, </math> i instrukcje
-niestrukturalnego zakończenia pętli (instrukcje <math> \mathbf{exit}</math> i <math> \mathbf{continue} </math>).
@@ Linia 14: / Linia 10: @@
-==== Zadanie 1 ====
+{{cwiczenie|1|cw1|
-Zdefiniuj znaczenie wyrażeń boolowskich i arytmetycznych
+Zdefiniuj znaczenie wyrażeń boolowskich i arytmetycznych w języku TINY w stylu dużych kroków (semantyka naturalna).
-w języku Tiny, w stylu dużych kroków (semantyka naturalna).
+}}
-==== Rozwiązanie ====
+<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
+Przypomnijmy składnię wyrażeń boolowskich i arytmetycznych języka TINY:
-jezyka Tiny:
 <math>
@@ Linia 37: / Linia 34: @@
 l \, ::= \,\,
          \mathbf{true}    \,\,|\,\,
-         \mathbf{true}
+         \mathbf{false}
 </math>
@@ Linia 55: / Linia 52: @@
 </math>
-Chcemy, aby tranzycje wyrażen wyglądały następująco:
+Chcemy, aby tranzycje wyrażeń wyglądały następująco:
 <math>
 e, s \longrightarrow n
 \quad \quad \quad
-b, s \longrightarrow l,
+b, s \longrightarrow l</math>,
-</math>
-gdzie <math> s \in \mathbf{State} </math>, <math> n \in </math> jest liczbą całkowitą,
+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>.
-<math> n \in \mathbf{Num} </math>, a <math> l \in \mathbf{Bool} = \{ \mathbf{true}, \mathbf{true} \} </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>.
-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
@@ Linia 74: / Linia 67: @@
 \mathbf{Num} \, \cup \, \mathbf{Bool} \, \cup \, \mathbf{State}
 </math>
-a konfiguracje końcowe to <math> \mathbf{State} </math> tak jak poprzednio.
+a konfiguracje końcowe to <math>\mathbf{State}</math> tak jak poprzednio.
-Tranzycje dla instrukcji pozostają zasadniczo bez zmian, z tym,
+Tranzycje dla instrukcji pozostają zasadniczo bez zmian, z tym że odwołania do funkcji semantycznych dla wyrażen zastępujemy przez odpowiednie tranzycje.
-ż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:
@@ Linia 86: / Linia 77: @@
 <math>
-\frac{b, s \,\longrightarrow\, \mathbf{true}}
+\frac{b, s \,\longrightarrow\, \mathbf{false}}
       {\mathbf{while}\, b \,\mathbf{do}\, I, s \,\longrightarrow\, s}
 </math>
@@ Linia 92: / Linia 83: @@
 Podobnie dla instrukcji warunkowej.
 Teraz zajmiemy się tranzycjami dla wyrażeń.
-Zacznijmy od stalych arytmetycznych i boolowskich:
+Zacznijmy od stałych arytmetycznych i boolowskich:
 <math>
 n, s \,\longrightarrow\, n
 \quad \quad
-l, s \,\longrightarrow\, l.
+l, s \,\longrightarrow\, l</math>
-</math>
 Operatory arytmetyczne definiujemy następująco:
@@ Linia 109: / Linia 99: @@
 </math>
-Czyli aby obliczyć sumę <math> e_1 + e_2 </math> w stanie
+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.
-<math> s </math>, trzeba najpierw obliczyć <math> e_1 </math> i
+Zauważmy, że nie specyfikujemy kolejności, w jakiej mają się obliczać obydwa podwyrażenia.
-<math> e_2 </math> w tym stanie, a następnie dodać obliczone wartości.
+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ń.
-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
+Podobne reguły można napisać dla pozostałych operacji arytmetycznych, oraz dla spójników logicznych:
-arytmnetycznych, oraz dla spójników logicznych:
 <math>
@@ Linia 128: / Linia 112: @@
 </math>
-Oto inny wariant, reguły lewo-stronne (ponieważ rozpoczynamy od ''lewego'' koniunktu):
+(strategia gorliwa).
+Reguły dla <math>\leq</math> są następujące:
 <math>
-\frac{b_1, s \,\longrightarrow\, \mathbf{true}}
+\frac{e_1, s \,\longrightarrow\, n_1 \quad \quad e_2, s \,\longrightarrow\, n_2 \quad \quad n_1 \leq n_2}
-      {b_1 \land b_2, s \,\longrightarrow\, \mathbf{true}}
+     {e_1 \leq e_2, s \,\longrightarrow\, \mathbf{true}}
+\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>
+\frac{b_1, s \,\longrightarrow\, \mathbf{false}}
+     {b_1 \land b_2, s \,\longrightarrow\, \mathbf{false}}
+\quad \quad
 \frac{b_1, s \,\longrightarrow\, \mathbf{true}  \quad \quad
        b_2, s \,\longrightarrow\, l}
@@ Linia 139: / Linia 134: @@
 </math>
-Inny wariant to wariant prawo-stronny (
+Inny wariant to strategia prawostronna (najpierw <math>b_2</math>, potem <math>b_1</math>).
-najpierw <math> b_2 </math>, potem <math> b_1 </math>).
+Wreszcie rozważmy kombinację obydwu semantyk (strategia ''równoległa'' lub ''leniwa''):
-Wreszcie rozważmy kombinację obydwu semantyk (reguły ''równoległe''):
 <math>
-\frac{b_1, s \,\longrightarrow\, \mathbf{true}}
+\frac{b_1, s \,\longrightarrow\, \mathbf{false}}
-      {b_1 \land b_2, s \,\longrightarrow\, \mathbf{true}}
+      {b_1 \land b_2, s \,\longrightarrow\, \mathbf{false}}
 \quad \quad \quad
-\frac{b_2, s \,\longrightarrow\, \mathbf{true}}
+\frac{b_2, s \,\longrightarrow\, \mathbf{false}}
-       {b_1 \land b_2, s \,\longrightarrow\, \mathbf{true}}
+       {b_1 \land b_2, s \,\longrightarrow\, \mathbf{false}}
 </math>
-Czyli jeśli którekolwiek z podwyrażeń daje wynik <math> \mathbf{true} </math>,
+Czyli jeśli którekolwiek z podwyrażeń daje wynik <math>\mathbf{false}</math>, to taki wynik zyskuje całe wyrażenie.
-to taki wynik zyskuje całe wyrażenie.
 Dodatkowo potrzebujemy jeszcze reguły:
@@ Linia 161: / Linia 154: @@
 </math>
-W naszym prostym języku wszystkie cztery warianty
+'''Pytanie:''' czy w naszym prostym języku wszystkie cztery strategie obliczania spójnika <math>\land</math> są równoważne?
-są równoważne.
-Reguły dla pozostałych spójników logicznych, dla
+Reguły dla negacji oraz dla instrukcji przypisania pozostawiamy jako proste ćwiczenie.
-negacji oraz dla instrukcji przypisania pozostawiamy jako proste
-ćwiczenie.
+</div></div>
-==== Zadanie 2 ====
+{{cwiczenie|2|cw2|
 Rozważ dodatkowo operację dzielenia:
@@ Linia 180: / Linia 172: @@
 i rozszerz semantykę z poprzedniego zadania.
-Dzielenie przez zero jest błądem i  kończy natychmiast wykonanie
+Dzielenie przez zero jest błędem i kończy natychmiast wykonanie programu.
-programu.
+Oprócz stanu wynikiem programu powinna byc informacja o błędzie, jeśli błąd wystąpił.
-Oprócz stanu wynikiem programu powinna byc informacja o błędzie,
+}}
-jeśli błąd wystąpił.
-==== Rozwiązanie (szkic) ====
+<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
+powinna być identyczna jak w poprzednim zadaniu. Zatem pozostawiamy wszystkie reguły z poprzedniego zadania.
-wszystkie reguły z poprzedniego zadania.
 Dodatkowo potrzebujemy reguł, które opiszą
@@ Linia 198: / Linia 189: @@
 Zaczynamy od pierwszego punktu.
-W tym celu dodajemy do konfiguracji jedną konfigurację końcową
+W tym celu dodajemy do konfiguracji jedną konfigurację końcową <math>\mathtt{Blad}</math>.
-<math> \mathtt{Blad} </math>.
+Reguła opisująca powstanie błędu może wyglądać np. tak (duże i małe kroki):
-Reguła opisująca powstanie błędu może wyglądać np. tak:
 <math>
-\frac{e_2, s \longrightarrow 0}
+\frac{e_2, s \,\longrightarrow\, 0}
-{e_1 / e_2, s \longrightarrow Blad}
+{e_1 / e_2, s \,\longrightarrow\, \mathtt{Blad}}
-</math>
+\quad \quad
+e_1 / 0, s \,\Longrightarrow, \mathtt{Blad}</math>
-Pomijamy tutaj reguły dla przypadku, gdy <math>e_2</math>
+Pomijamy tutaj reguły dla przypadku, gdy <math>e_2</math> oblicza się do wartości różnej od zera.
-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.
-Ponadto dla czytelności przyjęliśmy, że wynikiem tranzycji jest
+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ł.
-wyłącznie informacja o błędzie, a stan jest zapominany.
+Np. ostatnia reguła wyglądałaby następująco:
-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>
-e_1 / 0, s \Longrightarrow Blad, s
+\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
+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>.
-oczywiście całego zbioru <math> \{ \mathtt{Blad} \} \times \mathbf{State} </math>.
-Przejdźmy teraz do drugiego punktu. Potrzebujemy dodatkowych reguł,
+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.
-które zagwarantują, że błąd, raz pojawiwszy się, propaguje się przez
-wszystkie konstrukcje składniowe, a normalne obliczenie wyrażenia
-jest wstrzymame.
 <math>
@@ Linia 264: / Linia 250: @@
       {\mathbf{if}\, b \,\mathbf{then}\, I_1 \,\mathbf{else}\, I_2, s \,\longrightarrow\, \mathtt{Blad}}
 \quad \quad \quad
-\frac{b, s \,\longrightarrow\, \mathbf{true} \quad \quad I_2, s \,\longrightarrow\, \mathtt{Blad}}
+\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>
@@ Linia 277: / Linia 263: @@
 </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>
-==== Zadanie 3 ====
+{{cwiczenie|3|cw3|
-Rozszerz język Tiny o następującą instrukcję pętli:
+Rozszerzmy język TINY o następującą instrukcję pętli:
 <math>
@@ Linia 291: / Linia 281: @@
 </math>
-<math> \mathbf{loop}\, I </math> to instrukcja pętli, <math> I </math> stanowi instrukcję wewnętrzną.
+<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 pętli <math> \mathbf{loop}\, </math>
+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ą.
-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>,.
-Instrukcje <math> \mathbf{continue} </math> powraca na początek instrukcji wewnętrznej
-najbliższej pętli.
-Pozważ zarówno semantykę naturalną jak i semantykę małych kroków.
+Pozważ zarówno semantykę naturalną, jak i semantykę małych kroków.
+}}
-==== Rozwiązanie 1 (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">
-Dodamy do reguł semantyki naturalnej dla języka Tiny
+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.
-kilka nowych reguł opisujących nową konstrukcję języka
-i jej ''interakcję'' z pozostałymi konstrukcjami.
-Pomysł polega na dodaniu specjalnych konfiguracji zawierających
+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:
-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}.
+\mathbf{continue}, s \,\longrightarrow\, s, \mbox{było-}\mathbf{continue}</math>
-</math>
-Czyli instrukcje <math> \mathbf{exit} </math> i <math> \mathbf{continue} </math> nie modyfikują
+Czyli instrukcje <math>\mathbf{exit}</math> i <math>\mathbf{continue}</math> nie modyfikują stanu <math>s</math>, ale zostawiają po sobie "ślad".
-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>.
-Zauważmy, że taki ślad zostaje pozostawiony tylko wtedy, jesli
-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>[
+<math>
-\mathbf{State} \times \{ \mbox{było-}\mathbf{exit}, \mbox{było-}\mathbf{continue} \}
+\mathbf{State} \times \{ \mbox{było-}\mathbf{exit}, \mbox{było-}\mathbf{continue} \}</math>
-</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>?
-'''Pytanie''': jakie powinno być zachowanie <math> \mathbf{exit} </math> i
+Czy instrukcje <math>\mathbf{exit}</math> i <math>\mathbf{continue}</math> będą faktycznie wykonywane w takich konfiguracjach?
-<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
+Zapiszmy teraz, jak inne instrukcje korzystają z dodatkowej informacji (śladu) zawartej w konfiguracjach.
-(śladu) zawartej w konfiguracjach.
+Oczywiście "beneficjentem" korzystającym z tej informacji jest instrukcja <math>\mathbf{loop}\ </math>,:
-Oczywiście beneficjentem tej informacji jest instrukcji <math> \mathbf{loop}\, </math>:
 <math>
@@ Linia 347: / Linia 325: @@
 </math>
-Czyli w zależności od tego, jaki ślad został zarejestrowany
+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ę.
-podczas wykonania <math> I </math>, albo kończymy wykonanie  pętli <math> \mathbf{loop}\, </math>,
+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
-albo rozpoczynamy kolejną iterację.
+<math>\mathbf{continue}</math> mogły zostać zmienione wartości niektórych zmiennych.
-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ę
+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>:
-''normalnie'', kontynuujemy wykonanie pętli podobnie jak w przypadku
-wywołania <math> \mathbf{continue} </math>:
 <math>
@@ Linia 373: / Linia 346: @@
 </math>
-Okazuje się że nie, ponieważ ślad powinien zostać zawsze
+Okazuje się że nie, ponieważ ślad powinien zostać zawsze "wymazany" przez pętlę <math>\mathbf{loop}\ </math>,.
-''wymazany'' przez pętlę <math> \mathbf{loop}\, </math>.
-Poza tym reguły te wykraczałyby poza klasyczna podejście semantyki
-naturalnej, w którym zwykle bezpośrednio definiujemy
-tranzycje postaci <math> I, s \,\longrightarrow\, s' </math>.
-Teraz musimy określić zachowanie wszystkich instrukcji w sytuacji,
+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).
-gdy bieżąca konfiguracja zawiera już ślad. Zasadniczo, powinniśmy
+Oto odpowiednie reguły dla <math>\mbox{było-}\mathbf{exit}</math>:
-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>
@@ Linia 397: / Linia 363: @@
       {\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{true} \quad \quad I_2, s \,\longrightarrow\, s', \mbox{było-}\mathbf{exit}}
+\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>
@@ Linia 410: / Linia 376: @@
 </math>
-Pominęliśmy zupełnie analogiczne reguły dla konfiguracji
+Pominęliśmy zupełnie analogiczne reguły dla <math>\mbox{było-}\mathbf{continue}</math>.
-<math> s', \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.
-Zwróćmy szczególnie uwagę na ostatnią regułę dla pętli <math> \mathbf{while}\, </math>:
-wyraża ona przypadek, gdy ślad <math> \mathbf{exit} </math> 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.
-Zauważmy też, że dla pętli <math> \mathbf{while}\, </math> nie rozpatrujemy przypadku,
-gdy dozór <math> b </math> oblicza się do <math> \mathbf{true} </math>, gdyż w tym przypadku
-nie ma możliwości wygenerowania śladu.
-Zauważmy, że nasze reguły nie pozwalają na dodanie drugiego (kolejnego) śladu!
+Zauważmy też, że nasze reguły nie pozwalają na dodanie drugiego (kolejnego) śladu!
+</div></div>
-==== Rozwiązanie 2 (małe kroki) ====
+<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
+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.
-zapewnić pomijanie instrukcji w sytuacji, gdy został juz
+Okazuje się, że podejście mało-krokowe oferuje możliwość bardziej eleganckiego rozwiązania.
-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.
+Punktem startowym sę teraz reguły mało-krokowe dla języka TINY.
-Podobnie jak poprzednio rozszerzymy zbiór konfiguracji i podobnie
+Podobnie jak poprzednio, rozszerzymy zbiór konfiguracji i podobnie opiszemy, jak powstaje ślad:
-opiszemy, jak powstaje ślad:
 <math>
-\mathbf{exit}, s \,\Longrightarrow\, s, \mbox{było-}\mathbf{exit}
+\mathbf{exit}, s \,\Longrightarrow, s, \mbox{było-}\mathbf{exit}
 \quad \quad
-\mathbf{continue}, s \,\Longrightarrow\, s, \mbox{było-}\mathbf{continue}.
+\mathbf{continue}, s \,\Longrightarrow, s, \mbox{było-}\mathbf{continue}</math>
-</math>
-Ponadto musimy określić sposób, w jaki mały krok
+Ponadto musimy określić sposób, w jaki mały krok mniejszej instrukcji zostaje zamieniony na mały krok większej. Np.
-mniejszej instrukcji zostaje zamieniony na mały krok
-większej. Np.
 <math>
-\frac{I_1, s \,\Longrightarrow\, s', \mbox{było-}\mathbf{exit}}
+\frac{I_1, s \,\Longrightarrow, s', \mbox{było-}\mathbf{exit}}
-      {I_1;\, I_2, 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}.
+\mbox{ i analogicznie dla } \mbox{było-}\mathbf{continue}</math>
-</math>
-Zauważmy, że nie musimy zajmowac się przypadkiem, gdy ślad
+Nie musimy zajmowac się przypadkiem, gdy ślad powstaje w <math>I_2</math>, bo wybraliśmy podejście małokrokowe.
-powstaje w <math> I_2 </math>, bo wybraliśmy podejście mało-krokowe.
+Ponadto, nie musimy opisywać instrukcji warunkowej i pętli <math>\mathbf{while}\ </math>,, ponieważ ślad nie może powstać podczas obliczania dozoru!
-Ponadto, nie musimy opisywać instrukcji warunkowej i pętli <math> \mathbf{while}\, </math>,
-ponieważ ślad nie może powstać podczas oblcizania dozoru!
-Wreszcie zobaczmy jak zachowuje się pętla <math> \mathbf{loop}\, </math>:
+Wreszcie zobaczmy jak zachowuje się pętla <math>\mathbf{loop}\ </math>,:
 <math>
-\frac{I, s \,\Longrightarrow\, s', \mbox{było-}\mathbf{exit}}
+\frac{I, s \,\Longrightarrow, s', \mbox{było-}\mathbf{exit}}
-      {\mathbf{loop}\, I, s \,\Longrightarrow\, s'}
+      {\mathbf{loop}\, I, s \,\Longrightarrow, s'}
 \quad \quad
-\frac{I, s \,\Longrightarrow\, s', \mbox{było-}\mathbf{continue}}
+\frac{I, s \,\Longrightarrow, s', \mbox{było-}\mathbf{continue}}
-      {\mathbf{loop}\, I, s \,\Longrightarrow\, \mathbf{loop}\, I, s'}
+      {\mathbf{loop}\, I, s \,\Longrightarrow, \mathbf{loop}\, I, s'}
 </math>
-Reguły te są prawie identyczne do reguł semantyki naturalnej dla tej
+Reguły te są prawie identyczne z regułami semantyki naturalnej dla tej sytuacji!
-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>!
-Natomiast korzystamy z tego, że w podejściu mało-krokowym 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, powyzsze reguły '''nie są poprawne'''!
+Niestety powyższe reguły '''nie są poprawne'''!
-Dlaczego? Jak zwykle w semantyce małych kroków, wykonując instrukcję
+Dlaczego? Jak zwykle w semantyce małych kroków, wykonując instrukcję wewnętrzną "zapominamy" stopniowo, jaka była ona na początku.
-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>.
-I 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 blędu jest rozszerzenie składni
+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>,:
-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.
+\mathbf{loop}\, I, s \,\Longrightarrow, I \,\mathbf{then}\, \mathbf{loop}\, I, s</math>
-</math>
-Teraz możemy zapisać dwie powyższe reguły dla <math> \mathbf{loop}\, </math> w poprawnej
+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>,:
-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}}
+\frac{I', s \,\Longrightarrow, s', \mbox{było-}\mathbf{exit}}
-      {I' \,\mathbf{then}\, \mathbf{loop}\, I, s \,\Longrightarrow\, s'}
+      {I' \,\mathbf{then}\, \mathbf{loop}\, I, s \,\Longrightarrow, s'}
 \quad \quad
-\frac{I', s \,\Longrightarrow\, s', \mbox{było-}\mathbf{continue}}
+\frac{I', s \,\Longrightarrow, s', \mbox{było-}\mathbf{continue}}
-      {I; \,\mathbf{then}\, \mathbf{loop}\, I, s \,\Longrightarrow\, \mathbf{loop}\, I, s'}
+      {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>
-A ponieważ wewnątrz kopii mogą być zagnieżdzone instrukcje
+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> \mathbf{loop}\, </math> potrzebujemy dodatkowej reguły:
 <math>
-\frac{I', s \,\Longrightarrow\, I'', s'}
+\frac{I', s \,\Longrightarrow, I'', s'}
-      {I' \,\mathbf{then}\, \mathbf{loop}\, I, s \,\Longrightarrow\, I'' \,\mathbf{then}\, \mathbf{loop}\, 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
+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.
-pierwszych dwóch z powyższych trzech 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}
+\mathbf{exit}, s \,\Longrightarrow, \mbox{było-}\mathbf{exit}
 \quad \quad
-\mathbf{continue}, s \,\Longrightarrow\, \mbox{było-}\mathbf{continue}
+\mathbf{continue}, s \,\Longrightarrow, \mbox{było-}\mathbf{continue}
 </math>
 <math>
-\frac{I_1, s \,\Longrightarrow\, \mbox{było-}\mathbf{exit}}
+\frac{I_1, s \,\Longrightarrow, \mbox{było-}\mathbf{exit}}
-      {I_1;\, I_2, 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}}
+\frac{I_1, s \,\Longrightarrow, \mbox{było-}\mathbf{continue}}
-      {I_1;\, I_2, 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.
+\mathbf{loop}\, I, s \,\Longrightarrow, I \,\mathbf{then}\, \mathbf{loop}\, I, s</math>
-</math>
 <math>
-\frac{I', s \,\Longrightarrow\, \mbox{było-}\mathbf{exit}}
+\frac{I', s \,\Longrightarrow, \mbox{było-}\mathbf{exit}}
-      {I' \,\mathbf{then}\, \mathbf{loop}\, I, s \,\Longrightarrow\, s}
+      {I' \,\mathbf{then}\, \mathbf{loop}\, I, s \,\Longrightarrow, s}
 \quad \quad
-\frac{I', s \,\Longrightarrow\, \mbox{było-}\mathbf{continue}}
+\frac{I', s \,\Longrightarrow, \mbox{było-}\mathbf{continue}}
-      {I; \,\mathbf{then}\, \mathbf{loop}\, I, s \,\Longrightarrow\, \mathbf{loop}\, I, s}
+      {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'}
+\frac{I', s \,\Longrightarrow, I'', s'}
-      {I' \,\mathbf{then}\, \mathbf{loop}\, I, s \,\Longrightarrow\, I'' \,\mathbf{then}\, \mathbf{loop}\, 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
+a zbiór konfiguracji poszerzamy tylko o dwie nowe konfiguracje <math>\{ \mbox{było-}\mathbf{exit}, \mbox{było-}\mathbf{continue} \}</math>.
-<math> \{ \mbox{było-}\mathbf{exit}, \mbox{było-}\mathbf{continue} \} </math>.
+</div></div>
 == Zadania domowe ==
-==== Zadanie 1 ====
+{{cwiczenie|1|cw1.dom|
-Zaproponuj semantykę mało-krokową języka z zdania 2.
+Zaproponuj semantykę małokrokową dla rozszerzeń języka Tiny, które
-Czy różni się ona istotnie od semantyki naturalnej?
+studiowaliśmy powyżej.
+}}
-==== Zadanie 2 ====
+{{cwiczenie|2|cw2.dom|
-Napisz semantyję naturalną dla nieznacznie rozszerzonej wersji instrukcji <math> \mathbf{loop}\, </math>:
+Napisz semantykę naturalną dla nieznacznie rozszerzonej wersji instrukcji <math>\mathbf{loop}\ </math>,:
 <math>
 I \, ::= \,\,
         x: \mathbf{loop}\, I \,\,|\,\,
-        \mathbf{exit} x \,\,|\,\,
+        \mathbf{exit}\, x \,\,|\,\,
-        \mathbf{continue} x
+        \mathbf{continue}\, x
 </math>
-Identyfikator <math> x </math> pełni tutaj rolę etykiety przypisanej
+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.
-instrukcji <math> \mathbf{loop}\, </math>, jest też parametrem dwóch pozostałych
+<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>.
-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ą
-pętlę o etykiecie <math> x </math>. Np. program
+{{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;
-  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>,.
-kończy działanie z wartością zmiennej <math> a = 3 </math>.
-Zauważmy, że musieliśmy jakoś określić, do wnętrza której pętli
-<math> \mathbf{loop}\, </math> należą trzy ostatnie instrukcje. Użyliśmy to tego celu
-wcięć a 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>.
-==== Zadanie 3 ====
+{{cwiczenie|3|cw3.dom|
-Napisz semantykę naturalną i mało-krokową dla rozszerzenia
+Napisz semantykę naturalną i małokrokową dla rozszerzenia
-języka Tiny o wyrażenia z efektami ubocznymi:
+języka TINY o wyrażenia z efektami ubocznymi:
 <math>
@@ Linia 621: / Linia 551: @@
 </math>
-Obliczenie wyrażenia <math> \,\mathbf{do}\, I \,\mathbf{then}\, e </math> polega na wykonaniu <math> I </math>
+Obliczenie wyrażenia <math>\,\mathbf{do}\, I \,\mathbf{then}\, e</math> polega na wykonaniu <math>I</math> a potem na obliczeniu <math>e</math>.
-a potem na obliczeniu <math> e </math>. Wartość wyrażenia <math> x:= e </math> jest taka
+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>.
-jak wartość wyrażenia <math> e </math> a efektem ubocznym jest
+}}
-podstawienie tej wartości na zmienną <math> x </math>.