Semantyka i weryfikacja programów/Ćwiczenia 5: Różnice pomiędzy wersjami

Aktualna wersja na dzień 21:30, 11 wrz 2023

Zawartość

Kontynuujemy ćwiczenie semantyki naturalnej, dodając pewne konstrukcje do języka TINY. W szczególności rozszerzymy go o deklaracje zmiennych (bloki). Po raz pierwszy roszdzielimy informację przechowywaną w konfiguracji na środowisko określające wiązanie identyfikatorów i stan przechowujący wartości zmiennych. Będzie to przygotowanie do kolejnych zajęć.

Semantyka naturalna pewnej instrukcji $𝐟 𝐨 𝐫$ ,

Ćwiczenie 1

Rozszerzamy język TINY następująco:

$I : : = \dots | 𝐟 𝐨 𝐫 x = e_{1} 𝐭 𝐨 e_{2} 𝐭 𝐫 𝐲 I_{1} 𝐞 𝐥 𝐬 𝐞 I_{2} | 𝐟 𝐚 𝐢 𝐥$

Znaczenie instrukcji $𝐟 𝐨 𝐫 x = e_{1} 𝐭 𝐨 e_{2} 𝐭 𝐫 𝐲 I_{1} 𝐞 𝐥 𝐬 𝐞 I_{2}$ jest następujące. Obliczamy wartości wyrażeń $e_{1}$ i $e_{2}$ . Jeśli pierwsza z nich jest mniejsza od lub równa drugiej, podstawiamy pierwszą wartość (wartość wyrażenia $e_{1}$ ) na zmienną $x$ i uruchamiamy $I_{1}$ . Jeśli w $I_{1}$ nie zostanie napotkana instrukcja $𝐟 𝐚 𝐢 𝐥$ , kończymy instrukcję $𝐟 𝐨 𝐫$ , i przyracamy wartość zmiennej $x$ sprzed tej instrukcji. Natomiast jeśli w $I_{1}$ zostanie napotkana instrukcja $𝐟 𝐚 𝐢 𝐥$ , podstawiamy na $x$ kolejną, o jeden większą wartość, przywracamy wartości wszystkich pozostałych zmiennych sprzed instrukcji $𝐟 𝐨 𝐫$ , i ponownie wykonujemy $I_{1}$ . Powtarzamy w ten sposób, aż $I_{1}$ zakończy się nie napotkawszy $𝐟 𝐚 𝐢 𝐥$ , albo wartość zmiennej $x$ przekroczy wartość wyrażenia $e_{2}$ obliczoną na początku. W pierwszym przypadku kończymy instrukcję $𝐟 𝐨 𝐫$ , i przyracamy wartość zmiennej $x$ sprzed tej instrukcji. W drugim przywracamy wartości wszystkich zmiennych sprzed instrukcji $𝐟 𝐨 𝐫$ , i uruchamiamy $I_{2}$ .

Przykład

Oto przykładowy program:

x := 0; y := 1;
 $𝐟 𝐨 𝐫$ , x := 1  $𝐭 𝐨$ , 5  $𝐭 𝐫 𝐲$ ,
  y := y+1;
   $𝐢 𝐟$ , x <= 4  $𝐭 𝐡 𝐞 𝐧 𝐟 𝐚 𝐢 𝐥 𝐞 𝐥 𝐬 𝐞$ , z:= x
 $𝐞 𝐥 𝐬 𝐞 𝐬 𝐤 𝐢 𝐩$

Wartości zmiennych po zakończeniu programu to: $x = 0, y = 2, z = 5$ .

Rozwiązanie

Będziemy posługiwać się jak zwykle tranzycjami postaci:

$I, s ⟶ s^{'} e, s ⟶ n$

Zacznijmy od najprostszego przypadku, gdy nie ma wogóle potrzeby uruchamiania instrukcji wewnętrznej $I_{1}$ , ponieważ wartość wyrażenia $e_{1}$ jest większa od $e_{2}$ :

$\frac{e_{1}, s ⟶ n_{1} e_{2}, s ⟶ n_{2} I_{2}, s ⟶ s^{'}}{𝐟 𝐨 𝐫 x = e_{1} 𝐭 𝐨 e_{2} 𝐭 𝐫 𝐲 I_{1} 𝐞 𝐥 𝐬 𝐞 I_{2}, s ⟶ s^{'}} o ile n_{1} > n_{2}$

Po prostu uruchamiamy instrukcję $I_{2}$ w stanie $s$ , ignorując $I_{1}$ .

Kolejny nietrudny przypadek to sytuacja, w której $n_{1} \leq n_{2}$ , a wykonanie instrukcji wewnętrznej $I_{1}$ kończy się sukcesem, tzn. nie następuje wywołanie instrukcji $𝐟 𝐚 𝐢 𝐥$ . Oto reguła dla tego przypadku:

$\frac{e_{1}, s ⟶ n_{1} e_{2}, s ⟶ n_{2} I_{1}, s [x \mapsto n_{1}] ⟶ s^{'}}{𝐟 𝐨 𝐫 x = e_{1} 𝐭 𝐨 e_{2} 𝐭 𝐫 𝐲 I_{1} 𝐞 𝐥 𝐬 𝐞 I_{2}, s ⟶ s^{'} [x \mapsto s (x)]} o ile n_{1} \leq n_{2}$

Tym razem uruchamiamy instrukcję $I_{1}$ , podstawiając na zmienną $x$ wartość $n_{1}$ . Zwróćmy uwagę, że po zakończeniu $I_{1}$ przywracamy wartość zmiennej $x$ sprzed jej wykonania.

Pozostał nam trzeci przypadek, gdy $n_{1} \leq n_{2}$ , a wykonanie instrukcji $I_{1}$ zakończyło się wykonaniem instrukcji $𝐟 𝐚 𝐢 𝐥$ gdzieś wewnątrz $I_{1}$ . Aby poprawnie opisać takie zdarzenie, potrzebujemy dodatkowych tranzycji postaci:

$I, s ⟶ było- 𝐟 𝐚 𝐢 𝐥$

Mówiąc formalnie, poszerzamy zbiór konfiguracji o jeden element $było- 𝐟 𝐚 𝐢 𝐥$ . Zauważmy, że po prawej stronie tranzycji nie ma wogóle stanu. Nie potrzebujemy go dla opisania semantyki instrukcji $𝐟 𝐨 𝐫$ ,: jeśli wystąpi $𝐟 𝐚 𝐢 𝐥$ , powtarzamy $I_{1}$ dla większej o $1$ wartości zmiennej $x$ , ale pozostałym zmiennym przywracamy wartość sprzed $I_{1}$ . A więc załóżmy, że

$I_{1}, s [x \mapsto n_{1}] ⟶ było- 𝐟 𝐚 𝐢 𝐥$ .

W takiej sytuacji powinniśmy przypisać $n_{1} + 1$ na zmienną $x$ i spróbować ponownie wykonać $I_{1}$ przy wartościach wszystkich pozostałych zmiennych, takich jak na początku instrukcji $𝐟 𝐨 𝐫$ ,. Powtarzamy ten schemat aż do skutku, tzn. aż do mementu, gdy zaistnieje któraś z poprzednich dwóch (prostych) sytuacji. Oto odpowiednia reguła:

$\frac{e_{1}, s ⟶ n_{1} e_{2}, s ⟶ n_{2} I_{1}, s [x \mapsto n_{1}] ⟶ było- 𝐟 𝐚 𝐢 𝐥 𝐟 𝐨 𝐫 x = e_{1} + 1 𝐭 𝐨 e_{2} 𝐭 𝐫 𝐲 I_{1} 𝐞 𝐥 𝐬 𝐞 I_{2}, s ⟶ s^{'}}{𝐟 𝐨 𝐫 x = e_{1} 𝐭 𝐨 e_{2} 𝐭 𝐫 𝐲 I_{1} 𝐞 𝐥 𝐬 𝐞 I_{2}, s ⟶ s^{'}} o ile n_{1} \leq n_{2}$

Zwróćmy uwagę na pewnien niezwykle istotny szczegół: po zakończeniu wykonania instrukcji $𝐟 𝐨 𝐫 x = e_{1} + 1 𝐭 𝐨 e_{2} 𝐭 𝐫 𝐲 I_{1} 𝐞 𝐥 𝐬 𝐞 I_{2}$ otrzymujemy stan $s^{'}$ , w którym nie przywracamy wartości zmiennej $x$ . Gdybyśmy tak zrobili, tzn. gdybyśmy zastąpili $s^{'}$ przez $s^{'} [x \mapsto s (x)]$ , nasze semantyka byłaby niepoprawna. Dlaczego? Dlatego, że nie wiemy tak naprawdę, czy powinniśmy przywracać wartość zmiennej $x$ , czy nie. Jeśli ostatecznie nasza instrukcja $𝐟 𝐨 𝐫$ , zakończyła się przez bezbłędne zakończenie instrukcji $I_{1}$ (przypadek drugi), to powinniśmy to zrobić; ale jeśli zakończyła się wykonaniem instrukcji $I_{2}$ (przypadek pierwszy), powinniśmy pozostawić wartość zmiennej $x$ taką, jaka jest ona po zakończeniu $I_{2}$ . A zatem w powyższej regule dla przypadku trzeciego nie przywracamy wartości zmiennej $x$ ; jeśli było to konieczne, to zostało już wykonane "głębiej", dzięki regule dla przypadku drugiego oraz dzięki temu, że instrukcja $𝐟 𝐨 𝐫 x = e_{1} + 1 𝐭 𝐨 e_{2} 𝐭 𝐫 𝐲 I_{1} 𝐞 𝐥 𝐬 𝐞 I_{2}$ wykonywana jest w orginalnym stanie $s$ , a nie w stanie, w którym kończy się $I_{1}$ (tego ostatniego stanu nawet nie znamy).

Jeszcze jeden drobiazg: zamiast $e_{1} + 1$ w $𝐟 𝐨 𝐫 x = e_{1} + 1 𝐭 𝐨 e_{2} 𝐭 𝐫 𝐲 I_{1} 𝐞 𝐥 𝐬 𝐞 I_{2}, s ⟶ s^{'}$ w regule powyżej, moglibyśmy podstawić policzoną już wartość, czyli $n_{1} + 1$ .

Na zakończenie prezentujemy reguły niebędne do tego, aby wygenerować $było- 𝐟 𝐚 𝐢 𝐥$ :

$𝐟 𝐚 𝐢 𝐥, s ⟶ było- 𝐟 𝐚 𝐢 𝐥$

oraz aby wystąpienie $𝐟 𝐚 𝐢 𝐥$ umiejscowione gdzieś "głęboko" zostało rozpropagowane do najbliższej otaczającej instrukcji $𝐟 𝐨 𝐫$ ,. Jeśli pojawił się $𝐟 𝐚 𝐢 𝐥$ , powinniśmy zaniechać dalszego wykonania instrukcji, a w przypadku pętli, powinniśmy zaniechać dalszego iterowania tej pętli. Oto odpowiednie reguły:

$\frac{I_{1}, s ⟶ było- 𝐟 𝐚 𝐢 𝐥}{I_{1}; I_{2}, s ⟶ było- 𝐟 𝐚 𝐢 𝐥} \frac{I_{1}, s ⟶ s^{'} I_{2}, s^{'} ⟶ było- 𝐟 𝐚 𝐢 𝐥}{I_{1}; I_{2}, s ⟶ było- 𝐟 𝐚 𝐢 𝐥}$

$\frac{b, s ⟶ 𝐭 𝐫 𝐮 𝐞 I_{1}, s ⟶ było- 𝐟 𝐚 𝐢 𝐥}{𝐢 𝐟 b 𝐭 𝐡 𝐞 𝐧 I_{1} 𝐞 𝐥 𝐬 𝐞 I_{2}, s ⟶ było- 𝐟 𝐚 𝐢 𝐥} i analogicznie gdy b, s ⟶ 𝐟 𝐚 𝐥 𝐬 𝐞$

$\frac{b, s ⟶ 𝐭 𝐫 𝐮 𝐞 I, s ⟶ było- 𝐟 𝐚 𝐢 𝐥}{𝐰 𝐡 𝐢 𝐥 𝐞 b 𝐝 𝐨 I, s ⟶ było- 𝐟 𝐚 𝐢 𝐥} \frac{b, s ⟶ 𝐭 𝐫 𝐮 𝐞 I, s ⟶ s^{'} 𝐰 𝐡 𝐢 𝐥 𝐞 b 𝐝 𝐨 I, s^{'} ⟶ było- 𝐟 𝐚 𝐢 𝐥}{𝐰 𝐡 𝐢 𝐥 𝐞 b 𝐝 𝐨 I, s ⟶ było- 𝐟 𝐚 𝐢 𝐥}$

Widać podobieństwo do analogicznych reguł dla pętli $𝐥 𝐨 𝐨 𝐩 I$ , którą zajmowaliśmy się na wcześniejszych zajęciach.

Zauważmy, że jeśli $𝐟 𝐚 𝐢 𝐥$ zostało wykonane poza jakąkolwiek pętlą $𝐟 𝐨 𝐫$ ,, to program "zakończy się" w konfiguracji $było- 𝐟 𝐚 𝐢 𝐥$ . Możemy zatem tę właśnie konfigurację uznać za konfigurację końcową, informującą o porażce wykonania programu.

Semantyka naturalna bloków

Ćwiczenie 2 (bloki i deklaracje zmiennych)

Rozszerz semantykę języka TINY o deklarację zmiennej:

$I : : = \dots | 𝐛 𝐞 𝐠 𝐢 𝐧 𝐯 𝐚 𝐫 x = e; I 𝐞 𝐧 𝐝$

Zasięgiem zmiennej $x$ jest instrukcja $I$ , czyli wnętrze bloku, w którym jest zadeklarowana. Zakładamy zwykłe (statyczne) reguły widoczności, przesłaniania, itp.

Rozwiązanie

Wariant 1 (tylko stan)

Oczywiście powinniśmy odróżniać zmienne zadeklarowane (i zarazem zainicjowane) od tych niezadeklarowanych. Zatem przyjmijmy, że

$𝐒 𝐭 𝐚 𝐭 𝐞 = 𝐕 𝐚 𝐫 \to_{f i n} 𝐍 𝐮 𝐦$ .

Zachowujemy wszystkie reguły semantyczne dla języka Tiny i dodajemy jedną nową:

$\frac{e, s ⟶ n I, s [x \mapsto n] ⟶ s^{'}}{𝐛 𝐞 𝐠 𝐢 𝐧 𝐯 𝐚 𝐫 x = e; I 𝐞 𝐧 𝐝, s ⟶ s^{'}}$

mówiącą, że instrukcja wewnętrzna $I$ ewaluowana jest w stanie, w którym dodatkowo zaznaczono wartość zmiennej $x$ równą wartości, do której oblicza się $e$ . Oczywiście takie rozwiązanie jest niepoprawne, gdyż wartość zmiennej $x$ pozostaje w stanie nawet po wyjściu z bloku ("wycieka" z bloku). Musimy dodać "dealokację" zmiennej $x$ :

$\frac{e, s ⟶ n I, s [x \mapsto n] ⟶ s^{'}}{𝐛 𝐞 𝐠 𝐢 𝐧 𝐯 𝐚 𝐫 x = e; I 𝐞 𝐧 𝐝, s ⟶ s^{″}} o ile s^{″} = s^{'} [x \mapsto s (x)]$

I znów napotykamy podobne trudności jak na wcześniejszych zajęciach: powyższa reguła nie obejmuje przypadku, gdy $s (x)$ jest nieokreślone. I choć moglibyśmy naprawić ten mankament podobnie jak kiedyś (co pozostawiamy Czytelnikowi), istnieje inne, bardzo eleganckie i elastyczne rozwiązanie tego problemu, które teraz omówimy.

Wariant 2 (stan i środowisko)

Podstawowy pomysł polega na rozdzieleniu informacji przechowywanej dotychczas w stanie, czyli odwzorowania nazw zmiennych w wartości, na dwa "etapy". Pierwszy z nich odwzorowuje identyfikatory zmiennych w lokacje, a drugi lokacje w wartości. Mamy więc środowiska $E \in 𝐄 𝐧 𝐯$ , będące funkcjami częściowymi z $𝐕 𝐚 𝐫$ do $𝐋 𝐨 𝐜$ , zbioru lokacji:

$𝐄 𝐧 𝐯 = 𝐕 𝐚 𝐫 \to_{f i n} 𝐋 𝐨 𝐜$

oraz stany, będące teraz funkcjami częściowymi z $𝐋 𝐨 𝐜$ do $𝐍 𝐮 𝐦$ :

$𝐒 𝐭 𝐨 𝐫 𝐞 = 𝐋 𝐨 𝐜 \to_{f i n} 𝐍 𝐮 𝐦$

Dla ścisłości używamy innej nazwy ( $𝐒 𝐭 𝐨 𝐫 𝐞$ ), ale będziemy zwykle używać podobnych symboli jak dotychczas $s, s^{'}, s_{1}, \dots \in 𝐒 𝐭 𝐨 𝐫 𝐞$ itp. do nazywania stanów. Intuicyjnie można myśleć o lokacjach w pamięci operacyjnej maszyny. Środowisko zawiera informację o lokacji, w której przechowywana jest wartość danej zmiennej a stan opisuje właśnie zawartość używanych lokacji.

Zakładamy przy tym, że mamy do dyspozycji nieskończony zbiór lokacji $𝐋 𝐨 𝐜 = {l_{0}, l_{1}, \dots}$ i że w każdym momencie tylko skończenie wiele spośród nich jest wykorzystywane. Formalnie mowiąc, dziedzina funkcji częściowej $s$ jest zawsze skończona. Daje nam to pewność, że zawsze jest jakaś nieużywana lokacja.

Środowisko początkowe, w którym uruchamiany będzie program, będzie z reguły puste. Ponadto obraz funkcji częściowej $E$ będzie zawsze zawarty w zbiorze aktualnie używanych lokacji, czyli zawarty w dziedzinie funkcji częściowej $s$ , oznaczanej $d o m (s)$ .

Pożytek z tego podziału na dwa etapy będzie taki, że będziemy umieli łatwo i elastycznie opisywać deklaracje zmiennych, przesłanianie identyfikatorów, itp. Tranzycje będą teraz postaci:

$I, s, E ⟶ s^{'}$

czyli instrukcja $I$ będzie modyfikować stan, ale nie będzie zmieniać środowiska $E$ . Dla czytelności będziemy zapisywać nasze reguły w następujący sposób:

$E ⊢ I, s ⟶ s^{'}$

podkreślając w ten sposób, że środowisko nie ulega zmianie. Ale należy pamiętać, że konfiguracja, w której "uruchamiamy" instrukcję $I$ składa się naprawdę z trójki $(I, s, E)$ .

Deklarując nową zmienną $x$ dodamy po prostu do $E$ parę $(x, l)$ , gdzie $l$ jest nową, nieużywaną dotychczas lokacją. Dla wygody zapisu załóżmy, że mamy do dyspozycji funkcję

$n e w l o c : 𝐒 𝐭 𝐨 𝐫 𝐞 \to 𝐋 𝐨 𝐜$

która zwraca jakąś nową, nieużywaną lokację. Formalnie wymagamy, by

$n e w l o c (s) \notin d o m (s)$

Dla ilustracji popatrzmy na przykładową regułę dla deklaracji.

$\frac{E ⊢ e, s ⟶ n E [x \mapsto l] ⊢ I, s [l \mapsto n] ⟶ s^{'}}{E ⊢ 𝐛 𝐞 𝐠 𝐢 𝐧 𝐯 𝐚 𝐫 x = e; I 𝐞 𝐧 𝐝, s ⟶ s^{'}} gdzie l = n e w l o c (s)$

Zauważmy, że stan $s^{'}$ po zakończeniu instrukcji $𝐛 𝐞 𝐠 𝐢 𝐧 𝐯 𝐚 𝐫 x = e; I 𝐞 𝐧 𝐝$ zawiera informację o zmiennej lokalnej $x$ , tzn. $s (l)$ jest określone. Ale lokacja $l$ jest "nieosiągalna" w środowisku $E$ , gdyż para $x \mapsto l$ została dodana tylko do środowiska, w którym ewaluuje się wnętrze bloku, a środowisko $E$ całego bloku nie jest modyfikowane.

Poniżej przedstawiamy reguły dla pozostałych instrukcji. Przede wszystkim złożenie sekwencyjne:

$\frac{E ⊢ I_{1}, s ⟶ s^{'} E, ⊢ I_{2}, s^{'} ⟶ s^{″}}{E ⊢ I_{1}; I_{2}, s ⟶ s^{″}}$

Reguła ta uzmysławia nam różnicę pomiędzy środowiskiem a stanem: środowisko pozostaje to samo, gdy przechodzimy od jednej instrukcji do następnej, a stan oczywiście ewoluuje wraz ze zmieniającymi się wartościami zmiennych.

Reguły dla przypisania, instrukcji warunkowej i pętli nie przedstawiają żadnych nowych trudności. Musimy tylko najpierw ustalić postać reguł dla wyrażeń:

$E ⊢ e, s ⟶ n$

która jest zupełnie naturalna w naszym podejściu opartym o środowiska i stany. Reguły mogą wyglądać np. tak:

$\frac{E ⊢ e, s ⟶ n}{E ⊢ x : = e, s ⟶ s [x \mapsto n]} E ⊢ 𝐬 𝐤 𝐢 𝐩, s ⟶ s$

$\frac{E ⊢ b, s ⟶ 𝐭 𝐫 𝐮 𝐞 E ⊢ I_{1}, s ⟶ s^{'}}{E ⊢ 𝐢 𝐟 b 𝐭 𝐡 𝐞 𝐧 I_{1} 𝐞 𝐥 𝐬 𝐞 I_{2}, s ⟶ s^{'}} \frac{E ⊢ b, s ⟶ 𝐟 𝐚 𝐥 𝐬 𝐞 E ⊢ I_{2}, s ⟶ s^{'}}{E ⊢ 𝐢 𝐟 b 𝐭 𝐡 𝐞 𝐧 I_{1} 𝐞 𝐥 𝐬 𝐞 I_{2}, s ⟶ s^{'}}$

$\frac{E ⊢ 𝐢 𝐟 b 𝐭 𝐡 𝐞 𝐧 (𝐰 𝐡 𝐢 𝐥 𝐞 b 𝐝 𝐨 I) 𝐞 𝐥 𝐬 𝐞 𝐬 𝐤 𝐢 𝐩, s ⟶ s^{'}}{E ⊢ 𝐰 𝐡 𝐢 𝐥 𝐞 b 𝐝 𝐨 I, s ⟶ s^{'}}$

Reguły dla wyrażeń są oczywiste:

$E ⊢ n, s ⟶ n E ⊢ x, s ⟶ n o ile E (x) = l \in 𝐋 𝐨 𝐜 i s (l) = n$

i tak dalej -- pomijamy pozostałe reguły.

Wariant 3 (dealokacja)

Przypomnijmy sobie semantykę bloku

$\frac{E ⊢ e, s ⟶ n E [x \mapsto l] ⊢ I, s [l \mapsto n] ⟶ s^{'}}{E ⊢ 𝐛 𝐞 𝐠 𝐢 𝐧 𝐯 𝐚 𝐫 x = e; I 𝐞 𝐧 𝐝, s ⟶ s^{'}} gdzie l = n e w l o c (s)$

i zastanówmy się, jak "posprzątać" po zakończeniu wykonania bloku, tzn. zwolnić lokację $l$ , która była używana tylko w tym bloku i w związku z tym nie będzie już potrzebna. Oznaczałoby to przywrócenie lokacji $l$ do puli wolnych (nieużywanych) lokacji.

Zmodyfikowana reguła dla instrukcji bloku powinna wyglądać mniej więcej tak:

$\frac{E ⊢ d, s ⟶ (E^{'}, s^{'}) E^{'} ⊢ I, s^{'} ⟶ s^{″}}{E ⊢ 𝐛 𝐞 𝐠 𝐢 𝐧 d; I 𝐞 𝐧 𝐝, s ⟶ \bar{s}}$

gdzie $\bar{s}$ to stan $s^{″}$ "okrojony" do dziedziny stanu $s$ . Powinniśmy po prostu przywrócić nieokreśloność stanu dla lokacji $l$ . Natomiast oczywiście nie ma potrzeby dealokownia środowiska! Oto rozwiązanie:

$\frac{E ⊢ e, s ⟶ n E [x \mapsto l] ⊢ I, s [l \mapsto n] ⟶ s^{'}}{E ⊢ 𝐛 𝐞 𝐠 𝐢 𝐧 𝐯 𝐚 𝐫 x = e; I 𝐞 𝐧 𝐝, s ⟶ s^{'} ∖ {(l, s^{'} (l))}} gdzie l = n e w l o c (s)$

Zadania domowe

Ćwiczenie 1

Napisz semantykę naturalną dla następującego rozszerzenia języka TINY:

$I : : = \dots | 𝐭 𝐡 𝐫 𝐨 𝐰 x | 𝐭 𝐫 𝐲 I_{1} 𝐜 𝐚 𝐭 𝐜 𝐡 e x c I_{2}$

$e x c : : = x | 𝐚 𝐧 𝐲$

Instrukcja $𝐭 𝐡 𝐫 𝐨 𝐰 x$ oznacza podniesienie wyjątku o nazwie $x$ . Instrukcja $I = 𝐭 𝐫 𝐲 I_{1} 𝐜 𝐚 𝐭 𝐜 𝐡 e x c I_{2}$ wykonuje $I_{1}$ . Jeśli podczas wykonania $I_{1}$ zostanie podniesiony wyjątek $x$ , i $e x c = x$ albo $e x c = 𝐚 𝐧 𝐲$ , to następuje przerwanie $I_{1}$ i sterowanie zostaje przeniesione do $I_{2}$ (następuje obsługa wyjątku). Jeśli zaś podczas wykonania $I_{1}$ zostanie podniesiony wyjątek $x$ oraz $e x c \neq x$ i $e x c \neq 𝐚 𝐧 𝐲$ , to obsługa wyjątku przekazana jest do najbliższej instrukcji $𝐭 𝐫 𝐲$ , otaczającej $I$ . Umawiamy się, że $𝐭 𝐫 𝐲 I_{1} 𝐜 𝐚 𝐭 𝐜 𝐡 e x c I_{2}$ otacza $I_{1}$ i wszystkie instrukcje wewnątrz $I_{1}$ , ale nie otacza $I_{2}$ .

Ćwiczenie 2

Zaproponuj modyfikację semantyki, w której deklaracja jest wykonywana "równolegle", analogicznie do przypisania równoległego. Przy takiej semantyce kolejność poszczególnych deklaracji powinna być nieistotna.

@@ Linia 8: / Linia 8: @@
-== Semantyka naturalna pewnej instrukcji <math>\mathbf{for}\,</math> ==
+== Semantyka naturalna pewnej instrukcji <math>\mathbf{for}\ </math>, ==
@@ Linia 25: / Linia 25: @@
 Znaczenie instrukcji <math>\mathbf{for}\, x = e_1 \,\mathbf{to}\, e_2 \,\mathbf{try}\, I_1 \,\mathbf{else}\, I_2</math> jest następujące.
 Obliczamy wartości wyrażeń <math>e_1</math> i <math>e_2</math>. Jeśli pierwsza z nich jest mniejsza od lub równa drugiej, podstawiamy pierwszą wartość (wartość wyrażenia <math>e_1</math>) na zmienną <math>x</math> i uruchamiamy <math>I_1</math>.
-Jeśli w <math>I_1</math> nie zostanie napotkana instrukcja <math>\mathbf{fail}</math>, kończymy instrukcję <math>\mathbf{for}\,</math> i przyracamy wartość zmiennej <math>x</math>
+Jeśli w <math>I_1</math> nie zostanie napotkana instrukcja <math>\mathbf{fail}</math>, kończymy instrukcję <math>\mathbf{for}\ </math>, i przyracamy wartość zmiennej <math>x</math>
 sprzed tej instrukcji.
 Natomiast jeśli w <math>I_1</math> zostanie napotkana instrukcja <math>\mathbf{fail}</math>, podstawiamy na <math>x</math> kolejną, o jeden większą wartość, przywracamy wartości wszystkich
-pozostałych zmiennych sprzed instrukcji <math>\mathbf{for}\,</math> i ponownie wykonujemy <math>I_1</math>.
+pozostałych zmiennych sprzed instrukcji <math>\mathbf{for}\ </math>, i ponownie wykonujemy <math>I_1</math>.
 Powtarzamy w ten sposób, aż <math>I_1</math> zakończy się nie napotkawszy <math>\mathbf{fail}</math>, albo wartość zmiennej <math>x</math> przekroczy wartość wyrażenia <math>e_2</math> obliczoną na początku.
-W pierwszym przypadku kończymy instrukcję <math>\mathbf{for}\,</math> i przyracamy wartość zmiennej <math>x</math> sprzed tej instrukcji.
+W pierwszym przypadku kończymy instrukcję <math>\mathbf{for}\ </math>, i przyracamy wartość zmiennej <math>x</math> sprzed tej instrukcji.
-W drugim przywracamy wartości wszystkich zmiennych sprzed instrukcji <math>\mathbf{for}\,</math> i uruchamiamy <math>I_2</math>.
+W drugim przywracamy wartości wszystkich zmiennych sprzed instrukcji <math>\mathbf{for}\ </math>, i uruchamiamy <math>I_2</math>.
 }}
@@ Linia 40: / Linia 40: @@
   x := 0; y := 1;
-  <math>\mathbf{for}\,</math> x := 1 <math>\,\mathbf{to}\,</math> 5 <math>\,\mathbf{try}\,</math>
+  <math>\mathbf{for}\ </math>, x := 1 <math>\,\mathbf{to}\ </math>, 5 <math>\,\mathbf{try}\ </math>,
     y := y+1;
-    <math>\mathbf{if}\,</math> x <= 4 <math>\,\mathbf{then}\, \mathbf{fail} \,\mathbf{else}\,</math> z:= x
+    <math>\mathbf{if}\ </math>, x <= 4 <math>\,\mathbf{then}\, \mathbf{fail} \,\mathbf{else}\ </math>, z:= x
   <math>\,\mathbf{else}\, \mathbf{skip}</math>
@@ Linia 57: / Linia 57: @@
 <math>
-I, s \,\longrightarrow\, s' \quad \quad \quad e, s \,\longrightarrow\, n.
+I, s \,\longrightarrow\, s' \quad \quad \quad e, s \,\longrightarrow\, n</math>
-</math>
 Zacznijmy od najprostszego przypadku, gdy nie ma wogóle potrzeby uruchamiania instrukcji wewnętrznej <math>I_1</math>, ponieważ wartość wyrażenia <math>e_1</math> jest większa od <math>e_2</math>:
@@ Linia 69: / Linia 68: @@
        I_2, s \,\longrightarrow\, s'}
       {\mathbf{for}\, x = e_1 \,\mathbf{to}\, e_2 \,\mathbf{try}\, I_1 \,\mathbf{else}\, I_2, s \,\longrightarrow\, s'}
-\quad \mbox{ o ile } n_1 > n_2.
+\quad \mbox{ o ile } n_1 > n_2</math>
-</math>
 Po prostu uruchamiamy instrukcję <math>I_2</math> w stanie <math>s</math>, ignorując <math>I_1</math>.
@@ Linia 84: / Linia 82: @@
        I_1, s[x \mapsto n_1]  \,\longrightarrow\, s'}
       {\mathbf{for}\, x = e_1 \,\mathbf{to}\, e_2 \,\mathbf{try}\, I_1 \,\mathbf{else}\, I_2, s \,\longrightarrow\, s'[x \mapsto s(x)]}
-\quad \mbox{ o ile } n_1 \leq n_2.
+\quad \mbox{ o ile } n_1 \leq n_2</math>
-</math>
 Tym razem uruchamiamy instrukcję <math>I_1</math>, podstawiając na zmienną <math>x</math> wartość <math>n_1</math>.
@@ Linia 94: / Linia 91: @@
 <math>
-I, s \,\longrightarrow\, \mbox{było-}\mathbf{fail}.
+I, s \,\longrightarrow\, \mbox{było-}\mathbf{fail}</math>
-</math>
 Mówiąc formalnie, poszerzamy zbiór konfiguracji o jeden element <math>\mbox{było-}\mathbf{fail}</math>.
 Zauważmy, że po prawej stronie tranzycji nie ma wogóle stanu.
-Nie potrzebujemy go dla opisania semantyki instrukcji <math>\mathbf{for}\,</math>: jeśli wystąpi <math>\mathbf{fail}</math>, powtarzamy <math>I_1</math> dla większej o <math>1</math> wartości zmiennej <math>x</math>, ale pozostałym zmiennym przywracamy wartość ''sprzed'' <math>I_1</math>.
+Nie potrzebujemy go dla opisania semantyki instrukcji <math>\mathbf{for}\ </math>,: jeśli wystąpi <math>\mathbf{fail}</math>, powtarzamy <math>I_1</math> dla większej o <math>1</math> wartości zmiennej <math>x</math>, ale pozostałym zmiennym przywracamy wartość ''sprzed'' <math>I_1</math>.
 A więc załóżmy, że
-<math>I_1, s[x \mapsto n_1] \,\longrightarrow\, \mbox{było-}\mathbf{fail}.</math>
+<math>I_1, s[x \mapsto n_1] \,\longrightarrow\, \mbox{było-}\mathbf{fail}</math>.
-W takiej sytuacji powinniśmy przypisać <math>n_1 + 1</math> na zmienną <math>x</math> i spróbować ponownie wykonać <math>I_1</math> przy wartościach wszystkich pozostałych zmiennych, takich jak na początku instrukcji <math>\mathbf{for}\,</math>.
+W takiej sytuacji powinniśmy przypisać <math>n_1 + 1</math> na zmienną <math>x</math> i spróbować ponownie wykonać <math>I_1</math> przy wartościach wszystkich pozostałych zmiennych, takich jak na początku instrukcji <math>\mathbf{for}\ </math>,.
 Powtarzamy ten schemat aż do skutku, tzn. aż do mementu, gdy zaistnieje któraś z poprzednich dwóch (prostych) sytuacji.
 Oto odpowiednia reguła:
@@ Linia 117: / Linia 113: @@
        \mathbf{for}\, x = e_1 + 1 \,\mathbf{to}\, e_2 \,\mathbf{try}\, I_1 \,\mathbf{else}\, I_2, s \,\longrightarrow\, s'}
       {\mathbf{for}\, x = e_1 \,\mathbf{to}\, e_2 \,\mathbf{try}\, I_1 \,\mathbf{else}\, I_2, s \,\longrightarrow\, s'}
-\quad \mbox{ o ile } n_1 \leq n_2.
+\quad \mbox{ o ile } n_1 \leq n_2</math>
-</math>
 Zwróćmy uwagę na pewnien niezwykle istotny szczegół: po zakończeniu wykonania instrukcji <math>\mathbf{for}\, x = e_1 + 1 \,\mathbf{to}\, e_2 \,\mathbf{try}\, I_1 \,\mathbf{else}\, I_2</math> otrzymujemy stan <math>s'</math>, w którym '''nie przywracamy''' wartości zmiennej <math>x</math>.
 Gdybyśmy tak zrobili, tzn. gdybyśmy zastąpili <math>s'</math> przez <math>s'[x \mapsto s(x)]</math>, nasze semantyka byłaby niepoprawna.
 Dlaczego? Dlatego, że nie wiemy tak naprawdę, czy powinniśmy przywracać wartość zmiennej <math>x</math>, czy nie.
-Jeśli ostatecznie nasza instrukcja <math>\mathbf{for}\,</math> zakończyła się przez bezbłędne zakończenie instrukcji <math>I_1</math> (przypadek drugi), to powinniśmy to zrobić; ale jeśli zakończyła się wykonaniem instrukcji <math>I_2</math> (przypadek pierwszy), powinniśmy pozostawić wartość zmiennej <math>x</math> taką, jaka jest ona po zakończeniu <math>I_2</math>.
+Jeśli ostatecznie nasza instrukcja <math>\mathbf{for}\ </math>, zakończyła się przez bezbłędne zakończenie instrukcji <math>I_1</math> (przypadek drugi), to powinniśmy to zrobić; ale jeśli zakończyła się wykonaniem instrukcji <math>I_2</math> (przypadek pierwszy), powinniśmy pozostawić wartość zmiennej <math>x</math> taką, jaka jest ona po zakończeniu <math>I_2</math>.
 A zatem w powyższej regule dla przypadku trzeciego nie przywracamy wartości zmiennej <math>x</math>; jeśli było to konieczne, to zostało już wykonane "głębiej", dzięki regule dla przypadku drugiego oraz dzięki temu, że instrukcja <math>\mathbf{for}\, x = e_1 + 1 \,\mathbf{to}\, e_2 \,\mathbf{try}\, I_1 \,\mathbf{else}\, I_2</math> wykonywana jest w orginalnym stanie <math>s</math>, a nie w stanie, w którym kończy się <math>I_1</math> (tego ostatniego stanu nawet nie znamy).
@@ Linia 134: / Linia 129: @@
 </math>
-oraz aby wystąpienie <math>\mathbf{fail}</math> umiejscowione gdzieś "głęboko" zostało rozpropagowane do najbliższej otaczającej instrukcji <math>\mathbf{for}\,</math>.
+oraz aby wystąpienie <math>\mathbf{fail}</math> umiejscowione gdzieś "głęboko" zostało rozpropagowane do najbliższej otaczającej instrukcji <math>\mathbf{for}\ </math>,.
 Jeśli pojawił się <math>\mathbf{fail}</math>, powinniśmy zaniechać dalszego wykonania instrukcji, a w przypadku pętli, powinniśmy zaniechać dalszego iterowania tej pętli.
 Oto odpowiednie reguły:
@@ Linia 164: / Linia 159: @@
 Widać podobieństwo do analogicznych reguł dla pętli <math>\mathbf{loop}\, I</math>, którą zajmowaliśmy się na wcześniejszych zajęciach.
-Zauważmy, że jeśli <math>\mathbf{fail}</math> zostało wykonane poza jakąkolwiek pętlą <math>\mathbf{for}\,</math>, to program "zakończy się" w konfiguracji <math>\mbox{było-}\mathbf{fail}</math>.
+Zauważmy, że jeśli <math>\mathbf{fail}</math> zostało wykonane poza jakąkolwiek pętlą <math>\mathbf{for}\ </math>,, to program "zakończy się" w konfiguracji <math>\mbox{było-}\mathbf{fail}</math>.
 Możemy zatem tę właśnie konfigurację uznać za konfigurację końcową, informującą o porażce wykonania programu.
@@ Linia 187: / Linia 182: @@
-{{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">
 '''Wariant 1 (tylko stan)'''
@@ Linia 234: / Linia 229: @@
 <math>
-\mathbf{Store} = \mathbf{Loc} \to_{\mathrm{fin}} \mathbf{Num}.
+\mathbf{Store} = \mathbf{Loc} \to_{\mathrm{fin}} \mathbf{Num}</math>
-</math>
 Dla ścisłości używamy innej nazwy (<math>\mathbf{Store}</math>), ale będziemy zwykle używać podobnych symboli jak dotychczas <math>s, s', s_1, \ldots \in \mathbf{Store}</math> itp. do nazywania stanów.
@@ Linia 274: / Linia 268: @@
 <math>
-\mathtt{newloc}(s) \notin \mathrm{dom}(s).
+\mathtt{newloc}(s) \notin \mathrm{dom}(s)</math>
-</math>
 Dla ilustracji popatrzmy na przykładową regułę dla deklaracji.
@@ Linia 283: / Linia 276: @@
        E[x \mapsto l] \,\vdash\, I, s[l \mapsto n] \,\longrightarrow\, s'}
       {E \,\vdash\, \mathbf{begin}\, \mathbf{var}\, x=e;\, I \,\mathbf{end}, s \,\longrightarrow\, s'}
-\quad \mbox{ gdzie } l = \mathtt{newloc}(s).
+\quad \mbox{ gdzie } l = \mathtt{newloc}(s)</math>
-</math>
 Zauważmy, że stan <math>s'</math> po zakończeniu instrukcji <math>\mathbf{begin}\, \mathbf{var}\, x=e;\, I \,\mathbf{end}</math> zawiera informację o zmiennej lokalnej <math>x</math>, tzn. <math>s(l)</math> jest określone.
@@ Linia 380: / Linia 372: @@
        E[x \mapsto l] \,\vdash\, I, s[l \mapsto n] \,\longrightarrow\, s'}
       {E \,\vdash\, \mathbf{begin}\, \mathbf{var}\, x=e;\, I \,\mathbf{end}, s \,\longrightarrow\, s' \setminus \{ (l, s'(l)) \}}
-\quad \mbox{ gdzie } l = \mathtt{newloc}(s).
+\quad \mbox{ gdzie } l = \mathtt{newloc}(s)</math>
-</math>
 </div></div>
-}}
 == Zadania domowe ==
@@ Linia 395: / Linia 385: @@
 <math>
 I \, ::= \,\,
-       \ldotes \,\,|\,\,
+       \ldots \,\,|\,\,
         \mathbf{throw}\, x \,\,|\,\,
         \,\mathbf{try}\, I_1 \,\mathbf{catch}\, exc\, I_2
@@ Linia 409: / Linia 399: @@
 Instrukcja <math>I = \,\mathbf{try}\, I_1 \,\mathbf{catch}\, exc\, I_2</math> wykonuje <math>I_1</math>.
 Jeśli podczas wykonania <math>I_1</math> zostanie podniesiony wyjątek <math>x</math>, i <math>exc = x</math> albo <math>exc = \mathbf{any}</math>, to następuje przerwanie <math>I_1</math> i sterowanie zostaje przeniesione do <math>I_2</math> (następuje ''obsługa wyjątku'').
-Jeśli zaś podczas wykonania <math>I_1</math> zostanie podniesiony wyjątek <math>x</math> oraz <math>exc \neq x</math> i <math>exc \neq \mathbf{any}</math>, to obsługa wyjątku przekazana jest do najbliższej instrukcji <math>\,\mathbf{try}\,</math> otaczającej <math>I</math>.
+Jeśli zaś podczas wykonania <math>I_1</math> zostanie podniesiony wyjątek <math>x</math> oraz <math>exc \neq x</math> i <math>exc \neq \mathbf{any}</math>, to obsługa wyjątku przekazana jest do najbliższej instrukcji <math>\,\mathbf{try}\ </math>, otaczającej <math>I</math>.
 Umawiamy się, że <math>\,\mathbf{try}\, I_1 \,\mathbf{catch}\, exc\, I_2</math> ''otacza'' <math>I_1</math> i wszystkie instrukcje wewnątrz <math>I_1</math>, ale ''nie'' otacza <math>I_2</math>.
 }}

Semantyka i weryfikacja programów/Ćwiczenia 5: Różnice pomiędzy wersjami

Aktualna wersja na dzień 21:30, 11 wrz 2023

Spis treści

Zawartość

Semantyka naturalna pewnej instrukcji $𝐟 𝐨 𝐫$ ,

Semantyka naturalna bloków

Zadania domowe

Menu nawigacyjne

Działania na stronie

Opcje strony

Narzędzia osobiste

Nawigacja

Szukaj

Narzędzia

Semantyka i weryfikacja programów/Ćwiczenia 5: Różnice pomiędzy wersjami

Aktualna wersja na dzień 21:30, 11 wrz 2023

Zawartość

Semantyka naturalna pewnej instrukcji 𝐟𝐨𝐫 ,

Semantyka naturalna bloków

Zadania domowe

Menu nawigacyjne

Szukaj

Semantyka naturalna pewnej instrukcji $𝐟 𝐨 𝐫$ ,