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ą wyrażeń boolowskich i arytmetycznych oraz semantykę błędów wykonania.
+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>).
+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>).
@@ Linia 13: / Linia 12: @@
 {{cwiczenie|1|cw1|
-Zdefiniuj znaczenie wyrażeń boolowskich i arytmetycznych w języku Tiny, w stylu dużych kroków (semantyka naturalna).
+Zdefiniuj znaczenie wyrażeń boolowskich i arytmetycznych 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 jezyka Tiny:
+Przypomnijmy składnię wyrażeń boolowskich i arytmetycznych języka TINY:
 <math>
@@ Linia 57: / Linia 57: @@
 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ą, <math>n \in \mathbf{Num}</math>, a <math>l \in \mathbf{Bool} = \{ \mathbf{true}, \mathbf{false} \}</math>.
@@ Linia 69: / Linia 68: @@
 </math>
 a konfiguracje końcowe to <math>\mathbf{State}</math> tak jak poprzednio.
-Tranzycje dla instrukcji pozostają zasadniczo bez zmian, z tym, że odwołania do funkcji semantycznych dla wyrażen zastępujemy przez odpowiednie tranzycje.
+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:
@@ Linia 84: / 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 161: / Linia 159: @@
 </div></div>
-}}
@@ Linia 174: / Linia 172: @@
 i rozszerz semantykę z poprzedniego zadania.
-Dzielenie przez zero jest błądem i  kończy natychmiast wykonanie programu.
+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ł.
 }}
-{{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
@@ Linia 198: / 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> oblicza się do wartości różnej od zera.
@@ Linia 210: / 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>
@@ Linia 266: / 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.
+Zwróćmy szczególnie uwagę na ostatnią regułę dla pętli <math>\mathbf{while}\ </math>,: wyraża ona przypadek, gdy błąd został wygenerowany nie w pierwszym obiegu pętli, ale w którymś z kolejnych.
 Musieliśmy rozważyc również ten przypadek, ponieważ wybraliśmy podejście dużych kroków; w podejściu małych kroków nie byłoby to zapewne konieczne.
 </div></div>
-}}
 {{cwiczenie|3|cw3|
-Rozszerzmy język Tiny o następującą instrukcję pętli:
+Rozszerzmy język TINY o następującą instrukcję pętli:
 <math>
@@ Linia 285: / Linia 282: @@
 <math>\mathbf{loop}\, I</math> to instrukcja pętli, <math>I</math> stanowi instrukcję wewnętrzną.
-Instrukcja <math>\mathbf{exit}</math> wychodzi z nabliższej otaczającej pętli <math>\mathbf{loop}\,</math> i kontynuuje wykonanie programu od pierwszej instrukcji za tą pętlą.
+Instrukcja <math>\mathbf{exit}</math> wychodzi z nabliższej otaczającej pętli <math>\mathbf{loop}\ </math>, i kontynuuje wykonanie programu od pierwszej instrukcji za tą pętlą.
-Instrukcja <math>\mathbf{continue}</math> powraca na początek instrukcji wewnętrznej najbliższej otaczającej pętli <math>\mathbf{loop}\,</math>.
+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 kilka nowych reguł opisujących nową konstrukcję języka i jej ,,interakcję" z pozostałymi konstrukcjami.
+<div class="mw-collapsible mw-made=collapsible mw-collapsed">
+<span class="mw-collapsible-toogle mw-collapsible-toogle-default style="font-variant:small-caps">Rozwiązanie</span>
+<div class="mw-collapsible-content" style="display:none">
+Dodamy do reguł semantyki naturalnej dla języka TINY kilka nowych reguł opisujących nową konstrukcję języka i jej "interakcję" z pozostałymi konstrukcjami.
 Pomysł polega na dodaniu specjalnych konfiguracji zawierających informację o tym, że została wykonana instrukcja <math>\mathbf{exit}</math> lub <math>\mathbf{continue}</math>. Oto odpowiednie reguły:
@@ Linia 303: / Linia 302: @@
 \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ą stanu <math>s</math>, ale zostawiają po sobie ,,ślad".
+Czyli instrukcje <math>\mathbf{exit}</math> i <math>\mathbf{continue}</math> nie modyfikują stanu <math>s</math>, ale zostawiają po sobie "ślad".
-Zauważmy, że taki ślad zostaje pozostawiony tylko wtedy, 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>.
+Zauważmy, że taki ślad zostaje pozostawiony tylko wtedy, jeśli nie było dotychczas innego śladu, to znaczy jeśli <math>\mathbf{exit}</math> (lub <math>\mathbf{continue}</math>) zostało wykonane w zwykłym stanie <math>s</math>.
 Oczywiście poszerzamy odpowiednio zbiór konfiguracji o:
 <math>
-\mathbf{State} \times \{ \mbox{było-}\mathbf{exit}, \mbox{było-}\mathbf{continue} \}.
+\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>?
 Czy instrukcje <math>\mathbf{exit}</math> i <math>\mathbf{continue}</math> będą faktycznie wykonywane w takich konfiguracjach?
-Zapiszmy teraz jak inne instrukcje korzystają z dodatkowej informacji (śladu) zawartej w konfiguracjach.
+Zapiszmy teraz, jak inne instrukcje korzystają z dodatkowej informacji (śladu) zawartej w konfiguracjach.
-Oczywiście ,,beneficjentem" korzystającym z tej informacji jest instrukcja <math>\mathbf{loop}\,</math>:
+Oczywiście "beneficjentem" korzystającym z tej informacji jest instrukcja <math>\mathbf{loop}\ </math>,:
 <math>
@@ Linia 328: / Linia 325: @@
 </math>
-Czyli w zależności od tego, jaki ślad został zarejestrowany podczas wykonania <math>I</math>, albo kończymy wykonanie  pętli <math>\mathbf{loop}\,</math>, albo rozpoczynamy kolejną iterację.
+Czyli w zależności od tego, jaki ślad został zarejestrowany podczas wykonania <math>I</math>, albo kończymy wykonanie  pętli <math>\mathbf{loop}\ </math>,, albo rozpoczynamy kolejną iterację.
 Zauważmy, że stan <math>s'</math> może być różny od <math>s</math>, ponieważ zanim wykonała się ktoraś z instrukcji <math>\mathbf{exit}</math> lub
-<math>\mathbf{continue}</math>, mogły zostać zmienione wartości niektórych zmiennych.
+<math>\mathbf{continue}</math> mogły zostać zmienione wartości niektórych zmiennych.
-Oczywiście, jeśli instrukcja wewnętrzna <math>I</math> zakończyła się ''normalnie'', kontynuujemy wykonanie pętli podobnie jak w przypadku wywołania <math>\mathbf{continue}</math>:
+Oczywiście, jeśli instrukcja wewnętrzna <math>I</math> zakończyła się "normalnie", kontynuujemy wykonanie pętli podobnie jak w przypadku wywołania <math>\mathbf{continue}</math>:
 <math>
@@ Linia 349: / Linia 346: @@
 </math>
-Okazuje się że nie, ponieważ ślad powinien zostać zawsze ,,wymazany" przez pętlę <math>\mathbf{loop}\,</math>.
+Okazuje się że nie, ponieważ ślad powinien zostać zawsze "wymazany" przez pętlę <math>\mathbf{loop}\ </math>,.
 Teraz musimy określić zachowanie wszystkich instrukcji w sytuacji, gdy bieżąca konfiguracja zawiera już ślad. Zasadniczo, powinniśmy zaniechać wykonania instrukcji (w przypadku pętli, powinniśmy zaniechać dalszego iterowania tej pętli).
@@ Linia 380: / Linia 377: @@
 Pominęliśmy zupełnie analogiczne reguły dla <math>\mbox{było-}\mathbf{continue}</math>.
-Zauważmy, że dla pętli <math>\mathbf{while}\,</math> nie rozpatrujemy przypadku, gdy dozór <math>b</math> oblicza się do <math>\mathbf{false}</math>, gdyż w tym przypadku nie ma możliwości wygenerowania śladu.
+Zauważmy, że dla pętli <math>\mathbf{while}\ </math>, nie rozpatrujemy przypadku, gdy dozór <math>b</math> oblicza się do <math>\mathbf{false}</math>, gdyż w tym przypadku nie ma możliwości wygenerowania śladu.
 Zauważmy też, że nasze reguły nie pozwalają na dodanie drugiego (kolejnego) śladu!
 </div></div>
-}}
-{{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 zapewnić pomijanie instrukcji w sytuacji, gdy został juz zarejestrowany jakiś ślad. Było to dość uciążliwe.
+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.
+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:
+Podobnie jak poprzednio, rozszerzymy zbiór konfiguracji i podobnie 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 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 powstaje w <math>I_2</math>, bo wybraliśmy podejście mało-krokowe.
+Nie musimy zajmowac się przypadkiem, gdy ślad powstaje w <math>I_2</math>, bo wybraliśmy podejście małokrokowe.
-Ponadto, nie musimy opisywać instrukcji warunkowej i pętli <math>\mathbf{while}\,</math>, ponieważ ślad nie może powstać podczas obliczania dozoru!
+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 sytuacji!
+Reguły te są prawie identyczne z regułami semantyki naturalnej dla tej sytuacji!
-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>!
+Natomiast korzystamy z tego, że w podejściu małokrokowym zmiana konfiguracji na <math>s', \mbox{było-}\mathbf{exit}</math> czy <math>s', \mbox{było-}\mathbf{continue}</math> jest ''natychmiast'' widoczna w instrukcji <math>\mathbf{loop}\, I</math>, nawet jeśli <math>\mathbf{exit}</math> czy <math>\mathbf{continue}</math> zostało wywołane głęboko wewnątrz <math>I</math>!
 Niestety powyższe reguły '''nie są poprawne'''!
-Dlaczego? Jak zwykle w semantyce małych kroków, wykonując instrukcję wewnętrzną ''zapominamy'' stopniowo jaka była ona na początku.
+Dlaczego? Jak zwykle w semantyce małych kroków, wykonując instrukcję wewnętrzną "zapominamy" stopniowo, jaka była ona na początku.
-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>.
+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 tak, aby możliwe było jednorazowe rozwinięcie pętli <math>\mathbf{loop}\,</math>:
+Prostym sposobem poprawienia naszego błędu jest rozszerzenie składni tak, aby możliwe było jednorazowe rozwinięcie pętli <math>\mathbf{loop}\ </math>,:
 <math>
-\mathbf{loop}\, I, s \,\Longrightarrow\, I \,\mathbf{then}\, \mathbf{loop}\, I, s.
+\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 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>:
+Teraz możemy zapisać dwie powyższe reguły dla <math>\mathbf{loop}\ </math>, w poprawnej wersji, pamiętając o tym, że <math>\mbox{było-}\mathbf{exit}</math> i <math>\mbox{było-}\mathbf{continue}</math> pojawią się nie w instrukcji wewnętrznej, ale w jej ''kopii'' umieszczonej przed <math>\,\mathbf{then}\ </math>,:
 <math>
-\frac{I', s \,\Longrightarrow\, s', \mbox{było-}\mathbf{exit}}
+\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 stojącej przed <math>\,\mathbf{then}\,</math> (w szczególności może ona zawierać zagnieżdzone pętle <math>\mathbf{loop}\,</math>):
+Potrzebujemy też dodatkowej reguły dla obliczeń wewnątrz instrukcji stojącej przed <math>\,\mathbf{then}\ </math>, (w szczególności może ona zawierać zagnieżdzone pętle <math>\mathbf{loop}\ </math>,):
 <math>
-\frac{I', s \,\Longrightarrow\, I'', s'}
+\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 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.
+Na koniec zauważmy, że stan <math>s'</math> w pierwszych dwóch z powyższych reguł nigdy nie jest różny od <math>s</math>. Zatem równoważnie moglibyśmy zamienić <math>s'</math> na <math>s</math> w powyższych dwóch regułach. Ale wtedy okazuje się, <math>s</math> w parze z <math>\mbox{było-}\mathbf{exit}</math> albo <math>\mbox{było-}\mathbf{continue}</math> jest nadmiarowe i może zostać wyeliminowane.
 Zatem ostatecznie nasze reguły mogą wyglądać tak:
 <math>
-\mathbf{exit}, s \,\Longrightarrow\, \mbox{było-}\mathbf{exit}
+\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>
@@ Linia 500: / Linia 493: @@
 </div></div>
-}}
 == Zadania domowe ==
@@ Linia 508: / 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.
 }}
@@ Linia 515: / 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 524: / Linia 515: @@
 </math>
-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.
+Identyfikator <math>x</math> pełni tutaj rolę etykiety związanej z instrukcją <math>\mathbf{loop}\ </math>,, jest też parametrem dwóch pozostałych instrukcji.
-<math>\mathbf{exit} x</math> kończy teraz najbliższą otaczającą pętlę <math>\mathbf{loop}\,</math> o etykiecie <math>x</math>. Podobnie <math>\mathbf{continue} x</math> wznawia najbliższą otaczającą pętlę o etykiecie <math>x</math>.
+<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>.
 }}
@@ Linia 532: / Linia 523: @@
 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 542: / Linia 533: @@
 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.
+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>.
+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>,.
@@ Linia 549: / Linia 540: @@
 {{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 561: / Linia 552: @@
 Obliczenie wyrażenia <math>\,\mathbf{do}\, I \,\mathbf{then}\, e</math> polega na wykonaniu <math>I</math> a potem na obliczeniu <math>e</math>.
-Wartość wyrażenia <math>x:= e</math> jest taka jak wartość wyrażenia <math>e</math> a efektem ubocznym jest podstawienie tej wartości na zmienną <math>x</math>.
+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>.
 }}