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

Z Studia Informatyczne
Przejdź do nawigacjiPrzejdź do wyszukiwania
m (Zastępowanie tekstu - "\Longrightarrow\" na "\Longrightarrow")
 
Linia 198: Linia 198:
 
{e_1 / e_2, s \,\longrightarrow\, \mathtt{Blad}}
 
{e_1 / e_2, s \,\longrightarrow\, \mathtt{Blad}}
 
\quad \quad
 
\quad \quad
e_1 / 0, s \,\Longrightarrow\, \mathtt{Blad}.
+
e_1 / 0, s \,\Longrightarrow, \mathtt{Blad}.
 
</math>
 
</math>
  
Linia 210: Linia 210:
 
{e_1 / e_2, s \,\longrightarrow\, \mathtt{Blad}, s}
 
{e_1 / e_2, s \,\longrightarrow\, \mathtt{Blad}, s}
 
\quad \quad
 
\quad \quad
e_1 / 0, s \,\Longrightarrow\, \mathtt{Blad}, s
+
e_1 / 0, s \,\Longrightarrow, \mathtt{Blad}, s
 
</math>
 
</math>
  
Linia 402: Linia 402:
  
 
<math>
 
<math>
\mathbf{exit}, s \,\Longrightarrow\, s, \mbox{było-}\mathbf{exit}
+
\mathbf{exit}, s \,\Longrightarrow, s, \mbox{było-}\mathbf{exit}
 
\quad \quad
 
\quad \quad
\mathbf{continue}, s \,\Longrightarrow\, s, \mbox{było-}\mathbf{continue}.
+
\mathbf{continue}, s \,\Longrightarrow, s, \mbox{było-}\mathbf{continue}.
 
</math>
 
</math>
  
Linia 410: Linia 410:
  
 
<math>
 
<math>
\frac{I_1, s \,\Longrightarrow\, s', \mbox{było-}\mathbf{exit}}
+
\frac{I_1, s \,\Longrightarrow, s', \mbox{było-}\mathbf{exit}}
     {I_1;\, I_2, s \,\Longrightarrow\, s', \mbox{było-}\mathbf{exit}}
+
     {I_1;\, I_2, s \,\Longrightarrow, s', \mbox{było-}\mathbf{exit}}
 
\quad \quad
 
\quad \quad
 
\mbox{ i analogicznie dla } \mbox{było-}\mathbf{continue}.
 
\mbox{ i analogicznie dla } \mbox{było-}\mathbf{continue}.
Linia 422: Linia 422:
  
 
<math>
 
<math>
\frac{I, s \,\Longrightarrow\, s', \mbox{było-}\mathbf{exit}}
+
\frac{I, s \,\Longrightarrow, s', \mbox{było-}\mathbf{exit}}
     {\mathbf{loop}\, I, s \,\Longrightarrow\, s'}
+
     {\mathbf{loop}\, I, s \,\Longrightarrow, s'}
 
\quad \quad
 
\quad \quad
\frac{I, s \,\Longrightarrow\, s', \mbox{było-}\mathbf{continue}}
+
\frac{I, s \,\Longrightarrow, s', \mbox{było-}\mathbf{continue}}
     {\mathbf{loop}\, I, s \,\Longrightarrow\, \mathbf{loop}\, I, s'}
+
     {\mathbf{loop}\, I, s \,\Longrightarrow, \mathbf{loop}\, I, s'}
 
</math>
 
</math>
  
Linia 439: Linia 439:
  
 
<math>
 
<math>
\mathbf{loop}\, I, s \,\Longrightarrow\, I \,\mathbf{then}\, \mathbf{loop}\, I, s.
+
\mathbf{loop}\, I, s \,\Longrightarrow, I \,\mathbf{then}\, \mathbf{loop}\, I, s.
 
</math>
 
</math>
  
Linia 445: Linia 445:
  
 
<math>
 
<math>
\frac{I', s \,\Longrightarrow\, s', \mbox{było-}\mathbf{exit}}
+
\frac{I', s \,\Longrightarrow, s', \mbox{było-}\mathbf{exit}}
     {I' \,\mathbf{then}\, \mathbf{loop}\, I, s \,\Longrightarrow\, s'}
+
     {I' \,\mathbf{then}\, \mathbf{loop}\, I, s \,\Longrightarrow, s'}
 
\quad \quad
 
\quad \quad
\frac{I', s \,\Longrightarrow\, s', \mbox{było-}\mathbf{continue}}
+
\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
 
\quad \quad
\frac{I', s \,\Longrightarrow\, s'}
+
\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>
 
</math>
  
Linia 458: Linia 458:
  
 
<math>
 
<math>
\frac{I', s \,\Longrightarrow\, I'', s'}
+
\frac{I', s \,\Longrightarrow, I'', s'}
     {I' \,\mathbf{then}\, \mathbf{loop}\, I, s \,\Longrightarrow\, I'' \,\mathbf{then}\, \mathbf{loop}\, I, s'}
+
     {I' \,\mathbf{then}\, \mathbf{loop}\, I, s \,\Longrightarrow, I'' \,\mathbf{then}\, \mathbf{loop}\, I, s'}
 
</math>
 
</math>
  
Linia 466: Linia 466:
  
 
<math>
 
<math>
\mathbf{exit}, s \,\Longrightarrow\, \mbox{było-}\mathbf{exit}
+
\mathbf{exit}, s \,\Longrightarrow, \mbox{było-}\mathbf{exit}
 
\quad \quad
 
\quad \quad
\mathbf{continue}, s \,\Longrightarrow\, \mbox{było-}\mathbf{continue}
+
\mathbf{continue}, s \,\Longrightarrow, \mbox{było-}\mathbf{continue}
 
</math>
 
</math>
  
 
<math>
 
<math>
\frac{I_1, s \,\Longrightarrow\, \mbox{było-}\mathbf{exit}}
+
\frac{I_1, s \,\Longrightarrow, \mbox{było-}\mathbf{exit}}
     {I_1;\, I_2, s \,\Longrightarrow\, \mbox{było-}\mathbf{exit}}
+
     {I_1;\, I_2, s \,\Longrightarrow, \mbox{było-}\mathbf{exit}}
 
\quad \quad
 
\quad \quad
\frac{I_1, s \,\Longrightarrow\, \mbox{było-}\mathbf{continue}}
+
\frac{I_1, s \,\Longrightarrow, \mbox{było-}\mathbf{continue}}
     {I_1;\, I_2, s \,\Longrightarrow\, \mbox{było-}\mathbf{continue}}
+
     {I_1;\, I_2, s \,\Longrightarrow, \mbox{było-}\mathbf{continue}}
 
</math>
 
</math>
  
 
<math>
 
<math>
\mathbf{loop}\, I, s \,\Longrightarrow\, I \,\mathbf{then}\, \mathbf{loop}\, I, s.
+
\mathbf{loop}\, I, s \,\Longrightarrow, I \,\mathbf{then}\, \mathbf{loop}\, I, s.
 
</math>
 
</math>
  
 
<math>
 
<math>
\frac{I', s \,\Longrightarrow\, \mbox{było-}\mathbf{exit}}
+
\frac{I', s \,\Longrightarrow, \mbox{było-}\mathbf{exit}}
     {I' \,\mathbf{then}\, \mathbf{loop}\, I, s \,\Longrightarrow\, s}
+
     {I' \,\mathbf{then}\, \mathbf{loop}\, I, s \,\Longrightarrow, s}
 
\quad \quad
 
\quad \quad
\frac{I', s \,\Longrightarrow\, \mbox{było-}\mathbf{continue}}
+
\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
 
\quad \quad
\frac{I', s \,\Longrightarrow\, s'}
+
\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>
 
</math>
  
 
<math>
 
<math>
\frac{I', s \,\Longrightarrow\, I'', s'}
+
\frac{I', s \,\Longrightarrow, I'', s'}
     {I' \,\mathbf{then}\, \mathbf{loop}\, I, s \,\Longrightarrow\, I'' \,\mathbf{then}\, \mathbf{loop}\, I, s'}
+
     {I' \,\mathbf{then}\, \mathbf{loop}\, I, s \,\Longrightarrow, I'' \,\mathbf{then}\, \mathbf{loop}\, I, s'}
 
</math>
 
</math>
  

Aktualna wersja na dzień 14:16, 9 cze 2020

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:

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

Identyfikator pełni tutaj rolę etykiety związanej z instrukcją , jest też parametrem dwóch pozostałych instrukcji. kończy teraz najbliższą otaczającą pętlę o etykiecie . Podobnie wznawia najbliższą otaczającą pętlę o etykiecie .

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


Ć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ą .