Semantyka i weryfikacja programów/Ćwiczenia 3

Z Studia Informatyczne
< Semantyka i weryfikacja programów
Wersja z dnia 09:29, 5 wrz 2023 autorstwa Luki (dyskusja | edycje) (Zastępowanie tekstu – „,</math>” na „</math>,”)
Przejdź do nawigacjiPrzejdź do wyszukiwania

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:

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 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}\} ,:

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

Identyfikator x 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. 𝐞𝐱𝐢𝐭x kończy teraz najbliższą otaczającą pętlę Parser nie mógł rozpoznać (błąd składni): {\displaystyle \mathbf{loop}\} , o etykiecie x. Podobnie 𝐜𝐨𝐧𝐭𝐢𝐧𝐮𝐞x wznawia najbliższą otaczającą pętlę o etykiecie x.

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 a=3. 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:

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