Semantyka i weryfikacja programów/Ćwiczenia 3: Różnice pomiędzy wersjami
m Zastępowanie tekstu – „\</math>” na „\ </math>” |
m Zastępowanie tekstu – „,↵</math>” na „</math>,” |
||
| (Nie pokazano 1 pośredniej wersji utworzonej przez tego samego użytkownika) | |||
| Linia 57: | Linia 57: | ||
e, s \longrightarrow n | e, s \longrightarrow n | ||
\quad \quad \quad | \quad \quad \quad | ||
b, s \longrightarrow l | b, s \longrightarrow l</math>, | ||
</math> | |||
gdzie <math>s \in \mathbf{State}</math>, <math>n \in</math> jest liczbą całkowitą, <math>n \in \mathbf{Num}</math>, a <math>l \in \mathbf{Bool} = \{ \mathbf{true}, \mathbf{false} \}</math>. | gdzie <math>s \in \mathbf{State}</math>, <math>n \in</math> jest liczbą całkowitą, <math>n \in \mathbf{Num}</math>, a <math>l \in \mathbf{Bool} = \{ \mathbf{true}, \mathbf{false} \}</math>. | ||
| Linia 89: | Linia 88: | ||
n, s \,\longrightarrow\, n | n, s \,\longrightarrow\, n | ||
\quad \quad | \quad \quad | ||
l, s \,\longrightarrow\, l | l, s \,\longrightarrow\, l</math> | ||
</math> | |||
Operatory arytmetyczne definiujemy następująco: | Operatory arytmetyczne definiujemy następująco: | ||
| Linia 198: | Linia 196: | ||
{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, \mathtt{Blad} | e_1 / 0, s \,\Longrightarrow, \mathtt{Blad}</math> | ||
</math> | |||
Pomijamy tutaj reguły dla przypadku, gdy <math>e_2</math> oblicza się do wartości różnej od zera. | Pomijamy tutaj reguły dla przypadku, gdy <math>e_2</math> oblicza się do wartości różnej od zera. | ||
| Linia 305: | Linia 302: | ||
\mathbf{exit}, s \,\longrightarrow\, s, \mbox{było-}\mathbf{exit} | \mathbf{exit}, s \,\longrightarrow\, s, \mbox{było-}\mathbf{exit} | ||
\quad \quad | \quad \quad | ||
\mathbf{continue}, s \,\longrightarrow\, s, \mbox{było-}\mathbf{continue} | \mathbf{continue}, s \,\longrightarrow\, s, \mbox{było-}\mathbf{continue}</math> | ||
</math> | |||
Czyli instrukcje <math>\mathbf{exit}</math> i <math>\mathbf{continue}</math> nie modyfikują stanu <math>s</math>, ale zostawiają po sobie "ślad". | Czyli instrukcje <math>\mathbf{exit}</math> i <math>\mathbf{continue}</math> nie modyfikują stanu <math>s</math>, ale zostawiają po sobie "ślad". | ||
| Linia 313: | Linia 309: | ||
<math> | <math> | ||
\mathbf{State} \times \{ \mbox{było-}\mathbf{exit}, \mbox{było-}\mathbf{continue} \} | \mathbf{State} \times \{ \mbox{było-}\mathbf{exit}, \mbox{było-}\mathbf{continue} \}</math> | ||
</math> | |||
'''Pytanie''': jakie powinno być zachowanie <math>\mathbf{exit}</math> i <math>\mathbf{continue}</math> w konfiguracji <math>s, \mbox{było-}\mathbf{exit}</math> lub <math>s, \mbox{było-}\mathbf{continue}</math>? | '''Pytanie''': jakie powinno być zachowanie <math>\mathbf{exit}</math> i <math>\mathbf{continue}</math> w konfiguracji <math>s, \mbox{było-}\mathbf{exit}</math> lub <math>s, \mbox{było-}\mathbf{continue}</math>? | ||
| Linia 404: | Linia 399: | ||
\mathbf{exit}, s \,\Longrightarrow, s, \mbox{było-}\mathbf{exit} | \mathbf{exit}, s \,\Longrightarrow, s, \mbox{było-}\mathbf{exit} | ||
\quad \quad | \quad \quad | ||
\mathbf{continue}, s \,\Longrightarrow, s, \mbox{było-}\mathbf{continue} | \mathbf{continue}, s \,\Longrightarrow, s, \mbox{było-}\mathbf{continue}</math> | ||
</math> | |||
Ponadto musimy określić sposób, w jaki mały krok mniejszej instrukcji zostaje zamieniony na mały krok większej. Np. | Ponadto musimy określić sposób, w jaki mały krok mniejszej instrukcji zostaje zamieniony na mały krok większej. Np. | ||
| Linia 413: | Linia 407: | ||
{I_1;\, I_2, s \,\Longrightarrow, s', \mbox{było-}\mathbf{exit}} | {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}</math> | ||
</math> | |||
Nie musimy zajmowac się przypadkiem, gdy ślad powstaje w <math>I_2</math>, bo wybraliśmy podejście małokrokowe. | Nie musimy zajmowac się przypadkiem, gdy ślad powstaje w <math>I_2</math>, bo wybraliśmy podejście małokrokowe. | ||
| Linia 439: | Linia 432: | ||
<math> | <math> | ||
\mathbf{loop}\, I, s \,\Longrightarrow, I \,\mathbf{then}\, \mathbf{loop}\, I, s | \mathbf{loop}\, I, s \,\Longrightarrow, I \,\mathbf{then}\, \mathbf{loop}\, I, s</math> | ||
</math> | |||
Teraz możemy zapisać dwie powyższe reguły dla <math>\mathbf{loop}\ </math>, w poprawnej wersji, pamiętając o tym, że <math>\mbox{było-}\mathbf{exit}</math> i <math>\mbox{było-}\mathbf{continue}</math> pojawią się nie w instrukcji wewnętrznej, ale w jej ''kopii'' umieszczonej przed <math>\,\mathbf{then}\ </math>,: | Teraz możemy zapisać dwie powyższe reguły dla <math>\mathbf{loop}\ </math>, w poprawnej wersji, pamiętając o tym, że <math>\mbox{było-}\mathbf{exit}</math> i <math>\mbox{było-}\mathbf{continue}</math> pojawią się nie w instrukcji wewnętrznej, ale w jej ''kopii'' umieszczonej przed <math>\,\mathbf{then}\ </math>,: | ||
| Linia 480: | Linia 472: | ||
<math> | <math> | ||
\mathbf{loop}\, I, s \,\Longrightarrow, I \,\mathbf{then}\, \mathbf{loop}\, I, s | \mathbf{loop}\, I, s \,\Longrightarrow, I \,\mathbf{then}\, \mathbf{loop}\, I, s</math> | ||
</math> | |||
<math> | <math> | ||
Aktualna wersja na dzień 21:43, 11 wrz 2023
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ą .
