Semantyka i weryfikacja programów/Ćwiczenia 3: Różnice pomiędzy wersjami
m Zastępowanie tekstu - "\Longrightarrow\" na "\Longrightarrow" |
|||
| Linia 198: | Linia 198: | ||
{e_1 / e_2, s \,\longrightarrow\, \mathtt{Blad}} | {e_1 / e_2, s \,\longrightarrow\, \mathtt{Blad}} | ||
\quad \quad | \quad \quad | ||
e_1 / 0, s \,\Longrightarrow | e_1 / 0, s \,\Longrightarrow, \mathtt{Blad}. | ||
</math> | </math> | ||
| Linia 210: | Linia 210: | ||
{e_1 / e_2, s \,\longrightarrow\, \mathtt{Blad}, s} | {e_1 / e_2, s \,\longrightarrow\, \mathtt{Blad}, s} | ||
\quad \quad | \quad \quad | ||
e_1 / 0, s \,\Longrightarrow | e_1 / 0, s \,\Longrightarrow, \mathtt{Blad}, s | ||
</math> | </math> | ||
| Linia 402: | Linia 402: | ||
<math> | <math> | ||
\mathbf{exit}, s \,\Longrightarrow | \mathbf{exit}, s \,\Longrightarrow, s, \mbox{było-}\mathbf{exit} | ||
\quad \quad | \quad \quad | ||
\mathbf{continue}, s \,\Longrightarrow | \mathbf{continue}, s \,\Longrightarrow, s, \mbox{było-}\mathbf{continue}. | ||
</math> | </math> | ||
| Linia 410: | Linia 410: | ||
<math> | <math> | ||
\frac{I_1, s \,\Longrightarrow | \frac{I_1, s \,\Longrightarrow, s', \mbox{było-}\mathbf{exit}} | ||
{I_1;\, I_2, s \,\Longrightarrow | {I_1;\, I_2, s \,\Longrightarrow, s', \mbox{było-}\mathbf{exit}} | ||
\quad \quad | \quad \quad | ||
\mbox{ i analogicznie dla } \mbox{było-}\mathbf{continue}. | \mbox{ i analogicznie dla } \mbox{było-}\mathbf{continue}. | ||
| Linia 422: | Linia 422: | ||
<math> | <math> | ||
\frac{I, s \,\Longrightarrow | \frac{I, s \,\Longrightarrow, s', \mbox{było-}\mathbf{exit}} | ||
{\mathbf{loop}\, I, s \,\Longrightarrow | {\mathbf{loop}\, I, s \,\Longrightarrow, s'} | ||
\quad \quad | \quad \quad | ||
\frac{I, s \,\Longrightarrow | \frac{I, s \,\Longrightarrow, s', \mbox{było-}\mathbf{continue}} | ||
{\mathbf{loop}\, I, s \,\Longrightarrow | {\mathbf{loop}\, I, s \,\Longrightarrow, \mathbf{loop}\, I, s'} | ||
</math> | </math> | ||
| Linia 439: | Linia 439: | ||
<math> | <math> | ||
\mathbf{loop}\, I, s \,\Longrightarrow | \mathbf{loop}\, I, s \,\Longrightarrow, I \,\mathbf{then}\, \mathbf{loop}\, I, s. | ||
</math> | </math> | ||
| Linia 445: | Linia 445: | ||
<math> | <math> | ||
\frac{I', s \,\Longrightarrow | \frac{I', s \,\Longrightarrow, s', \mbox{było-}\mathbf{exit}} | ||
{I' \,\mathbf{then}\, \mathbf{loop}\, I, s \,\Longrightarrow | {I' \,\mathbf{then}\, \mathbf{loop}\, I, s \,\Longrightarrow, s'} | ||
\quad \quad | \quad \quad | ||
\frac{I', s \,\Longrightarrow | \frac{I', s \,\Longrightarrow, s', \mbox{było-}\mathbf{continue}} | ||
{I' \,\mathbf{then}\, \mathbf{loop}\, I, s \,\Longrightarrow | {I' \,\mathbf{then}\, \mathbf{loop}\, I, s \,\Longrightarrow, \mathbf{loop}\, I, s'} | ||
\quad \quad | \quad \quad | ||
\frac{I', s \,\Longrightarrow | \frac{I', s \,\Longrightarrow, s'} | ||
{I' \,\mathbf{then}\, \mathbf{loop}\, I, s \,\Longrightarrow | {I' \,\mathbf{then}\, \mathbf{loop}\, I, s \,\Longrightarrow, \mathbf{loop}\, I, s'} | ||
</math> | </math> | ||
| Linia 458: | Linia 458: | ||
<math> | <math> | ||
\frac{I', s \,\Longrightarrow | \frac{I', s \,\Longrightarrow, I'', s'} | ||
{I' \,\mathbf{then}\, \mathbf{loop}\, I, s \,\Longrightarrow | {I' \,\mathbf{then}\, \mathbf{loop}\, I, s \,\Longrightarrow, I'' \,\mathbf{then}\, \mathbf{loop}\, I, s'} | ||
</math> | </math> | ||
| Linia 466: | Linia 466: | ||
<math> | <math> | ||
\mathbf{exit}, s \,\Longrightarrow | \mathbf{exit}, s \,\Longrightarrow, \mbox{było-}\mathbf{exit} | ||
\quad \quad | \quad \quad | ||
\mathbf{continue}, s \,\Longrightarrow | \mathbf{continue}, s \,\Longrightarrow, \mbox{było-}\mathbf{continue} | ||
</math> | </math> | ||
<math> | <math> | ||
\frac{I_1, s \,\Longrightarrow | \frac{I_1, s \,\Longrightarrow, \mbox{było-}\mathbf{exit}} | ||
{I_1;\, I_2, s \,\Longrightarrow | {I_1;\, I_2, s \,\Longrightarrow, \mbox{było-}\mathbf{exit}} | ||
\quad \quad | \quad \quad | ||
\frac{I_1, s \,\Longrightarrow | \frac{I_1, s \,\Longrightarrow, \mbox{było-}\mathbf{continue}} | ||
{I_1;\, I_2, s \,\Longrightarrow | {I_1;\, I_2, s \,\Longrightarrow, \mbox{było-}\mathbf{continue}} | ||
</math> | </math> | ||
<math> | <math> | ||
\mathbf{loop}\, I, s \,\Longrightarrow | \mathbf{loop}\, I, s \,\Longrightarrow, I \,\mathbf{then}\, \mathbf{loop}\, I, s. | ||
</math> | </math> | ||
<math> | <math> | ||
\frac{I', s \,\Longrightarrow | \frac{I', s \,\Longrightarrow, \mbox{było-}\mathbf{exit}} | ||
{I' \,\mathbf{then}\, \mathbf{loop}\, I, s \,\Longrightarrow | {I' \,\mathbf{then}\, \mathbf{loop}\, I, s \,\Longrightarrow, s} | ||
\quad \quad | \quad \quad | ||
\frac{I', s \,\Longrightarrow | \frac{I', s \,\Longrightarrow, \mbox{było-}\mathbf{continue}} | ||
{I' \,\mathbf{then}\, \mathbf{loop}\, I, s \,\Longrightarrow | {I' \,\mathbf{then}\, \mathbf{loop}\, I, s \,\Longrightarrow, \mathbf{loop}\, I, s} | ||
\quad \quad | \quad \quad | ||
\frac{I', s \,\Longrightarrow | \frac{I', s \,\Longrightarrow, s'} | ||
{I' \,\mathbf{then}\, \mathbf{loop}\, I, s \,\Longrightarrow | {I' \,\mathbf{then}\, \mathbf{loop}\, I, s \,\Longrightarrow, \mathbf{loop}\, I, s} | ||
</math> | </math> | ||
<math> | <math> | ||
\frac{I', s \,\Longrightarrow | \frac{I', s \,\Longrightarrow, I'', s'} | ||
{I' \,\mathbf{then}\, \mathbf{loop}\, I, s \,\Longrightarrow | {I' \,\mathbf{then}\, \mathbf{loop}\, I, s \,\Longrightarrow, I'' \,\mathbf{then}\, \mathbf{loop}\, I, s'} | ||
</math> | </math> | ||
Wersja z 14:16, 9 cze 2020
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ą wyrażeń boolowskich i arytmetycznych oraz semantykę błędów wykonania. Wreszcie dodamy nową instrukcję pętli , pozwalającą na niestrukturalne przerwanie lub wznowienie iteracji (instrukcje i ).
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
Ćwiczenie 2
Rozważ dodatkowo operację dzielenia:
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
Ćwiczenie 3
Rozszerzmy język TINY o następującą instrukcję pętli:
to instrukcja pętli, stanowi instrukcję wewnętrzną. Instrukcja wychodzi z nabliższej otaczającej pętli i kontynuuje wykonanie programu od pierwszej instrukcji za tą pętlą. Instrukcja powraca na początek instrukcji wewnętrznej najbliższej otaczającej pętli .
Pozważ zarówno semantykę naturalną, jak i semantykę małych kroków.
Rozwiązanie
Rozwiązanie
Zadania domowe
Ćwiczenie 1
Zaproponuj semantykę małokrokową dla rozszerzeń języka Tiny, które studiowaliśmy powyżej.
Ćwiczenie 2
Napisz semantykę naturalną dla nieznacznie rozszerzonej wersji instrukcji :
Identyfikator pełni tutaj rolę etykiety związanej z instrukcją , jest też parametrem dwóch pozostałych instrukcji. kończy teraz najbliższą otaczającą pętlę o etykiecie . Podobnie wznawia najbliższą otaczającą pętlę o etykiecie .
Przykład
Program
x:
a := 1;
y:
x;
a := a-10;
a := a+1;
a := a+2;
kończy działanie z wartością zmiennej .
Za pomocą wcięć określiliśmy, do wnętrza której pętli 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ę , np. .
Ćwiczenie 3
Napisz semantykę naturalną i małokrokową dla rozszerzenia języka TINY o wyrażenia z efektami ubocznymi:
Obliczenie wyrażenia polega na wykonaniu a potem na obliczeniu . Wartość wyrażenia jest taka, jak wartość wyrażenia a efektem ubocznym jest podstawienie tej wartości na zmienną .
