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ść ==
-== 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 <math>\mathbf{loop}\ </math>,, pozwalającą na niestrukturalne przerwanie lub wznowienie iteracji (instrukcje <math>\mathbf{exit}</math> i <math>\mathbf{continue}</math>).
-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>).
+== Rozszerzenia semantyki języka Tiny ==
-== Rozszerzenia semantyki jêzyka Tiny ==
 {{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).
 }}
-{{rozwiazanie||roz1|
-<div class="mw-collapsible mw-made=collapsible mw-collapsed"><div class="mw-collapsible-content" style="display:none">
+<div class="mw-collapsible mw-made=collapsible mw-collapsed">
+<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 56: / Linia 52: @@
 </math>
-Chcemy, aby tranzycje wyra¿eñ 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{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>.
-Tranzycja taka oznacza, ¿e wyra¿enie <math>e</math> w stanie <math>s</math> wylicza siê do
+Zatem zbiór konfiguracji dla semantyki całego języka Tiny to znów
-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>
@@ Linia 75: / 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
+Np. dla instrukcji pętli będziemy mieć następujące reguły:
-przez odpowiednie tranzycje.
-Np. dla instrukcji pêtli bêdziemy mieæ nastêpuj±ce regu³y:
 <math>
@@ Linia 92: / Linia 82: @@
 Podobnie dla instrukcji warunkowej.
-Teraz zajmiemy siê tranzycjami dla wyra¿eñ.
+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:
+Operatory arytmetyczne definiujemy następująco:
 <math>
@@ Linia 110: / 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 129: / 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{e_1, s \,\longrightarrow\, n_1 \quad \quad e_2, s \,\longrightarrow\, n_2 \quad \quad n_1 \leq n_2}
+     {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>
@@ Linia 140: / 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>
@@ Linia 152: / Linia 145: @@
 </math>
-Czyli je¶li którekolwiek z podwyra¿eñ daje wynik <math>\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.
-to taki wynik zyskuje ca³e wyra¿enie.
+Dodatkowo potrzebujemy jeszcze reguły:
-Dodatkowo potrzebujemy jeszcze regu³y:
 <math>
@@ Linia 162: / 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>
-}}
 {{cwiczenie|2|cw2|
-Rozwa¿ dodatkowo operacjê dzielenia:
+Rozważ dodatkowo operację dzielenia:
 <math>
@@ Linia 181: / Linia 171: @@
 </math>
-i rozszerz semantykê z poprzedniego zadania.
+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³.
 }}
-{{rozwiazanie||roz2|
+<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 mw-made=collapsible mw-collapsed"><div class="mw-collapsible-content" style="display:none">
+<div class="mw-collapsible-content" style="display:none">
-Dopóki nie wyst±pi b³±d dzielenia przez zero, semantyka programu
+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ą
-Dodatkowo potrzebujemy regu³, które opisz±
-* kiedy powstaje b³±d oraz
+* kiedy powstaje błąd oraz
-* jak zachowuje siê program po wyst±pieniu b³êdu
+* jak zachowuje się program po wystąpieniu błędu
 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
-(du¿e i ma³e kroki):
 <math>
@@ Linia 211: / Linia 196: @@
 {e_1 / e_2, s \,\longrightarrow\, \mathtt{Blad}}
 \quad \quad
-e_1 / 0, s \,\Longrightarrow\, \mathtt{Blad}.
+e_1 / 0, s \,\Longrightarrow, \mathtt{Blad}</math>
-</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>
@@ Linia 227: / Linia 207: @@
 {e_1 / e_2, s \,\longrightarrow\, \mathtt{Blad}, s}
 \quad \quad
-e_1 / 0, s \,\Longrightarrow\, \mathtt{Blad}, s
+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 246: / Linia 222: @@
 </math>
-Nastêpnie, b³±d w wyra¿eniu powinien wstrzymaæ normalne wykonanie instrukcji:
+Następnie, błąd w wyrażeniu powinien wstrzymać normalne wykonanie instrukcji:
 <math>
@@ Linia 263: / Linia 239: @@
 </math>
-I wreszcie b³±d powinien propagowaæ siê do kolejnych instrukcji:
+I wreszcie błąd powinien propagować się do kolejnych instrukcji:
 <math>
@@ Linia 287: / Linia 263: @@
 </math>
-Zwróæmy szczególnie uwagê na ostatni± regu³ê dla pêtli <math>\mathbf{while}\,</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.
-wyra¿a ona przypadek, gdy b³±d zosta³ wygenerowany
+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.
-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:
+Rozszerzmy język TINY o następującą instrukcję pętli:
 <math>
@@ Linia 309: / 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 otaczaj±cej 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>,.
-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.
+Pozważ zarówno semantykę naturalną, jak i semantykę małych kroków.
 }}
-{{rozwiazanie|(semantyka naturalna)|roz3.1|
-<div class="mw-collapsible mw-made=collapsible mw-collapsed"><div class="mw-collapsible-content" style="display:none">
-Dodamy do regu³ semantyki naturalnej dla jêzyka Tiny
+<div class="mw-collapsible mw-made=collapsible mw-collapsed">
-kilka nowych regu³ opisuj±cych now± konstrukcjê jêzyka
+<span class="mw-collapsible-toogle mw-collapsible-toogle-default style="font-variant:small-caps">Rozwiązanie</span>
-i jej ,,interakcjê\'' z pozosta³ymi konstrukcjami.
+<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
+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}
+\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
+Oczywiście poszerzamy odpowiednio zbiór konfiguracji o:
-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} \}
+\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
+'''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>?
-<math>\mathbf{continue}</math> w konfiguracji <math>s, \mbox{by³o-}\mathbf{exit}</math>
+Czy instrukcje <math>\mathbf{exit}</math> i <math>\mathbf{continue}</math> będą faktycznie wykonywane w takich konfiguracjach?
-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>
-\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'}
 \quad \quad
-\frac{I, s \,\longrightarrow\, s', \mbox{by³o-}\mathbf{continue} \quad \quad \mathbf{loop}\, I, s' \,\longrightarrow\, s''}
+\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
+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 382: / Linia 336: @@
 </math>
-'''Pytanie:''' czy potrzebujemy dodatkowo regu³ postaci:
+'''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}}
+\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}}
+      {\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}}
+\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}}
+      {\mathbf{loop}\, I, s \,\longrightarrow\, s'', \mbox{było-}\mathbf{exit}}
 </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>
-\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
-\frac{I_1, s \,\longrightarrow\, s' \quad \quad I_2, s' \,\longrightarrow\, s'', \mbox{by³o-}\mathbf{exit}}
+\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}}
+      {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}}
+\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}}
+      {\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}}
+\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}}
+      {\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}}
+\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}}
+      {\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}}
-      {\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>.
+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,
+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.
-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, ¿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>
-}}
-{{rozwiazanie|(ma³e kroki)|roz3.2|
-<div class="mw-collapsible mw-made=collapsible mw-collapsed"><div class="mw-collapsible-content" style="display:none">
+<div class="mw-collapsible mw-made=collapsible mw-collapsed">
+<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>
-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 obliczania 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 powy¿sze 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'}
+\frac{I', s \,\Longrightarrow, s'}
-      {I; \,\mathbf{then}\, \mathbf{loop}\, I, s \,\Longrightarrow\, \mathbf{loop}\, I, s'}
+      {I' \,\mathbf{then}\, \mathbf{loop}\, I, s \,\Longrightarrow, \mathbf{loop}\, I, s'}
 </math>
-Potrzebujemy te¿ dodatkowej regu³y dla obliczeñ wewn±trz instrukcji
+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>,):
-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'}
+\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 regu³ nigdy nie jest ró¿ny
+Zatem ostatecznie nasze reguły mogą wyglądać tak:
-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'}
+\frac{I', s \,\Longrightarrow, s'}
-      {I; \,\mathbf{then}\, \mathbf{loop}\, I, s \,\Longrightarrow\, \mathbf{loop}\, I, 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 dwie nowe konfiguracje
+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 ==
@@ Linia 591: / Linia 499: @@
 {{cwiczenie|1|cw1.dom|
-Zaproponuj semantykê ma³o-krokow± dla rozszerzeñ jêzyka Tiny, które
+Zaproponuj semantykę małokrokową dla rozszerzeń języka Tiny, które
-studiowali¶my powy¿ej.
+studiowaliśmy powyżej.
 }}
@@ Linia 598: / Linia 506: @@
 {{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>
@@ Linia 607: / Linia 515: @@
 </math>
-Identyfikator <math>x</math> pe³ni tutaj rolê etykiety zwi±zanej z
+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.
-instrukcj± <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±
-otaczaj±c± pêtlê o etykiecie <math>x</math>.
 {{przyklad|||
+}}
 Program
-  x: <math>\mathbf{loop}\,</math>
+  x: <math>\mathbf{loop}\ </math>,
     a := 1;
-    y: <math>\mathbf{loop}\,</math>
+    y: <math>\mathbf{loop}\ </math>,
       <math>\mathbf{exit}</math> x;
       a := a-10;
@@ Linia 625: / Linia 531: @@
   a := a+2;
-}}
-koñczy dzia³anie z warto¶ci± zmiennej <math>a = 3</math>.
+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
+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.
-<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>,.
-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>.
-}}
 {{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 650: / 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>.
 }}