Semantyka i weryfikacja programów/Ćwiczenia 3: Różnice pomiędzy wersjami

Wersja z 08:25, 11 sie 2006

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

{{{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

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

$I : : = 𝐥 𝐨 𝐨 𝐩 I | 𝐞 𝐱 𝐢 𝐭 | 𝐜 𝐨 𝐧 𝐭 𝐢 𝐧 𝐮 𝐞$

$𝐥 𝐨 𝐨 𝐩 I$ to instrukcja pętli, $I$ 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 (semantyka naturalna)

{{{3}}}

Rozwiązanie (małe kroki)

{{{3}}}

Zadania domowe

Ćwiczenie 1

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

Ćwiczenie 2

Napisz semantyję naturalną dla nieznacznie rozszerzonej wersji instrukcji $𝐥 𝐨 𝐨 𝐩$ :

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

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

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 $a = 3$ . 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. $𝐥 𝐨 𝐨 𝐩 I 𝐞 𝐧 𝐝 𝐥 𝐨 𝐨 𝐩$ .

Ćwiczenie 3

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

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

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

Semantyka i weryfikacja programów/Ćwiczenia 3: Różnice pomiędzy wersjami

Wersja z 08:25, 11 sie 2006

Zawartość

Rozszerzenia semantyki języka Tiny

Zadania domowe

Menu nawigacyjne

Działania na stronie

Opcje strony

Narzędzia osobiste

Nawigacja

Szukaj

Narzędzia

@@ Linia 4: / Linia 4: @@
 Kończymy semantykę małych kroków i rozpoczynamy semantykę naturalną (duże kroki).
-Uzupełnimy semantykę naturalną języka Tiny o semantykę naturalną
+Uzupełnimy semantykę naturalną języka Tiny o semantykę naturalną wyrażeń boolowskich i arytmetycznych oraz semantykę błędów wykonania.
-wyrażeń boolowskich i arytmetycznych oraz semantykę błędów wykonania.
+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>).
-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 15: / Linia 13: @@
 {{cwiczenie|1|cw1|
-Zdefiniuj znaczenie wyrażeń boolowskich i arytmetycznych
+Zdefiniuj znaczenie wyrażeń boolowskich i arytmetycznych w języku Tiny, w stylu dużych kroków (semantyka naturalna).
-w języku Tiny, w stylu dużych kroków (semantyka naturalna).
 }}
@@ Linia 24: / Linia 21: @@
 <div class="mw-collapsible mw-made=collapsible mw-collapsed"><div class="mw-collapsible-content" style="display:none">
-Przypomnijmy składnię wyrażeń boolowskich i arytmetycznych
+Przypomnijmy składnię wyrażeń boolowskich i arytmetycznych jezyka Tiny:
-jezyka Tiny:
 <math>
@@ Linia 64: / Linia 60: @@
 </math>
-gdzie <math>s \in \mathbf{State}</math>, <math>n \in</math> jest liczbą całkowitą,
+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>.
-<math>n \in \mathbf{Num}</math>, a <math>l \in \mathbf{Bool} = \{ \mathbf{true}, \mathbf{false} \}</math>.
+Tranzycja taka oznacza, że wyrażenie <math>e</math> w stanie <math>s</math> wylicza się do wartości <math>n</math> oraz analogicznie, wyrażenie logiczne <math>b</math> w stanie <math>s</math> wylicza się do <math>l</math>.
-Tranzycja taka oznacza, że wyrażenie <math>e</math> w stanie <math>s</math> wylicza się do
-wartości <math>n</math> oraz analogicznie, wyrażenie logiczne <math>b</math> w
-stanie <math>s</math> wylicza się do <math>l</math>.
 Zatem zbiór konfiguracji dla semantyki całego języka Tiny to znów
@@ Linia 76: / Linia 69: @@
 </math>
 a konfiguracje końcowe to <math>\mathbf{State}</math> tak jak poprzednio.
-Tranzycje dla instrukcji pozostają zasadniczo bez zmian, z tym,
+Tranzycje dla instrukcji pozostają zasadniczo bez zmian, z tym, że odwołania do funkcji semantycznych dla wyrażen zastępujemy przez odpowiednie tranzycje.
-że odwołania do funkcji semantycznych dla wyrażen zastępujemy
-przez odpowiednie tranzycje.
 Np. dla instrukcji pętli będziemy mieć następujące reguły:
@@ Linia 110: / Linia 101: @@
 </math>
-Czyli aby obliczyć sumę <math>e_1 + e_2</math> w stanie
+Czyli aby obliczyć sumę <math>e_1 + e_2</math> w stanie <math>s</math>, trzeba najpierw obliczyć <math>e_1</math> i <math>e_2</math> w tym stanie, a następnie dodać obliczone wartości.
-<math>s</math>, trzeba najpierw obliczyć <math>e_1</math> i
+Zauważmy, że nie specyfikujemy kolejności, w jakiej mają się obliczać obydwa podwyrażenia.
-<math>e_2</math> w tym stanie, a następnie dodać obliczone wartości.
+I choć tutaj nie ma to żadnego znaczenia, w przyszłości będzie inaczej, gdy jezyk będzie umożliwiał efekty uboczne podczas obliczania wyrażeń.
-Zauważmy, że nie specyfikujemy kolejności, w jakiej mają się
-obliczać obydwa podwyrażenia.
-I choć tutaj nie ma to żadnego znaczenia, w przyszłości
-będzie inaczej, gdy jezyk będzie umożliwiał efekty uboczne
-podczas obliczania wyrażeń.
-Podobne reguły można napisać dla pozostałych operacji
+Podobne reguły można napisać dla pozostałych operacji arytmetycznych, oraz dla spójników logicznych:
-arytmnetycznych, oraz dla spójników logicznych:
 <math>
@@ Linia 129: / Linia 114: @@
 </math>
-Oto inny wariant, reguły lewo-stronne (ponieważ rozpoczynamy od ''lewego'' koniunktu):
+(strategia gorliwa).
+Reguły dla <math>\leq</math> są następujące:
+<math>
+\frac{e_1, s \,\longrightarrow\, n_1 \quad \quad e_2, s \,\longrightarrow\, n_2 \quad \quad n_1 \leq n_2}
+     {e_1 \leq e_2, s \,\longrightarrow\, \mathbf{true}}
+\quad \quad
+\frac{e_1, s \,\longrightarrow\, n_1 \quad \quad e_2, s \,\longrightarrow\, n_2 \quad \quad n_1 > n_2}
+     {e_1 \leq e_2, s \,\longrightarrow\, \mathbf{false}}
+</math>
+Oto inny wariant semantyki spójnika <math>\land</math>, tzw. strategia lewostronna (ponieważ rozpoczynamy od ''lewego'' koniunktu):
 <math>
@@ Linia 140: / Linia 136: @@
 </math>
-Inny wariant to wariant prawo-stronny (
+Inny wariant to strategia prawostronna (najpierw <math>b_2</math>, potem <math>b_1</math>).
-najpierw <math>b_2</math>, potem <math>b_1</math>).
+Wreszcie rozważmy kombinację obydwu semantyk (strategia ''równoległa'' lub ''leniwa''):
-Wreszcie rozważmy kombinację obydwu semantyk (reguły ''równoległe''):
 <math>
@@ Linia 152: / Linia 147: @@
 </math>
-Czyli jeśli którekolwiek z podwyrażeń daje wynik <math>\mathbf{false}</math>,
+Czyli jeśli którekolwiek z podwyrażeń daje wynik <math>\mathbf{false}</math>, to taki wynik zyskuje całe wyrażenie.
-to taki wynik zyskuje całe wyrażenie.
 Dodatkowo potrzebujemy jeszcze reguły:
@@ Linia 162: / Linia 156: @@
 </math>
-W naszym prostym języku wszystkie cztery warianty
+'''Pytanie:''' czy w naszym prostym języku wszystkie cztery strategie obliczania spójnika <math>\land</math> są równoważne?
-są równoważne.
-Reguły dla pozostałych spójników logicznych, dla
+Reguły dla negacji oraz dla instrukcji przypisania pozostawiamy jako proste ćwiczenie.
-negacji oraz dla instrukcji przypisania pozostawiamy jako proste
-ćwiczenie.
 </div></div>
@@ Linia 182: / Linia 174: @@
 i rozszerz semantykę z poprzedniego zadania.
-Dzielenie przez zero jest błądem i  kończy natychmiast wykonanie
+Dzielenie przez zero jest błądem i  kończy natychmiast wykonanie programu.
-programu.
+Oprócz stanu wynikiem programu powinna byc informacja o błędzie, jeśli błąd wystąpił.
-Oprócz stanu wynikiem programu powinna byc informacja o błędzie,
-jeśli błąd wystąpił.
 }}
@@ Linia 194: / Linia 184: @@
 Dopóki nie wystąpi błąd dzielenia przez zero, semantyka programu
-powinna być identyczna jak w poprzednim zadaniu. Zatem pozostawiamy
+powinna być identyczna jak w poprzednim zadaniu. Zatem pozostawiamy wszystkie reguły z poprzedniego zadania.
-wszystkie reguły z poprzedniego zadania.
 Dodatkowo potrzebujemy reguł, które opiszą
@@ Linia 202: / Linia 191: @@
 Zaczynamy od pierwszego punktu.
-W tym celu dodajemy do konfiguracji jedną konfigurację końcową
+W tym celu dodajemy do konfiguracji jedną konfigurację końcową <math>\mathtt{Blad}</math>.
-<math>\mathtt{Blad}</math>.
+Reguła opisująca powstanie błędu może wyglądać np. tak (duże i małe kroki):
-Reguła opisująca powstanie błędu może wyglądać np. tak
-(duże i małe kroki):
 <math>
@@ Linia 214: / Linia 201: @@
 </math>
-Pomijamy tutaj reguły dla przypadku, gdy <math>e_2</math>
+Pomijamy tutaj reguły dla przypadku, gdy <math>e_2</math> oblicza się do wartości różnej od zera.
-oblicza się do wartości różnej od zera.
+Ponadto dla czytelności przyjęliśmy, że wynikiem tranzycji jest wyłącznie informacja o błędzie, a stan jest zapominany.
-Ponadto dla czytelności przyjęliśmy, że wynikiem tranzycji jest
+Bez trudu możnaby wszystkie reguły (zarówno te powyżej jak i te poniżej) zmodyfikować tak, by wraz z informacją o błędzie zwracany był też stan, w którym błąd się pojawił.
-wyłącznie informacja o błędzie, a stan jest zapominany.
+Np. ostatnia reguła wyglądałaby następująco:
-Bez trudu możnaby wszystkie reguły (zarówno te powyżej jak i te
-poniżej) zmodyfikować tak, by wraz z
-informacją o błędzie zwracany był też stan, w którym błąd się
-pojawił. Np. ostatnia reguła wyglądałaby następująco:
 <math>
@@ Linia 230: / Linia 213: @@
 </math>
-i zamiast pojedyńczej konfiguracji końcowej <math>\mathtt{Blad}</math> potrzebowalibyśmy
+i zamiast pojedyńczej konfiguracji końcowej <math>\mathtt{Blad}</math> potrzebowalibyśmy oczywiście całego zbioru <math>\{ \mathtt{Blad} \} \times \mathbf{State}</math>.
-oczywiście całego zbioru <math>\{ \mathtt{Blad} \} \times \mathbf{State}</math>.
-Przejdźmy teraz do drugiego punktu. Potrzebujemy dodatkowych reguł,
+Przejdźmy teraz do drugiego punktu. Potrzebujemy dodatkowych reguł, które zagwarantują, że błąd, raz pojawiwszy się, propaguje się przez wszystkie konstrukcje składniowe, a normalne obliczenie wyrażenia jest wstrzymame.
-które zagwarantują, że błąd, raz pojawiwszy się, propaguje się przez
-wszystkie konstrukcje składniowe, a normalne obliczenie wyrażenia
-jest wstrzymame.
 <math>
@@ Linia 287: / Linia 266: @@
 </math>
-Zwróćmy szczególnie uwagę na ostatnią regułę dla pętli <math>\mathbf{while}\,</math>:
+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.
-wyraża ona przypadek, gdy błąd został wygenerowany
+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.
-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.
 </div></div>
@@ Linia 310: / Linia 285: @@
 <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}\,</math>
+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ą.
-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}\,</math>.
-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.
@@ Linia 323: / Linia 296: @@
 <div class="mw-collapsible mw-made=collapsible mw-collapsed"><div class="mw-collapsible-content" style="display:none">
-Dodamy do reguł semantyki naturalnej dla języka Tiny
+Dodamy do reguł semantyki naturalnej dla języka Tiny kilka nowych reguł opisujących nową konstrukcję języka i jej ,,interakcję" z pozostałymi konstrukcjami.
-kilka nowych reguł opisujących nową konstrukcję języka
-i jej ,,interakcję\'' z pozostałymi konstrukcjami.
-Pomysł polega na dodaniu specjalnych konfiguracji zawierających
+Pomysł polega na dodaniu specjalnych konfiguracji zawierających informację o tym, że została wykonana instrukcja <math>\mathbf{exit}</math> lub <math>\mathbf{continue}</math>. Oto odpowiednie reguły:
-informację o tym, że została wykonana instrukcja <math>\mathbf{exit}</math>
-lub <math>\mathbf{continue}</math>. Oto odpowiednie reguły:
 <math>
@@ Linia 337: / Linia 306: @@
 </math>
-Czyli instrukcje <math>\mathbf{exit}</math> i <math>\mathbf{continue}</math> nie modyfikują
+Czyli instrukcje <math>\mathbf{exit}</math> i <math>\mathbf{continue}</math> nie modyfikują stanu <math>s</math>, ale zostawiają po sobie ,,ślad".
-stanu <math>s</math>, ale zostawiają po sobie ,,ślad".
+Zauważmy, że taki ślad zostaje pozostawiony tylko wtedy, jesli nie było dotychczas innego śladu, to znaczy jeśli <math>\mathbf{exit}</math> (lub <math>\mathbf{continue}</math>) zostało wykonane w zwykłym stanie <math>s</math>.
-Zauważmy, że taki ślad zostaje pozostawiony tylko wtedy, jesli
-nie było dotychczas innego śladu, to znaczy jeśli <math>\mathbf{exit}</math>
-(lub <math>\mathbf{continue}</math>) zostało wykonane w zwykłym stanie <math>s</math>.
 Oczywiście poszerzamy odpowiednio zbiór konfiguracji o:
 <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>
-'''Pytanie''': jakie powinno być zachowanie <math>\mathbf{exit}</math> i
+'''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>?
-<math>\mathbf{continue}</math> w konfiguracji <math>s, \mbox{było-}\mathbf{exit}</math>
+Czy instrukcje <math>\mathbf{exit}</math> i <math>\mathbf{continue}</math> będą faktycznie wykonywane w takich konfiguracjach?
-lub <math>s, \mbox{było-}\mathbf{continue}</math>?
-Czy instrukcje <math>\mathbf{exit}</math> i <math>\mathbf{continue}</math>
-będą faktycznie wykonywane w takich konfiguracjach?
-Zapiszmy teraz jak inne instrukcje korzystają z dodatkowej informacji
+Zapiszmy teraz jak inne instrukcje korzystają z dodatkowej informacji (śladu) zawartej w konfiguracjach.
-(śladu) zawartej w konfiguracjach.
+Oczywiście ,,beneficjentem" korzystającym z tej informacji jest instrukcja <math>\mathbf{loop}\,</math>:
-Oczywiście beneficjentem tej informacji jest instrukcji <math>\mathbf{loop}\,</math>:
 <math>
@@ Linia 366: / Linia 328: @@
 </math>
-Czyli w zależności od tego, jaki ślad został zarejestrowany
+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ę.
-podczas wykonania <math>I</math>, albo kończymy wykonanie  pętli <math>\mathbf{loop}\,</math>,
+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
-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
 <math>\mathbf{continue}</math>, mogły zostać zmienione wartości niektórych zmiennych.
-Oczywiście, jeśli instrukcja wewnętrzna <math>I</math> zakończyła się
+Oczywiście, jeśli instrukcja wewnętrzna <math>I</math> zakończyła się ''normalnie'', kontynuujemy wykonanie pętli podobnie jak w przypadku wywołania <math>\mathbf{continue}</math>:
-''normalnie'', kontynuujemy wykonanie pętli podobnie jak w przypadku
-wywołania <math>\mathbf{continue}</math>:
 <math>
@@ Linia 392: / Linia 349: @@
 </math>
-Okazuje się że nie, ponieważ ślad powinien zostać zawsze
+Okazuje się że nie, ponieważ ślad powinien zostać zawsze ,,wymazany" przez pętlę <math>\mathbf{loop}\,</math>.
-,,wymazany" przez pętlę <math>\mathbf{loop}\,</math>.
-<!--
-Poza tym reguły te wykraczałyby poza klasyczna podejście semantyki
-naturalnej, w którym zwykle bezpośrednio definiujemy
-tranzycje postaci <math>I, s \,\longrightarrow\, s'</math>.
--->
-Teraz musimy określić zachowanie wszystkich instrukcji w sytuacji,
+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).
-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).
 Oto odpowiednie reguły dla <math>\mbox{było-}\mathbf{exit}</math>:
@@ Linia 432: / Linia 380: @@
 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}\,</math> nie rozpatrujemy przypadku,
+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.
-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, ż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!
 </div></div>
@@ Linia 447: / Linia 392: @@
 <div class="mw-collapsible mw-made=collapsible mw-collapsed"><div class="mw-collapsible-content" style="display:none">
-W semantyce naturalnej musieliśmy napisać wiele reguł aby
+W semantyce naturalnej musieliśmy napisać wiele reguł aby zapewnić pomijanie instrukcji w sytuacji, gdy został juz zarejestrowany jakiś ślad. Było to dość uciążliwe.
-zapewnić pomijanie instrukcji w sytuacji, gdy został juz
+Okazuje się, że podejście mało-krokowe oferuje możliwość bardziej eleganckiego rozwiązania.
-zarejestrowany jakiś ślad. Było to dość uciążliwe.
-Okazuje się, że podejście mało-krokowe oferuje możliwość
-bardziej eleganckiego rozwiązania.
 Punktem startowym sę teraz reguły mało-krokowe dla języka Tiny.
-Podobnie jak poprzednio rozszerzymy zbiór konfiguracji i podobnie
+Podobnie jak poprzednio rozszerzymy zbiór konfiguracji i podobnie opiszemy, jak powstaje ślad:
-opiszemy, jak powstaje ślad:
 <math>
@@ Linia 464: / Linia 405: @@
 </math>
-Ponadto musimy określić sposób, w jaki mały krok
+Ponadto musimy określić sposób, w jaki mały krok mniejszej instrukcji zostaje zamieniony na mały krok większej. Np.
-mniejszej instrukcji zostaje zamieniony na mały krok
-większej. Np.
 <math>
@@ Linia 475: / Linia 414: @@
 </math>
-Nie musimy zajmowac się przypadkiem, gdy ślad
+Nie musimy zajmowac się przypadkiem, gdy ślad powstaje w <math>I_2</math>, bo wybraliśmy podejście mało-krokowe.
-powstaje w <math>I_2</math>, bo wybraliśmy podejście mało-krokowe.
+Ponadto, nie musimy opisywać instrukcji warunkowej i pętli <math>\mathbf{while}\,</math>, ponieważ ślad nie może powstać podczas obliczania dozoru!
-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}\,</math>:
@@ Linia 490: / Linia 427: @@
 </math>
-Reguły te są prawie identyczne do reguł semantyki naturalnej dla tej
+Reguły te są prawie identyczne do reguł semantyki naturalnej dla tej sytuacji!
-sytuacji!
+Natomiast korzystamy z tego, że w podejściu mało-krokowym zmiana konfiguracji na <math>s', \mbox{było-}\mathbf{exit}</math> czy <math>s', \mbox{było-}\mathbf{continue}</math> jest ''natychmiast'' widoczna w instrukcji <math>\mathbf{loop}\, I</math>, nawet jeśli <math>\mathbf{exit}</math> czy <math>\mathbf{continue}</math> zostało wywołane głęboko wewnątrz <math>I</math>!
-Natomiast korzystamy z tego, że w podejściu mało-krokowym zmiana konfiguracji
-na <math>s', \mbox{było-}\mathbf{exit}</math> czy <math>s', \mbox{było-}\mathbf{continue}</math> jest
-''natychmiast'' widoczna w instrukcji <math>\mathbf{loop}\, I</math>, nawet jeśli
-<math>\mathbf{exit}</math> czy <math>\mathbf{continue}</math> zostało wywołane głęboko wewnątrz
-<math>I</math>!
 Niestety powyższe reguły '''nie są poprawne'''!
-Dlaczego? Jak zwykle w semantyce małych kroków, wykonując instrukcję
+Dlaczego? Jak zwykle w semantyce małych kroków, wykonując instrukcję wewnętrzną ''zapominamy'' stopniowo jaka była ona na początku.
-wewnętrzną ''zapominamy'' stopniowo jaka była ona na początku.
+I 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>.
-I 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 blędu jest rozszerzenie składni
+Prostym sposobem poprawienia naszego blędu jest rozszerzenie składni tak, aby możliwe było jednorazowe rozwinięcie pętli <math>\mathbf{loop}\,</math>:
-tak, aby możliwe było jednorazowe rozwinięcie pętli <math>\mathbf{loop}\,</math>:
 <math>
@@ Linia 511: / Linia 440: @@
 </math>
-Teraz możemy zapisać dwie powyższe reguły dla <math>\mathbf{loop}\,</math> w poprawnej
+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>:
-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>
@@ Linia 521: / Linia 447: @@
 \quad \quad
 \frac{I', s \,\Longrightarrow\, s', \mbox{było-}\mathbf{continue}}
-      {I; \,\mathbf{then}\, \mathbf{loop}\, I, s \,\Longrightarrow\, \mathbf{loop}\, I, s'}
+      {I' \,\mathbf{then}\, \mathbf{loop}\, I, s \,\Longrightarrow\, \mathbf{loop}\, I, s'}
 \quad \quad
 \frac{I', s \,\Longrightarrow\, s'}
-      {I; \,\mathbf{then}\, \mathbf{loop}\, I, s \,\Longrightarrow\, \mathbf{loop}\, I, s'}
+      {I' \,\mathbf{then}\, \mathbf{loop}\, I, s \,\Longrightarrow\, \mathbf{loop}\, I, s'}
 </math>
-Potrzebujemy też dodatkowej reguły dla obliczeń wewnątrz instrukcji
+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>):
-stojącej przed <math>\,\mathbf{then}\,</math> (w szczególności może ona zawierać
-zagnieżdzone pętle <math>\mathbf{loop}\,</math> :
 <math>
@@ Linia 536: / Linia 460: @@
 </math>
-Na koniec zauważmy, że stan <math>s'</math> w
+Na koniec zauważmy, że stan <math>s'</math> w pierwszych dwóch z powyższych reguł nigdy nie jest różny od <math>s</math>. Zatem równoważnie moglibyśmy zamienić <math>s'</math> na <math>s</math> w powyższych dwóch regułach. Ale wtedy okazuje się , <math>s</math> w parze z <math>\mbox{było-}\mathbf{exit}</math> albo <math>\mbox{było-}\mathbf{continue}</math> jest nadmiarowe i może zostać wyeliminowane.
-pierwszych dwóch z powyższych reguł nigdy nie jest różny
-od <math>s</math>. Zatem równoważnie moglibyśmy zamienić <math>s'</math> na <math>s</math>
-w powyższych dwóch regułach. Ale wtedy okazuje się , <math>s</math>
-w parze z <math>\mbox{było-}\mathbf{exit}</math> albo <math>\mbox{było-}\mathbf{continue}</math> jest nadmiarowe
-i może zostać wyeliminowane.
 Zatem ostatecznie nasze reguły mogą wyglądać tak:
@@ Linia 568: / Linia 486: @@
 \quad \quad
 \frac{I', s \,\Longrightarrow\, \mbox{było-}\mathbf{continue}}
-      {I; \,\mathbf{then}\, \mathbf{loop}\, I, s \,\Longrightarrow\, \mathbf{loop}\, I, s}
+      {I' \,\mathbf{then}\, \mathbf{loop}\, I, s \,\Longrightarrow\, \mathbf{loop}\, I, s}
 \quad \quad
 \frac{I', s \,\Longrightarrow\, s'}
-      {I; \,\mathbf{then}\, \mathbf{loop}\, I, s \,\Longrightarrow\, \mathbf{loop}\, I, s}
+      {I' \,\mathbf{then}\, \mathbf{loop}\, I, s \,\Longrightarrow\, \mathbf{loop}\, I, s}
 </math>
@@ Linia 579: / Linia 497: @@
 </math>
-a zbiór konfiguracji poszerzamy tylko o dwie nowe konfiguracje
+a zbiór konfiguracji poszerzamy tylko o dwie nowe konfiguracje <math>\{ \mbox{było-}\mathbf{exit}, \mbox{było-}\mathbf{continue} \}</math>.
-<math>\{ \mbox{było-}\mathbf{exit}, \mbox{było-}\mathbf{continue} \}</math>.
 </div></div>
@@ Linia 607: / Linia 524: @@
 </math>
-Identyfikator <math>x</math> pełni tutaj rolę etykiety związanej z
+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.
-instrukcją <math>\mathbf{loop}\,</math>, jest też parametrem dwóch pozostałych
+<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>.
-instrukcji. <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 628: / Linia 542: @@
 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
+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.
-<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}\,</math>, np. <math>\mathbf{loop}\, I \,\mathbf{end}\mathbf{loop}\,</math>.
-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>.
@@ Linia 650: / Linia 560: @@
 </math>
-Obliczenie wyrażenia <math>\,\mathbf{do}\, I \,\mathbf{then}\, e</math> polega na wykonaniu <math>I</math>
+Obliczenie wyrażenia <math>\,\mathbf{do}\, I \,\mathbf{then}\, e</math> polega na wykonaniu <math>I</math> a potem na obliczeniu <math>e</math>.
-a potem na obliczeniu <math>e</math>. Wartość wyrażenia <math>x:= e</math> jest taka
+Wartość wyrażenia <math>x:= e</math> jest taka jak wartość wyrażenia <math>e</math> a efektem ubocznym jest podstawienie tej wartości na zmienną <math>x</math>.
-jak wartość wyrażenia <math>e</math> a efektem ubocznym jest
-podstawienie tej wartości na zmienną <math>x</math>.
 }}