Semantyka i weryfikacja programów/Ćwiczenia 3

Zawartość

Kończymy semantykę małych kroków i rozpoczynamy semantykę naturalną (duże kroki). Uzupełnimy semantykę naturalną języka Tiny o semantykę naturalną dla wyrażeń boolowskich i arytmetycznych i semantykę dla błędów wykonania. Wreszcie dodamy instrukcję pętli $𝐥 𝐨 𝐨 𝐩$ i instrukcje niestrukturalnego zakończenia pętli (instrukcje $𝐞 𝐱 𝐢 𝐭$ i $𝐜 𝐨 𝐧 𝐭 𝐢 𝐧 𝐮 𝐞$ ).

Rozszerzenia semantyki języka Tiny

Zadanie 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 jezyka 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żen 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 stalych 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 arytmnetycznych, 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}$

Oto inny wariant, reguły lewo-stronne (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 wariant prawo-stronny ( najpierw $b_{2}$ , potem $b_{1}$ ). Wreszcie rozważmy kombinację obydwu semantyk (reguły równoległe):

$\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 ⟶ 𝐭 𝐫 𝐮 𝐞}$

W naszym prostym języku wszystkie cztery warianty są równoważne. Reguły dla pozostałych spójników logicznych, dla negacji oraz dla instrukcji przypisania pozostawiamy jako proste ćwiczenie.

Zadanie 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 (szkic)

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:

$\frac{e_{2}, s ⟶ 0}{e_{1} / e_{2}, 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:

$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}$

Zadanie 3

Rozszerz 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 pętli $𝐥 𝐨 𝐨 𝐩$ i kontynuuje wykonanie programu od pierwszej instrukcji za tą pętlą. Instrukcje $𝐜 𝐨 𝐧 𝐭 𝐢 𝐧 𝐮 𝐞$ powraca na początek instrukcji wewnętrznej najbliższej pętli.

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

Rozwiązanie 1 (semantyka naturalna)

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, jesli 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:

</math>[ \mathbf{State} \times \{ \mbox{było-}\mathbf{exit}, \mbox{było-}\mathbf{continue} \} </math> , 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 tej informacji jest instrukcji $𝐥 𝐨 𝐨 𝐩$ :

$\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ę $𝐥 𝐨 𝐨 𝐩$ . Poza tym reguły te wykraczałyby poza klasyczna podejście semantyki naturalnej, w którym zwykle bezpośrednio definiujemy tranzycje postaci $I, s ⟶ s^{'}$ .

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 konfiguracji $s^{'}, było- 𝐜 𝐨 𝐧 𝐭 𝐢 𝐧 𝐮 𝐞$ . Zwróćmy szczególnie uwagę na ostatnią regułę dla pętli $𝐰 𝐡 𝐢 𝐥 𝐞$ : wyraża ona przypadek, gdy ślad $𝐞 𝐱 𝐢 𝐭$ został wygenerowany nie w pierwszym obiegu pętli, ale w którymś z kolejnych. Musieliśmy rozważyc również ten przypadek, ponieważ wybraliśmy podejście dużych kroków; w podejściu małych kroków nie byłoby to zapewne konieczne. Zauważmy też, że dla pętli $𝐰 𝐡 𝐢 𝐥 𝐞$ nie rozpatrujemy przypadku, gdy dozór $b$ oblicza się do $𝐭 𝐫 𝐮 𝐞$ , gdyż w tym przypadku nie ma możliwości wygenerowania śladu.

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

Rozwiązanie 2 (małe kroki)

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- 𝐜 𝐨 𝐧 𝐭 𝐢 𝐧 𝐮 𝐞 .$

Zauważmy, że nie musimy zajmowac się przypadkiem, gdy ślad powstaje w $I_{2}$ , bo wybraliśmy podejście mało-krokowe. Ponadto, nie musimy opisywać instrukcji warunkowej i pętli $𝐰 𝐡 𝐢 𝐥 𝐞$ , ponieważ ślad nie może powstać podczas oblcizania 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 do reguł semantyki naturalnej dla tej sytuacji! Natomiast korzystamy z tego, że w podejściu mało-krokowym 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, powyzsze 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. I w związku z tym nie potrafimy poprawnie powrócić do wykonywania pętli $𝐥 𝐨 𝐨 𝐩$ po wywołaniu $𝐜 𝐨 𝐧 𝐭 𝐢 𝐧 𝐮 𝐞$ .

Prostym sposobem poprawienia naszego blę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^{'}}$

A ponieważ wewnątrz kopii mogą być zagnieżdzone instrukcje $𝐥 𝐨 𝐨 𝐩$ potrzebujemy dodatkowej reguły:

$\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 trzech 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 ⟹ I^{″}, s^{'}}{I^{'} 𝐭 𝐡 𝐞 𝐧 𝐥 𝐨 𝐨 𝐩 I, s ⟹ I^{″} 𝐭 𝐡 𝐞 𝐧 𝐥 𝐨 𝐨 𝐩 I, s^{'}}$

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

Zadania domowe

Zadanie 1

Zaproponuj semantykę mało-krokową języka z zdania 2. Czy różni się ona istotnie od semantyki naturalnej?

Zadanie 2

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

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

Identyfikator $x$ pełni tutaj rolę etykiety przypisanej instrukcji $𝐥 𝐨 𝐨 𝐩$ , 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ą pętlę o etykiecie $x$ . Np. program

Parser nie mógł rozpoznać (błąd składni): {\displaystyle x: \mathbf{loop}\,\\ \quad \quad a := 1; \quad \quad y: \mathbf{loop}\, \quad \quad \quad \quad \mathbf{exit} x; \quad \quad \quad \quad a := a-10; \quad \quad a := a+1; a := a+2; }

kończy działanie z wartością zmiennej $a = 3$ . Zauważmy, że musieliśmy jakoś określić, do wnętrza której pętli $𝐥 𝐨 𝐨 𝐩$ należą trzy ostatnie instrukcje. Użyliśmy to tego celu wcięć a niejednoznaczność bierze się oczywiście stąd, że pracujemy ze składnią abstrakcyjną. Składnia konkretna zawierałaby prawdopodobnie jakąś konstukcję zamykającą pętlę $𝐥 𝐨 𝐨 𝐩$ , np. $𝐥 𝐨 𝐨 𝐩 I 𝐞 𝐧 𝐝 𝐥 𝐨 𝐨 𝐩$ .

Zadanie 3

Napisz semantykę naturalną i mało-krokową 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

Spis treści

Zawartość

Rozszerzenia semantyki języka Tiny

Zadanie 1

Rozwiązanie

Zadanie 2

Rozwiązanie (szkic)

Zadanie 3

Rozwiązanie 1 (semantyka naturalna)

Rozwiązanie 2 (małe kroki)

Zadania domowe

Zadanie 1

Zadanie 2

Zadanie 3

Menu nawigacyjne

Działania na stronie

Opcje strony

Narzędzia osobiste

Nawigacja

Szukaj

Narzędzia