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

Z Studia Informatyczne
Przejdź do nawigacjiPrzejdź do wyszukiwania
← poprzednia edycja
WizualnieWikikod
m Zastępowanie tekstu – „.↵</math>” na „</math>”
m Zastępowanie tekstu – „,↵</math>” na „</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>.

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:

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


Ć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


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 𝐥𝐨𝐨𝐩 ,:

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=82233”