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

Z Studia Informatyczne
Przejdź do nawigacjiPrzejdź do wyszukiwania
← poprzednia edycjanastępna edycja →
WizualnieWikikod
Sl (dyskusja | edycje)
101 edycji
Nie podano opisu zmian
Dorota (dyskusja | edycje)
376 edycji
Nie podano opisu zmian
Linia 1: Linia 1:


== Zawartość ==
== Zawartość ==


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}\,</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 13: Linia 12:
{{cwiczenie|1|cw1|
{{cwiczenie|1|cw1|


Zdefiniuj znaczenie wyrażeń boolowskich i arytmetycznych w języku Tiny, w stylu dużych kroków (semantyka naturalna).
Zdefiniuj znaczenie wyrażeń boolowskich i arytmetycznych w języku TINY w stylu dużych kroków (semantyka naturalna).
}}
}}


Linia 21: Linia 20:
<div class="mw-collapsible mw-made=collapsible mw-collapsed"><div class="mw-collapsible-content" style="display:none">
<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 jezyka Tiny:
Przypomnijmy składnię wyrażeń boolowskich i arytmetycznych języka TINY:


<math>
<math>
Linia 69: Linia 68:
</math>
</math>
a konfiguracje końcowe to <math>\mathbf{State}</math> tak jak poprzednio.
a konfiguracje końcowe to <math>\mathbf{State}</math> tak jak poprzednio.
Tranzycje dla instrukcji pozostają zasadniczo bez zmian, z tym, że odwołania do funkcji semantycznych dla wyrażen zastępujemy przez odpowiednie tranzycje.
Tranzycje dla instrukcji pozostają zasadniczo bez zmian, z tym ż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:
Np. dla instrukcji pętli będziemy mieć następujące reguły:


Linia 84: Linia 83:
Podobnie dla instrukcji warunkowej.
Podobnie dla instrukcji warunkowej.
Teraz zajmiemy się tranzycjami dla wyrażeń.
Teraz zajmiemy się tranzycjami dla wyrażeń.
Zacznijmy od stalych arytmetycznych i boolowskich:
Zacznijmy od stałych arytmetycznych i boolowskich:


<math>
<math>
Linia 174: Linia 173:


i rozszerz semantykę z poprzedniego zadania.
i rozszerz semantykę z poprzedniego zadania.
Dzielenie przez zero jest błądem i kończy natychmiast wykonanie programu.
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ł.
Oprócz stanu wynikiem programu powinna byc informacja o błędzie, jeśli błąd wystąpił.
}}
}}
Linia 275: Linia 274:
{{cwiczenie|3|cw3|
{{cwiczenie|3|cw3|


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


<math>
<math>
Linia 288: Linia 287:
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.
Pozważ zarówno semantykę naturalną, jak i semantykę małych kroków.
}}
}}


Linia 296: Linia 295:
<div class="mw-collapsible mw-made=collapsible mw-collapsed"><div class="mw-collapsible-content" style="display:none">
<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 kilka nowych reguł opisujących nową konstrukcję języka i jej ,,interakcję" z pozostałymi konstrukcjami.
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.


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:
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:
Linia 306: Linia 305:
</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".  
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, jeśli 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:
Oczywiście poszerzamy odpowiednio zbiór konfiguracji o:


Linia 317: Linia 316:
Czy instrukcje <math>\mathbf{exit}</math> i <math>\mathbf{continue}</math> będą faktycznie wykonywane w takich konfiguracjach?
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 (ś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}\,</math>:
Oczywiście "beneficjentem" korzystającym z tej informacji jest instrukcja <math>\mathbf{loop}\,</math>:


<math>
<math>
Linia 330: Linia 329:
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ę.
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.


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


<math>
<math>
Linia 349: Linia 348:
</math>
</math>


Okazuje się że nie, ponieważ ślad powinien zostać zawsze ,,wymazany" przez pętlę <math>\mathbf{loop}\,</math>.
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 392: Linia 391:
<div class="mw-collapsible mw-made=collapsible mw-collapsed"><div class="mw-collapsible-content" style="display:none">
<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 zapewnić pomijanie instrukcji w sytuacji, gdy został juz zarejestrowany jakiś ślad. Było to dość uciążliwe.
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.
Okazuje się, że podejście mało-krokowe oferuje możliwość bardziej eleganckiego rozwiązania.
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.
Punktem startowym sę teraz reguły mało-krokowe dla języka TINY.


Podobnie jak poprzednio rozszerzymy zbiór konfiguracji i podobnie opiszemy, jak powstaje ślad:
Podobnie jak poprzednio, rozszerzymy zbiór konfiguracji i podobnie opiszemy, jak powstaje ślad:


<math>
<math>
Linia 414: Linia 413:
</math>
</math>


Nie musimy zajmowac się przypadkiem, gdy ślad powstaje w <math>I_2</math>, bo wybraliśmy podejście mało-krokowe.
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}\,</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!


Linia 427: Linia 426:
</math>
</math>


Reguły te są prawie identyczne do reguł semantyki naturalnej dla tej sytuacji!  
Reguły te są prawie identyczne z regułami semantyki naturalnej dla tej 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łokrokowym 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'''!
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.
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>.  
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 tak, aby możliwe było jednorazowe rozwinięcie pętli <math>\mathbf{loop}\,</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}\,</math>:


<math>
<math>
Linia 460: Linia 459:
</math>
</math>


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.
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.
Zatem ostatecznie nasze reguły mogą wyglądać tak:
Zatem ostatecznie nasze reguły mogą wyglądać tak:


Linia 508: Linia 507:
{{cwiczenie|1|cw1.dom|
{{cwiczenie|1|cw1.dom|


Zaproponuj semantykę mało-krokową dla rozszerzeń języka Tiny, które
Zaproponuj semantykę małokrokową dla rozszerzeń języka Tiny, które
studiowaliśmy powyżej.
studiowaliśmy powyżej.
}}
}}
Linia 515: Linia 514:
{{cwiczenie|2|cw2.dom|
{{cwiczenie|2|cw2.dom|


Napisz semantyję naturalną dla nieznacznie rozszerzonej wersji instrukcji <math>\mathbf{loop}\,</math>:
Napisz semantykę naturalną dla nieznacznie rozszerzonej wersji instrukcji <math>\mathbf{loop}\,</math>:


<math>
<math>
Linia 543: 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}\,</math> należy każda z trzech ostatnich instrukcji przypisania.  
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}\,</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 549: Linia 548:
{{cwiczenie|3|cw3.dom|
{{cwiczenie|3|cw3.dom|


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


<math>
<math>
Linia 561: Linia 560:


Obliczenie wyrażenia <math>\,\mathbf{do}\, I \,\mathbf{then}\, e</math> polega na wykonaniu <math>I</math> a potem na obliczeniu <math>e</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>.  
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>.
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>.
}}
}}

Wersja z 12:11, 29 wrz 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::=…|e1/e2

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łokrokową dla rozszerzeń języka Tiny, które studiowaliśmy powyżej.


Ćwiczenie 2

Napisz semantykę 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łokrokową dla rozszerzenia języka TINY o wyrażenia z efektami ubocznymi:

e::=…|𝐝𝐨I𝐭𝐡𝐞𝐧e|x:=e|x++|…

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.

Źródło: „https://wazniak.mimuw.edu.pl/index.php?title=Semantyka_i_weryfikacja_programów/Ćwiczenia_3&oldid=59235”