Semantyka i weryfikacja programów/Ćwiczenia 1

Ćwiczenia 1: semantyka operacyjna wyrażeń (małe kroki)

Zadanie 1 (przygotowawcze)

Rozważmy prosty język wyrażeń, którego składnia opisana jest następującą gramatyką:

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

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

$e : : = n | x | e_{1} + e_{2} | 𝐢 𝐟 e_{1} 𝐭 𝐡 𝐞 𝐧 e_{2} 𝐞 𝐥 𝐬 𝐞 e_{3}$

Wynikiem wyrażenienia warunkowego $𝐢 𝐟 e_{1} 𝐭 𝐡 𝐞 𝐧 e_{2} 𝐞 𝐥 𝐬 𝐞 e_{3}$ jest wartość wyrażenia $e_{2}$ , o ile wyrażenie $e_{1}$ oblicza się do wartości różnej od zera; w przeciwnym przypadku wynikiem jest wartość wyrażenia $e_{3}$ .

Zaproponuj semantykę operacyjną (małe kroki) dla tego języka.

Rozwiązanie

Zacznijmy od ustalenia notacji i dziedzin syntaktycznych. Niech $𝐍 𝐮 𝐦$ oznacza zbiór stałych liczbowych, $n \in 𝐍 𝐮 𝐦 = {0, 1, \dots}$ . Podobnie, niech $𝐕 𝐚 𝐫$ oznacza zbiór identyfikatorów, które mogą być nazwami zmiennych; $x \in 𝐕 𝐚 𝐫$ . Wreszcie, niech $𝐄 𝐱 𝐩$ oznacza zbiór wyrażeń; $e \in 𝐄 𝐱 𝐩$ . Dla ułatwienia zapisywania reguł zakładamy, ze stałe liczbowe sa wyrażeniami, czyli $𝐍 𝐮 𝐦 \subseteq 𝐄 𝐱 𝐩$ .

Będziemy potrzebować zbioru stanów, opisujących wartości przypisane zmiennym. Najprostszym rozwiązaniem jest przyjąc, że stan to funkcja z $𝐕 𝐚 𝐫$ do $𝐍 𝐮 𝐦$ . Oznaczmy przez $𝐒 𝐭 𝐚 𝐭 𝐞$ zbiór wszystkich takich funkcji; stany oznaczac będziemy przez $s, s_{1}, s^{'}, \dots \in 𝐒 𝐭 𝐚 𝐭 𝐞$ .

W naszej semantyce będziemy potrzebowac tranzycji dwóch postaci. Po pierwsze, tranzycja

$e, s ⟹ e^{'}, s$

oznaczająca mały krok w trakcie obliczania wyrażenia $e$ w stanie $s$ , w wyniku którego $e$ wyewoluowało do $e^{'}$ . Stan nie ulega zmiania podczas obliczania wyrażenia, więc to samo $s$ figuruje po lewej i prawej stronie strzałki.

Po drugie, tranzycja $e, s ⟹ n$

będzie oznaczaczać, że wyrażenie $e$ jest już policzone, a jego wartością jest $n$ .

Zatem przyjmijmy, że zbiór konfiguracji to

$(𝐄 𝐱 𝐩 \times 𝐒 𝐭 𝐚 𝐭 𝐞) \cup 𝐍 𝐮 𝐦$

a konfiguracje końcowe to $𝐍 𝐮 𝐦$ .

Uwaga: tranzycje pierwszej postaci mogłyby również wyglądać następująco: $e, s ⟹ e^{'};$ wtedy zbiorem konfiguracji byłby zbiór $(𝐄 𝐱 𝐩 \times 𝐒 𝐭 𝐚 𝐭 𝐞) \cup 𝐄 𝐱 𝐩$ a konfiguracje końcowe pozostałyby bez zmian (koniec uwagi).

Najprostsze są tranzycje prowadzące do konfiguracji końcowej:

$n, s ⟹ n$

Zmienna oblicza się do swojej wartości w bieżącym stanie: $x, s ⟹ n, s o ile s (x) = n$

Teraz zajmiemy się dodawaniem $e_{1} + e_{2}$ . Ponieważ semantyka jest w stylu małych kroków, musimy zdecydować się czy najpierw obliczyć pierwszy (lewy) składnik Parser nie mógł rozpoznać (błąd składni): {\displaystyle e_1 ] czy drugi? Jeśli wybierzemy lewy, otrzymamy regułę: <math> \frac{e_1, s \,\Longrightarrow\, e'_1, s} {e_1 + e_2, s \,\Longrightarrow\, e'_1 + e_2}. }

Czyli mały krok w $e_{1}$ stanowi też mały krok w $e_{1} + e_{2}$ . Po zakończeniu obliczania $e_{1}$ przechodzimy do $e_{2}$ :

$\frac{e_{2}, s ⟹ e'_{2}, s}{n + e_{2}, s ⟹ n + e'_{2}, s} .$

A na końcu dodajemy:

$n_{1} + n_{2}, s ⟹ n, s o ile n = n_{1} + n_{2} .$

Zauważmy tutaj pewną subtelność, dotyczącą dwóch wystąpień symbolu +: pierwsze wystąpienie oznacza jedną z konstrukcji składniowych języka, a drugie oznacza operację dodawania w zbiorze $𝐍 𝐮 𝐦$ . Pozwalamy sobie na taką kolizję oznaczeń, gdyż nie powinna ona prowadzić do niejednoznaczności. Pamiętajmy, że składnia języka jest składnią abstrajkcyjną, więc zamiast $e_{1} + e_{2}$ moglibyśmy równie dobrze pisać np. $a d d (e_{1}, e_{2})$ .

Inna możliwą strategią obliczania $e_{1} + e_{2}$ jest strategia prawostronna, którą otrzymujemy zastępując pierwsze dwie z trzech powyższych reguł przez:

$\frac{e_{2}, s ⟹ e'_{2}, s}{e_{1} + e_{2}, s ⟹ e_{1} + e'_{2}} \frac{e_{1}, s ⟹ e'_{1}, s}{e_{1} + n, s ⟹ e'_{1} + n, s} .$

Ponadto, jeśli przyjmiemy wszystkie pięc reguł, otrzymamy strategię równoległą, polegającą na obliczaniu jednocześnie $e_{1}$ i $e_{2}$ . Bardziej precyzyjnie mówiąc, małe kroki obliczające obydwa podwyrażenia przeplatają się, i to w dowolny sposób. Ta dowolność prowadzi do niedeterminizmu, czyli do sytuacji, gdy kolejna (następna) konfiguracja nie jest wyznaczona jednoznacznie. Jest tak, gdyż jednocześnie możemy mieć dwie tranzycje

$e_{1} + e_{2}, s ⟹ e'_{1} + e_{2}, s e_{1} + e_{2}, s ⟹ e_{1} + e'_{2}, s .$

Zauważmy natomiast, że kolejność przeplatania się małych kroków obliczających $e_{1}$ i $e_{2}$ nie wpływa w tym przypadku na końcową wartość całego wyrażenia.

Na koniec reguły dla wyrażenia warunkowego.

$\frac{e_{1}, s ⟹ e'_{1}, s}{𝐢 𝐟 e_{1} 𝐭 𝐡 𝐞 𝐧 e_{2} 𝐞 𝐥 𝐬 𝐞 e_{3}, s ⟹ 𝐢 𝐟 e'_{1} 𝐭 𝐡 𝐞 𝐧 e_{2} 𝐞 𝐥 𝐬 𝐞 e_{3}, s}$

$𝐢 𝐟 n 𝐭 𝐡 𝐞 𝐧 e_{2} 𝐞 𝐥 𝐬 𝐞 e_{3}, s ⟹ e_{2}, s o ile n \neq 0$

$𝐢 𝐟 n 𝐭 𝐡 𝐞 𝐧 e_{2} 𝐞 𝐥 𝐬 𝐞 e_{3}, s ⟹ e_{3}, s o ile n = 0$

Zadanie 2

Rozszerzmy język wyrażeń z poprzedniego zadania o jedną konstrukcję $e : : = \dots | 𝐥 𝐞 𝐭 x = e_{1} 𝐢 𝐧 e_{2}$

Wyrażenie $𝐥 𝐞 𝐭 x = e_{1} 𝐢 𝐧 e_{2}$ zawiera w sobie deklarację $x = e_{1}$ , która stanowi jedyny mechannizm wiązania identyfikatorów w naszym języku. Wartość wyrażenia $𝐥 𝐞 𝐭 x = e_{1} 𝐢 𝐧 e_{2}$ obliczamy następująco: najpierw oblicza się wartość $e_{1}$ , podstawia ją na zmienna $x$ , a następnie oblicza wyrażenie $e_{2}$ . Zakresem zmiennej $x$ jest wyrażenie $e_{2}$ , ale jeśli w $e_{2}$ występuje podwyrażenie $𝐥 𝐞 𝐭 x = \dots 𝐢 𝐧 e$ to odwołania do $x$ wewnątrz $e$ odnoszą się do najbliższej (najbardziej zagnieżdzonej) deklaracji zmiennej $x$ . Taki mechanizm wiązania identyfikatorów nazywamy wiązaniem statycznym.

Zakładamy, że na początku wartości wszystkich zmiennych są nieokreślone, czyli zmienne są niezainicjowane, a odwołanie do niezainicjowanej zmiennej jest uważane za niepoprawne.

Przykłady

$𝐥 𝐞 𝐭 x = z + z 𝐢 𝐧 𝐥 𝐞 𝐭 y = 7 𝐢 𝐧 𝐥 𝐞 𝐭 x = y + 3 𝐢 𝐧 x + x + y wynik = 24$ $𝐥 𝐞 𝐭 y = 5 𝐢 𝐧 𝐥 𝐞 𝐭 x = (𝐥 𝐞 𝐭 y = 3 𝐢 𝐧 y + y) 𝐢 𝐧 x + y wynik = 11$ Parser nie mógł rozpoznać (błąd składni): {\displaystyle \mathbf{let}\, z = 5 \,\mathbf{in}\, x+z \quad \quad \mbox{brak wyniku; odwołanie do niezainicjowanej zmiennej}\, x } $𝐥 𝐞 𝐭 x = 1 𝐢 𝐧 𝐥 𝐞 𝐭 x = x + x 𝐢 𝐧 x wynik = 2$

Rozwiązanie

Podobnie jak poprzednio, stan powinien opisywać wartości przypisane zmiennym, ale powinniśmy też uwzględnić niezainicjowane zmienne, czyli zmienne bez żadnej wartości. Przyjmijmy zatem, że stan to skończona funkcja częściowa z $𝐕 𝐚 𝐫$ do $𝐍 𝐮 𝐦$ . Oznaczmy przez $𝐒 𝐭 𝐚 𝐭 𝐞$ zbiór wszystkich takich funkcji. Naturalnym stanem początkowym jest stan pusty, tzn. pusta funkcja częściowa, który będziemy oznaczać $\emptyset$ . A wartość wyrażenia $e$ w stanie początkowym wynosi $n$ o ile zachodzi:

$e, \emptyset ⟹^{*} n .$

Będziemy potrzebowac tranzycji dwóch postaci, podobnie jak poprzednio, ale pierwsza postać będzie trochę ogólniejsza:

$e, s ⟹ e^{'}, s^{'} .$

Tranzycja ta oznacza mały krok w trankcie obliczania wyrażenia $e$ w stanie $s$ , w wyniku którego $e$ wyewoluowało do $e^{'}$ a nowym stanem jest $s^{'}$ . Stan może się teraz zmienić na skutek deklaracji zmiennych.

Ponieważ stan jest funkcją częściową, musimy zmienić niektóre reguły, np.

$x, s ⟹ n, s o ile s (x) jest określone i s (x) = n$

Zadanie 3

Zmodyfikuj semantykę z poprzedniego zadania tak, aby uzyskać leniwą ewaluację wyrażeń, zgodnie z dyrektywą: nie obliczaj wyrażenia o ile jego wynik nie jest potrzebny (albo: obliczaj wartość wyrażenia dopiero wtedy, gdy jego wynik jest naprawdę potrzebny). Spojrzmy na przykład:

$𝐥 𝐞 𝐭 x = 7 𝐢 𝐧 𝐥 𝐞 𝐭 y = y + y 𝐢 𝐧 x + x$

Według semantyki z poprzedniego zadania wyrażnie to nie ma wartości, bo w deklaracji $y = y + y$ jest odwołanie do niezainicjowanej zmiennej. Natomiast w semantyce leniwej wyrażenie to obliczy się do wartości $14$ , ponieważ wyrażenie $y + y$ nie będzie wogóle obliczane. Będzie tak dlatego, że w wyrażeniu $x + x$ nie ma odwołań do zmiennej $y$ .

Rozwiązanie

Zadanie 4

Dotychczas wystąpienie błędu podczas obliczania wyrażenia, np. odwołanie do niezainicjowanej zmiennej, powodowało, że wyrażenie nie posiadało wartości (nie było ciągu tranzycji prowadzących do konfiguracji końcowej). Zmodyfikuj którąś z semantyk z poprzednich zadań tak, aby błąd był komunikowany jako jedna z konfiguracji końcowych. To znaczy: jeśli obliczenie wyrażenia $e$ w stanie $s$ jest niemożliwe bo wystąpił błąd, to

$e, s ⟹^{*} B l a d$

Semantyka i weryfikacja programów/Ćwiczenia 1

Spis treści

Ćwiczenia 1: semantyka operacyjna wyrażeń (małe kroki)

Zadanie 1 (przygotowawcze)

Rozwiązanie

Zadanie 2

Przykłady

Rozwiązanie

Zadanie 3

Rozwiązanie

Zadanie 4

Menu nawigacyjne

Działania na stronie

Opcje strony

Narzędzia osobiste

Nawigacja

Szukaj

Narzędzia