Semantyka i weryfikacja programów/Ćwiczenia 3: Różnice pomiędzy wersjami
Z Studia Informatyczne
Przejdź do nawigacjiPrzejdź do wyszukiwania
m Zastępowanie tekstu – „,↵</math>” na „</math>,” |
|||
| (Nie pokazano 4 pośrednich wersji utworzonych przez tego samego użytkownika) | |||
| Linia 4: | Linia 4: | ||
Kończymy semantykę małych kroków i rozpoczynamy semantykę naturalną (duże kroki). | 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. | 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 <math>\mathbf{loop}\ | Wreszcie dodamy nową instrukcję pętli <math>\mathbf{loop}\ </math>,, pozwalającą na niestrukturalne przerwanie lub wznowienie iteracji (instrukcje <math>\mathbf{exit}</math> i <math>\mathbf{continue}</math>). | ||
| 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 | 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 210: | Linia 207: | ||
{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 266: | Linia 263: | ||
</math> | </math> | ||
Zwróćmy szczególnie uwagę na ostatnią regułę dla pętli <math>\mathbf{while}\ | Zwróćmy szczególnie uwagę na ostatnią regułę dla pętli <math>\mathbf{while}\ </math>,: wyraża ona przypadek, gdy błąd został wygenerowany nie w pierwszym obiegu pętli, ale w którymś z kolejnych. | ||
Musieliśmy rozważyc również ten przypadek, ponieważ wybraliśmy podejście dużych kroków; w podejściu małych kroków nie byłoby to zapewne konieczne. | Musieliśmy rozważyc również ten przypadek, ponieważ wybraliśmy podejście dużych kroków; w podejściu małych kroków nie byłoby to zapewne konieczne. | ||
| Linia 285: | Linia 282: | ||
<math>\mathbf{loop}\, I</math> to instrukcja pętli, <math>I</math> stanowi instrukcję wewnętrzną. | <math>\mathbf{loop}\, I</math> to instrukcja pętli, <math>I</math> stanowi instrukcję wewnętrzną. | ||
Instrukcja <math>\mathbf{exit}</math> wychodzi z nabliższej otaczającej pętli <math>\mathbf{loop}\ | Instrukcja <math>\mathbf{exit}</math> wychodzi z nabliższej otaczającej pętli <math>\mathbf{loop}\ </math>, i kontynuuje wykonanie programu od pierwszej instrukcji za tą pętlą. | ||
Instrukcja <math>\mathbf{continue}</math> powraca na początek instrukcji wewnętrznej najbliższej otaczającej pętli <math>\mathbf{loop}\ | Instrukcja <math>\mathbf{continue}</math> powraca na początek instrukcji wewnętrznej najbliższej otaczającej pętli <math>\mathbf{loop}\ </math>,. | ||
Pozważ zarówno semantykę naturalną, jak i semantykę małych kroków. | Pozważ zarówno semantykę naturalną, jak i semantykę małych kroków. | ||
| 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 320: | Linia 315: | ||
Zapiszmy teraz, jak inne instrukcje korzystają z dodatkowej informacji (śladu) zawartej w konfiguracjach. | Zapiszmy teraz, jak inne instrukcje korzystają z dodatkowej informacji (śladu) zawartej w konfiguracjach. | ||
Oczywiście "beneficjentem" korzystającym z tej informacji jest instrukcja <math>\mathbf{loop}\ | Oczywiście "beneficjentem" korzystającym z tej informacji jest instrukcja <math>\mathbf{loop}\ </math>,: | ||
<math> | <math> | ||
| Linia 330: | Linia 325: | ||
</math> | </math> | ||
Czyli w zależności od tego, jaki ślad został zarejestrowany podczas wykonania <math>I</math>, albo kończymy wykonanie pętli <math>\mathbf{loop}\ | Czyli w zależności od tego, jaki ślad został zarejestrowany podczas wykonania <math>I</math>, albo kończymy wykonanie pętli <math>\mathbf{loop}\ </math>,, albo rozpoczynamy kolejną iterację. | ||
Zauważmy, że stan <math>s'</math> może być różny od <math>s</math>, ponieważ zanim wykonała się ktoraś z instrukcji <math>\mathbf{exit}</math> lub | Zauważmy, że stan <math>s'</math> może być różny od <math>s</math>, ponieważ zanim wykonała się ktoraś z instrukcji <math>\mathbf{exit}</math> lub | ||
<math>\mathbf{continue}</math> mogły zostać zmienione wartości niektórych zmiennych. | <math>\mathbf{continue}</math> mogły zostać zmienione wartości niektórych zmiennych. | ||
| Linia 351: | Linia 346: | ||
</math> | </math> | ||
Okazuje się że nie, ponieważ ślad powinien zostać zawsze "wymazany" przez pętlę <math>\mathbf{loop}\ | Okazuje się że nie, ponieważ ślad powinien zostać zawsze "wymazany" przez pętlę <math>\mathbf{loop}\ </math>,. | ||
Teraz musimy określić zachowanie wszystkich instrukcji w sytuacji, gdy bieżąca konfiguracja zawiera już ślad. Zasadniczo, powinniśmy zaniechać wykonania instrukcji (w przypadku pętli, powinniśmy zaniechać dalszego iterowania tej pętli). | Teraz musimy określić zachowanie wszystkich instrukcji w sytuacji, gdy bieżąca konfiguracja zawiera już ślad. Zasadniczo, powinniśmy zaniechać wykonania instrukcji (w przypadku pętli, powinniśmy zaniechać dalszego iterowania tej pętli). | ||
| Linia 382: | Linia 377: | ||
Pominęliśmy zupełnie analogiczne reguły dla <math>\mbox{było-}\mathbf{continue}</math>. | Pominęliśmy zupełnie analogiczne reguły dla <math>\mbox{było-}\mathbf{continue}</math>. | ||
Zauważmy, że dla pętli <math>\mathbf{while}\ | Zauważmy, że dla pętli <math>\mathbf{while}\ </math>, nie rozpatrujemy przypadku, gdy dozór <math>b</math> oblicza się do <math>\mathbf{false}</math>, gdyż w tym przypadku nie ma możliwości wygenerowania śladu. | ||
Zauważmy też, że nasze reguły nie pozwalają na dodanie drugiego (kolejnego) śladu! | Zauważmy też, że nasze reguły nie pozwalają na dodanie drugiego (kolejnego) śladu! | ||
| Linia 402: | Linia 397: | ||
<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> | |||
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. | ||
<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}</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. | ||
Ponadto, nie musimy opisywać instrukcji warunkowej i pętli <math>\mathbf{while}\ | Ponadto, nie musimy opisywać instrukcji warunkowej i pętli <math>\mathbf{while}\ </math>,, ponieważ ślad nie może powstać podczas obliczania dozoru! | ||
Wreszcie zobaczmy jak zachowuje się pętla <math>\mathbf{loop}\ | Wreszcie zobaczmy jak zachowuje się pętla <math>\mathbf{loop}\ </math>,: | ||
<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 434: | Linia 427: | ||
Niestety powyższe reguły '''nie są poprawne'''! | Niestety powyższe reguły '''nie są poprawne'''! | ||
Dlaczego? Jak zwykle w semantyce małych kroków, wykonując instrukcję wewnętrzną "zapominamy" stopniowo, jaka była ona na początku. | Dlaczego? Jak zwykle w semantyce małych kroków, wykonując instrukcję wewnętrzną "zapominamy" stopniowo, jaka była ona na początku. | ||
W związku z tym nie potrafimy poprawnie powrócić do wykonywania pętli <math>\mathbf{loop}\ | W związku z tym nie potrafimy poprawnie powrócić do wykonywania pętli <math>\mathbf{loop}\ </math>, po wywołaniu <math>\mathbf{continue}</math>. | ||
Prostym sposobem poprawienia naszego błędu jest rozszerzenie składni tak, aby możliwe było jednorazowe rozwinięcie pętli <math>\mathbf{loop}\ | Prostym sposobem poprawienia naszego błędu jest rozszerzenie składni tak, aby możliwe było jednorazowe rozwinięcie pętli <math>\mathbf{loop}\ </math>,: | ||
<math> | <math> | ||
\mathbf{loop}\, I, s \,\Longrightarrow | \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}\ | 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>,: | ||
<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> | ||
Potrzebujemy też dodatkowej reguły dla obliczeń wewnątrz instrukcji stojącej przed <math>\,\mathbf{then}\ | Potrzebujemy też dodatkowej reguły dla obliczeń wewnątrz instrukcji stojącej przed <math>\,\mathbf{then}\ </math>, (w szczególności może ona zawierać zagnieżdzone pętle <math>\mathbf{loop}\ </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> | ||
| Linia 466: | Linia 458: | ||
<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> | ||
| Linia 515: | Linia 506: | ||
{{cwiczenie|2|cw2.dom| | {{cwiczenie|2|cw2.dom| | ||
Napisz semantykę naturalną dla nieznacznie rozszerzonej wersji instrukcji <math>\mathbf{loop}\ | Napisz semantykę naturalną dla nieznacznie rozszerzonej wersji instrukcji <math>\mathbf{loop}\ </math>,: | ||
<math> | <math> | ||
| Linia 524: | Linia 515: | ||
</math> | </math> | ||
Identyfikator <math>x</math> pełni tutaj rolę etykiety związanej z instrukcją <math>\mathbf{loop}\ | Identyfikator <math>x</math> pełni tutaj rolę etykiety związanej z instrukcją <math>\mathbf{loop}\ </math>,, jest też parametrem dwóch pozostałych instrukcji. | ||
<math>\mathbf{exit} x</math> kończy teraz najbliższą otaczającą pętlę <math>\mathbf{loop}\ | <math>\mathbf{exit} x</math> kończy teraz najbliższą otaczającą pętlę <math>\mathbf{loop}\ </math>, o etykiecie <math>x</math>. Podobnie <math>\mathbf{continue} x</math> wznawia najbliższą otaczającą pętlę o etykiecie <math>x</math>. | ||
}} | }} | ||
| Linia 532: | Linia 523: | ||
Program | Program | ||
x: <math>\mathbf{loop}\ | x: <math>\mathbf{loop}\ </math>, | ||
a := 1; | a := 1; | ||
y: <math>\mathbf{loop}\ | y: <math>\mathbf{loop}\ </math>, | ||
<math>\mathbf{exit}</math> x; | <math>\mathbf{exit}</math> x; | ||
a := a-10; | a := a-10; | ||
| Linia 542: | Linia 533: | ||
kończy działanie z wartością zmiennej <math>a = 3</math>. | kończy działanie z wartością zmiennej <math>a = 3</math>. | ||
Za pomocą wcięć określiliśmy, do wnętrza której pętli <math>\mathbf{loop}\ | Za pomocą wcięć określiliśmy, do wnętrza której pętli <math>\mathbf{loop}\ </math>, 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ę <math>\mathbf{loop}\ | 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ę <math>\mathbf{loop}\ </math>,, np. <math>\mathbf{loop}\, I \,\mathbf{end}\mathbf{loop}\ </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ą .
