Semantyka i weryfikacja programów/Ćwiczenia 5

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 $\mathbf{𝐟}\mathbf{𝐨}\mathbf{𝐫}$

Ćwiczenie 1

Rozszerzamy język TINY następująco:

$I::=\dots |\mathbf{𝐟}\mathbf{𝐨}\mathbf{𝐫}x=e_1\mathbf{𝐭}\mathbf{𝐨}{e}_2\mathbf{𝐭}\mathbf{𝐫}\mathbf{𝐲}{I}_1\mathbf{𝐞}\mathbf{𝐥}\mathbf{𝐬}\mathbf{𝐞}{I}_2|\mathbf{𝐟}\mathbf{𝐚}\mathbf{𝐢}\mathbf{𝐥}$

Znaczenie instrukcji $\mathbf{𝐟}\mathbf{𝐨}\mathbf{𝐫}x=e_1\mathbf{𝐭}\mathbf{𝐨}{e}_2\mathbf{𝐭}\mathbf{𝐫}\mathbf{𝐲}{I}_1\mathbf{𝐞}\mathbf{𝐥}\mathbf{𝐬}\mathbf{𝐞}{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 $\mathbf{𝐟}\mathbf{𝐚}\mathbf{𝐢}\mathbf{𝐥}$, kończymy instrukcję $\mathbf{𝐟}\mathbf{𝐨}\mathbf{𝐫}$ i przyracamy wartość zmiennej $x$ sprzed tej instrukcji. Natomiast jeśli w $I_1$ zostanie napotkana instrukcja $\mathbf{𝐟}\mathbf{𝐚}\mathbf{𝐢}\mathbf{𝐥}$, podstawiamy na $x$ kolejną, o jeden większą wartość, przywracamy wartości wszystkich pozostałych zmiennych sprzed instrukcji $\mathbf{𝐟}\mathbf{𝐨}\mathbf{𝐫}$ i ponownie wykonujemy $I_1$. Powtarzamy w ten sposób, aż $I_1$ zakończy się nie napotkawszy $\mathbf{𝐟}\mathbf{𝐚}\mathbf{𝐢}\mathbf{𝐥}$, albo wartość zmiennej $x$ przekroczy wartość wyrażenia $e_2$ obliczoną na początku. W pierwszym przypadku kończymy instrukcję $\mathbf{𝐟}\mathbf{𝐨}\mathbf{𝐫}$ i przyracamy wartość zmiennej $x$ sprzed tej instrukcji. W drugim przywracamy wartości wszystkich zmiennych sprzed instrukcji $\mathbf{𝐟}\mathbf{𝐨}\mathbf{𝐫}$ i uruchamiamy $I_2$.

Przykład

Oto przykładowy program:

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

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^{\prime }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^{\prime }}{\mathbf{𝐟}\mathbf{𝐨}\mathbf{𝐫}x=e_1\mathbf{𝐭}\mathbf{𝐨}{e}_2\mathbf{𝐭}\mathbf{𝐫}\mathbf{𝐲}{I}_1\mathbf{𝐞}\mathbf{𝐥}\mathbf{𝐬}\mathbf{𝐞}{I}_2,s⟶s^{\prime }}\text{ 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\le n_2$, a wykonanie instrukcji wewnętrznej $I_1$ kończy się sukcesem, tzn. nie następuje wywołanie instrukcji $\mathbf{𝐟}\mathbf{𝐚}\mathbf{𝐢}\mathbf{𝐥}$. 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^{\prime }}{\mathbf{𝐟}\mathbf{𝐨}\mathbf{𝐫}x=e_1\mathbf{𝐭}\mathbf{𝐨}{e}_2\mathbf{𝐭}\mathbf{𝐫}\mathbf{𝐲}{I}_1\mathbf{𝐞}\mathbf{𝐥}\mathbf{𝐬}\mathbf{𝐞}{I}_2,s⟶s^{\prime }[x\mapsto s(x)]}\text{ o ile }{n}_1\le 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\le n_2$, a wykonanie instrukcji $I_1$ zakończyło się wykonaniem instrukcji $\mathbf{𝐟}\mathbf{𝐚}\mathbf{𝐢}\mathbf{𝐥}$ gdzieś wewnątrz $I_1$. Aby poprawnie opisać takie zdarzenie, potrzebujemy dodatkowych tranzycji postaci:

$I,s⟶\text{było-}\mathbf{𝐟}\mathbf{𝐚}\mathbf{𝐢}\mathbf{𝐥}.$

Mówiąc formalnie, poszerzamy zbiór konfiguracji o jeden element $\text{było-}\mathbf{𝐟}\mathbf{𝐚}\mathbf{𝐢}\mathbf{𝐥}$. Zauważmy, że po prawej stronie tranzycji nie ma wogóle stanu. Nie potrzebujemy go dla opisania semantyki instrukcji $\mathbf{𝐟}\mathbf{𝐨}\mathbf{𝐫}$: jeśli wystąpi $\mathbf{𝐟}\mathbf{𝐚}\mathbf{𝐢}\mathbf{𝐥}$, 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]⟶\text{było-}\mathbf{𝐟}\mathbf{𝐚}\mathbf{𝐢}\mathbf{𝐥}.$

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 $\mathbf{𝐟}\mathbf{𝐨}\mathbf{𝐫}$. 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]⟶\text{było-}\mathbf{𝐟}\mathbf{𝐚}\mathbf{𝐢}\mathbf{𝐥}\mathbf{𝐟}\mathbf{𝐨}\mathbf{𝐫}x=e_1+1\mathbf{𝐭}\mathbf{𝐨}{e}_2\mathbf{𝐭}\mathbf{𝐫}\mathbf{𝐲}{I}_1\mathbf{𝐞}\mathbf{𝐥}\mathbf{𝐬}\mathbf{𝐞}{I}_2,s⟶s^{\prime }}{\mathbf{𝐟}\mathbf{𝐨}\mathbf{𝐫}x=e_1\mathbf{𝐭}\mathbf{𝐨}{e}_2\mathbf{𝐭}\mathbf{𝐫}\mathbf{𝐲}{I}_1\mathbf{𝐞}\mathbf{𝐥}\mathbf{𝐬}\mathbf{𝐞}{I}_2,s⟶s^{\prime }}\text{ o ile }{n}_1\le n_2.$

Zwróćmy uwagę na pewnien niezwykle istotny szczegół: po zakończeniu wykonania instrukcji $\mathbf{𝐟}\mathbf{𝐨}\mathbf{𝐫}x=e_1+1\mathbf{𝐭}\mathbf{𝐨}{e}_2\mathbf{𝐭}\mathbf{𝐫}\mathbf{𝐲}{I}_1\mathbf{𝐞}\mathbf{𝐥}\mathbf{𝐬}\mathbf{𝐞}{I}_2$ otrzymujemy stan $s^{\prime }$, w którym nie przywracamy wartości zmiennej $x$. Gdybyśmy tak zrobili, tzn. gdybyśmy zastąpili $s^{\prime }$ przez $s^{\prime }[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 $\mathbf{𝐟}\mathbf{𝐨}\mathbf{𝐫}$ 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 $\mathbf{𝐟}\mathbf{𝐨}\mathbf{𝐫}x=e_1+1\mathbf{𝐭}\mathbf{𝐨}{e}_2\mathbf{𝐭}\mathbf{𝐫}\mathbf{𝐲}{I}_1\mathbf{𝐞}\mathbf{𝐥}\mathbf{𝐬}\mathbf{𝐞}{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 $\mathbf{𝐟}\mathbf{𝐨}\mathbf{𝐫}x=e_1+1\mathbf{𝐭}\mathbf{𝐨}{e}_2\mathbf{𝐭}\mathbf{𝐫}\mathbf{𝐲}{I}_1\mathbf{𝐞}\mathbf{𝐥}\mathbf{𝐬}\mathbf{𝐞}{I}_2,s⟶s^{\prime }$ 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ć $\text{było-}\mathbf{𝐟}\mathbf{𝐚}\mathbf{𝐢}\mathbf{𝐥}$:

$\mathbf{𝐟}\mathbf{𝐚}\mathbf{𝐢}\mathbf{𝐥},s⟶\text{było-}\mathbf{𝐟}\mathbf{𝐚}\mathbf{𝐢}\mathbf{𝐥}$

oraz aby wystąpienie $\mathbf{𝐟}\mathbf{𝐚}\mathbf{𝐢}\mathbf{𝐥}$ umiejscowione gdzieś "głęboko" zostało rozpropagowane do najbliższej otaczającej instrukcji $\mathbf{𝐟}\mathbf{𝐨}\mathbf{𝐫}$. Jeśli pojawił się $\mathbf{𝐟}\mathbf{𝐚}\mathbf{𝐢}\mathbf{𝐥}$, 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⟶\text{było-}\mathbf{𝐟}\mathbf{𝐚}\mathbf{𝐢}\mathbf{𝐥}}{I_1;I_2,s⟶\text{było-}\mathbf{𝐟}\mathbf{𝐚}\mathbf{𝐢}\mathbf{𝐥}}\frac{I_1,s⟶s^{\prime }{I}_2,s^{\prime }⟶\text{było-}\mathbf{𝐟}\mathbf{𝐚}\mathbf{𝐢}\mathbf{𝐥}}{I_1;I_2,s⟶\text{było-}\mathbf{𝐟}\mathbf{𝐚}\mathbf{𝐢}\mathbf{𝐥}}$

$\frac{b,s⟶\mathbf{𝐭}\mathbf{𝐫}\mathbf{𝐮}\mathbf{𝐞}{I}_1,s⟶\text{było-}\mathbf{𝐟}\mathbf{𝐚}\mathbf{𝐢}\mathbf{𝐥}}{\mathbf{𝐢}\mathbf{𝐟}b\mathbf{𝐭}\mathbf{𝐡}\mathbf{𝐞}\mathbf{𝐧}{I}_1\mathbf{𝐞}\mathbf{𝐥}\mathbf{𝐬}\mathbf{𝐞}{I}_2,s⟶\text{było-}\mathbf{𝐟}\mathbf{𝐚}\mathbf{𝐢}\mathbf{𝐥}}\text{ i analogicznie gdy }b,s⟶\mathbf{𝐟}\mathbf{𝐚}\mathbf{𝐥}\mathbf{𝐬}\mathbf{𝐞}$

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

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

Zauważmy, że jeśli $\mathbf{𝐟}\mathbf{𝐚}\mathbf{𝐢}\mathbf{𝐥}$ zostało wykonane poza jakąkolwiek pętlą $\mathbf{𝐟}\mathbf{𝐨}\mathbf{𝐫}$, to program "zakończy się" w konfiguracji $\text{było-}\mathbf{𝐟}\mathbf{𝐚}\mathbf{𝐢}\mathbf{𝐥}$. 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 |\mathbf{𝐛}\mathbf{𝐞}\mathbf{𝐠}\mathbf{𝐢}\mathbf{𝐧}\mathbf{𝐯}\mathbf{𝐚}\mathbf{𝐫}x=e;I\mathbf{𝐞}\mathbf{𝐧}\mathbf{𝐝}$

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

{{{3}}}

Zadania domowe

Ćwiczenie 1

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

Parser nie mógł rozpoznać (nieznana funkcja „\ldotes”): {\displaystyle I \, ::= \,\, \ldotes \,\,|\,\, \mathbf{throw}\, x \,\,|\,\, \,\mathbf{try}\, I_1 \,\mathbf{catch}\, exc\, I_2 }

$exc::=x|\mathbf{𝐚}\mathbf{𝐧}\mathbf{𝐲}$

Instrukcja $\mathbf{𝐭}\mathbf{𝐡}\mathbf{𝐫}\mathbf{𝐨}\mathbf{𝐰}x$ oznacza podniesienie wyjątku o nazwie $x$. Instrukcja $I=\mathbf{𝐭}\mathbf{𝐫}\mathbf{𝐲}{I}_1\mathbf{𝐜}\mathbf{𝐚}\mathbf{𝐭}\mathbf{𝐜}\mathbf{𝐡}exc{I}_2$ wykonuje $I_1$. Jeśli podczas wykonania $I_1$ zostanie podniesiony wyjątek $x$, i $exc=x$ albo $exc=\mathbf{𝐚}\mathbf{𝐧}\mathbf{𝐲}$, 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 $exc\ne x$ i $exc\ne \mathbf{𝐚}\mathbf{𝐧}\mathbf{𝐲}$, to obsługa wyjątku przekazana jest do najbliższej instrukcji $\mathbf{𝐭}\mathbf{𝐫}\mathbf{𝐲}$ otaczającej $I$. Umawiamy się, że $\mathbf{𝐭}\mathbf{𝐫}\mathbf{𝐲}{I}_1\mathbf{𝐜}\mathbf{𝐚}\mathbf{𝐭}\mathbf{𝐜}\mathbf{𝐡}exc{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.