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 nową instrukcję pętli $\mathbf{𝐥}\mathbf{𝐨}\mathbf{𝐨}\mathbf{𝐩}$ pozwalającą na niestrukturalne przerwanie lub wznowienie iteracji (instrukcje $\mathbf{𝐞}\mathbf{𝐱}\mathbf{𝐢}\mathbf{𝐭}$ i $\mathbf{𝐜}\mathbf{𝐨}\mathbf{𝐧}\mathbf{𝐭}\mathbf{𝐢}\mathbf{𝐧}\mathbf{𝐮}\mathbf{𝐞}$).

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

{{{3}}}

Ć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

{{{3}}}

Ćwiczenie 3

Rozszerz język Tiny o następującą instrukcję pętli:

$I::=\mathbf{𝐥}\mathbf{𝐨}\mathbf{𝐨}\mathbf{𝐩}I|\mathbf{𝐞}\mathbf{𝐱}\mathbf{𝐢}\mathbf{𝐭}|\mathbf{𝐜}\mathbf{𝐨}\mathbf{𝐧}\mathbf{𝐭}\mathbf{𝐢}\mathbf{𝐧}\mathbf{𝐮}\mathbf{𝐞}$

$\mathbf{𝐥}\mathbf{𝐨}\mathbf{𝐨}\mathbf{𝐩}I$ to instrukcja pętli, $I$ stanowi instrukcję wewnętrzną. Instrukcja $\mathbf{𝐞}\mathbf{𝐱}\mathbf{𝐢}\mathbf{𝐭}$ wychodzi z nabliższej pętli $\mathbf{𝐥}\mathbf{𝐨}\mathbf{𝐨}\mathbf{𝐩}$ i kontynuuje wykonanie programu od pierwszej instrukcji za tą pętlą. Instrukcje $\mathbf{𝐜}\mathbf{𝐨}\mathbf{𝐧}\mathbf{𝐭}\mathbf{𝐢}\mathbf{𝐧}\mathbf{𝐮}\mathbf{𝐞}$ 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

{{{3}}}

Rozwiązanie

{{{3}}}

Zadania domowe

Zadanie 1

Zaproponuj semantykę mało-krokową dla rozszerzeń języka Tiny, które studiowaliśmy powyżej.

Zadanie 2

Napisz semantyję naturalną dla nieznacznie rozszerzonej wersji instrukcji $\mathbf{𝐥}\mathbf{𝐨}\mathbf{𝐨}\mathbf{𝐩}$:

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

Identyfikator $x$ pełni tutaj rolę etykiety przypisanej instrukcji $\mathbf{𝐥}\mathbf{𝐨}\mathbf{𝐨}\mathbf{𝐩}$, jest też parametrem dwóch pozostałych instrukcji. $\mathbf{𝐞}\mathbf{𝐱}\mathbf{𝐢}\mathbf{𝐭}x$ kończy teraz najbliższą otaczającą pętlę $\mathbf{𝐥}\mathbf{𝐨}\mathbf{𝐨}\mathbf{𝐩}$ o etykiecie $x$. Podobnie $\mathbf{𝐜}\mathbf{𝐨}\mathbf{𝐧}\mathbf{𝐭}\mathbf{𝐢}\mathbf{𝐧}\mathbf{𝐮}\mathbf{𝐞}x$ wznawia najbliższą otaczającą pętlę o etykiecie $x$.

Przykład

x: $\mathbf{𝐥}\mathbf{𝐨}\mathbf{𝐨}\mathbf{𝐩}$
  a := 1; 
  y: $\mathbf{𝐥}\mathbf{𝐨}\mathbf{𝐨}\mathbf{𝐩}$
    $\mathbf{𝐞}\mathbf{𝐱}\mathbf{𝐢}\mathbf{𝐭}$ x;
    a := a-10;
  a := a+1;
a := a+2;

Program kończy działanie z wartością zmiennej $a=3$. Za pomocą wcięć określiliśmy, do wnętrza której pętli $\mathbf{𝐥}\mathbf{𝐨}\mathbf{𝐨}\mathbf{𝐩}$ 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ę $\mathbf{𝐥}\mathbf{𝐨}\mathbf{𝐨}\mathbf{𝐩}$, np. $\mathbf{𝐥}\mathbf{𝐨}\mathbf{𝐨}\mathbf{𝐩}I\mathbf{𝐞}\mathbf{𝐧}\mathbf{𝐝}\mathbf{𝐥}\mathbf{𝐨}\mathbf{𝐨}\mathbf{𝐩}$.

Zadanie 3

Napisz semantykę naturalną i mało-krokową dla rozszerzenia języka Tiny o wyrażenia z efektami ubocznymi:

$e::=\dots |\mathbf{𝐝}\mathbf{𝐨}I\mathbf{𝐭}\mathbf{𝐡}\mathbf{𝐞}\mathbf{𝐧}e|x:=e|x++|\dots$

Obliczenie wyrażenia $\mathbf{𝐝}\mathbf{𝐨}I\mathbf{𝐭}\mathbf{𝐡}\mathbf{𝐞}\mathbf{𝐧}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$.