Semantyka i weryfikacja programów/Ćwiczenia 3: Różnice pomiędzy wersjami
m Zastępowanie tekstu - "\Longrightarrow\" na "\Longrightarrow" |
m Zastępowanie tekstu – „,</math>” na „</math>,” |
||
| 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 266: | Linia 266: | ||
</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 285: | ||
<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 320: | Linia 320: | ||
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 330: | ||
</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 351: | ||
</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 382: | ||
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 417: | Linia 417: | ||
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> | ||
| Linia 434: | Linia 434: | ||
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> | ||
| Linia 442: | Linia 442: | ||
</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> | ||
| Linia 455: | Linia 455: | ||
</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> | ||
| Linia 515: | Linia 515: | ||
{{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 524: | ||
</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 532: | ||
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 542: | ||
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>,. | ||
Wersja z 09:29, 5 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 Parser nie mógł rozpoznać (błąd składni): {\displaystyle \mathbf{loop}\} ,, 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 Parser nie mógł rozpoznać (błąd składni): {\displaystyle \mathbf{loop}\} , 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 Parser nie mógł rozpoznać (błąd składni): {\displaystyle \mathbf{loop}\} ,.
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 Parser nie mógł rozpoznać (błąd składni): {\displaystyle \mathbf{loop}\} ,:
Identyfikator pełni tutaj rolę etykiety związanej z instrukcją Parser nie mógł rozpoznać (błąd składni): {\displaystyle \mathbf{loop}\} ,, jest też parametrem dwóch pozostałych instrukcji. kończy teraz najbliższą otaczającą pętlę Parser nie mógł rozpoznać (błąd składni): {\displaystyle \mathbf{loop}\} , o etykiecie . Podobnie wznawia najbliższą otaczającą pętlę o etykiecie .
Przykład
Program
x: Parser nie mógł rozpoznać (błąd składni): {\displaystyle \mathbf{loop}\}
,
a := 1;
y: Parser nie mógł rozpoznać (błąd składni): {\displaystyle \mathbf{loop}\}
,
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 Parser nie mógł rozpoznać (błąd składni): {\displaystyle \mathbf{loop}\}
, 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ę Parser nie mógł rozpoznać (błąd składni): {\displaystyle \mathbf{loop}\}
,, np. Parser nie mógł rozpoznać (błąd składni): {\displaystyle \mathbf{loop}\, I \,\mathbf{end}\mathbf{loop}\}
,.
Ć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ą .
