Semantyka i weryfikacja programów/Ćwiczenia 1: Różnice pomiędzy wersjami
Nie podano opisu zmian |
Nie podano opisu zmian |
||
| Linia 42: | Linia 42: | ||
{{rozwiazanie||roz1| | {{rozwiazanie||roz1| | ||
<div class="mw-collapsible mw-made=collapsible mw-collapsed"><div class="mw-collapsible-content" style="display:none"> | |||
Zacznijmy od ustalenia notacji i dziedzin syntaktycznych. | Zacznijmy od ustalenia notacji i dziedzin syntaktycznych. | ||
| Linia 89: | Linia 90: | ||
a konfiguracje końcowe to <math>\mathbf{Num}</math>. | a konfiguracje końcowe to <math>\mathbf{Num}</math>. | ||
{{ | |||
uwaga||uwaga1| | |||
Tak naprawdę to druga postać tranzycji nie jest | |||
niezbędna, gdyż moglibyśmy umówić się, że konfiguracje końcowe | niezbędna, gdyż moglibyśmy umówić się, że konfiguracje końcowe | ||
to <math>\mathbf{Num} \times \mathbf{State}</math>. | to <math>\mathbf{Num} \times \mathbf{State}</math>. | ||
}} | |||
<!-- | <!-- | ||
| Linia 115: | Linia 118: | ||
</math> | </math> | ||
Symbol <math>n</math> po lewej stronie to wyrażenie składające się | |||
ze stałej, podczas gdy <math>n</math> po prawej stronie reprezentuje liczbę | ze stałej liczbowej, podczas gdy <math>n</math> po prawej stronie reprezentuje liczbę | ||
będącą wartością wyrażenia. | będącą wartością wyrażenia. | ||
| Linia 136: | Linia 139: | ||
</math> | </math> | ||
Reguły tej postaci | Reguły tej postaci będziemy zapisywać tak: | ||
<math> | |||
\frac{e_1, s \,\Longrightarrow\, e'_1, s} | \frac{e_1, s \,\Longrightarrow\, e'_1, s} | ||
{e_1 + e_2, s \,\Longrightarrow\, e'_1 + e_2, s} | {e_1 + e_2, s \,\Longrightarrow\, e'_1 + e_2, s} | ||
</math> | </math> | ||
| Linia 157: | Linia 160: | ||
</math> | </math> | ||
Zwróćmy tutaj uwagę na pewną subtelność, dotyczącą dwóch wystąpień | |||
symbolu | symbolu <math>+</math>: pierwsze wystąpienie oznacza jedną z konstrukcji składniowych | ||
języka, a drugie oznacza operację dodawania w zbiorze <math>\mathbf{Num}</math>. | języka, a drugie oznacza operację dodawania w zbiorze <math>\mathbf{Num}</math>. | ||
Pozwalamy sobie na taką kolizję oznaczeń, gdyż nie powinna ona | Pozwalamy sobie na taką kolizję oznaczeń, gdyż nie powinna ona | ||
prowadzić do niejednoznaczności. Pamiętajmy, że składnia języka jest | prowadzić do niejednoznaczności. Pamiętajmy, że składnia języka jest | ||
składnią | składnią abstrakcyjną, więc zamiast <math>e_1 + e_2</math> moglibyśmy równie | ||
dobrze pisać np. <math>{\mathrm{add}}(e_1, e_2)</math> | dobrze pisać np. <math>{\mathrm{add}}(e_1, e_2)</math> a wtedy reguła | ||
wyglądałaby tak: | |||
<math> | |||
\mathrm{add}(n_1, n_2), s \,\Longrightarrow\, n, s \quad \mbox{ o ile } n = n_1 + n_2. | |||
</math> | |||
Inną możliwą strategią obliczania <math>e_1 + e_2</math> jest strategia | |||
''prawostronna'', którą otrzymujemy zastępując pierwsze dwie z trzech | ''prawostronna'', którą otrzymujemy zastępując pierwsze dwie z trzech | ||
powyższych reguł przez: | powyższych reguł przez: | ||
| Linia 223: | Linia 231: | ||
</math> | </math> | ||
</div></div> | |||
}} | }} | ||
| Linia 261: | Linia 269: | ||
===== | ===== Przykład ===== | ||
<math> | <math> | ||
| Linia 285: | Linia 293: | ||
{{rozwiazanie||roz2| | {{rozwiazanie||roz2| | ||
<div class="mw-collapsible mw-made=collapsible mw-collapsed"><div class="mw-collapsible-content" style="display:none"> | |||
Podobnie jak poprzednio, | Podobnie jak poprzednio, | ||
| Linia 387: | Linia 396: | ||
<br> | |||
'''Wariant 1''' | |||
<br> | |||
Wygodne i eleganckie rozwiązanie tego problemu jest możliwe, jeśli | Wygodne i eleganckie rozwiązanie tego problemu jest możliwe, jeśli | ||
| Linia 414: | Linia 426: | ||
</math> | </math> | ||
Wyrażenie <math>e \,\mathbf{then}\, x:= n</math> jest w pewnym sensie dualne | |||
do <math>\mathbf{let}\, x = n \,\mathbf{in}\, e</math>, gdyż jedyna (choc niewątpliwie istotna) różnica | do <math>\mathbf{let}\, x = n \,\mathbf{in}\, e</math>, gdyż jedyna (choc niewątpliwie istotna) różnica | ||
między nimi to kolejność obliczenia <math>e</math> i przypisania wartości | między nimi to kolejność obliczenia <math>e</math> i przypisania wartości | ||
| Linia 466: | Linia 478: | ||
<br> | |||
'''Wariant 2''' | |||
<br> | |||
Zanim przejdziemy do kolejnego wariantu, zastanówmy się czy | Zanim przejdziemy do kolejnego wariantu, zastanówmy się czy | ||
| Linia 501: | Linia 516: | ||
Trzeba jednak w takim razie zadbać o to, aby wyrażenie <math>\mathbf{let}\, x = e_1 | Trzeba jednak w takim razie zadbać o to, aby wyrażenie <math>\mathbf{let}\, x = e_1 | ||
in e_2</math> obliczało się normalnie tylko wtedy, gdy wartość | \,\mathbf{in}\, e_2</math> obliczało się normalnie tylko wtedy, gdy wartość | ||
wyrażenia <math>e_1</math> jest różna od <math>\bot</math>. | wyrażenia <math>e_1</math> jest różna od <math>\bot</math>. | ||
<br> | |||
'''Wariant 3''' | |||
<br> | |||
Zrewidujmy teraz podstawowe założenia, które dotychczas poczyniliśmy. | Zrewidujmy teraz podstawowe założenia, które dotychczas poczyniliśmy. | ||
| Linia 568: | Linia 585: | ||
Niekiedy jednak rozszerzanie języka będzie zabronione. | Niekiedy jednak rozszerzanie języka będzie zabronione. | ||
</div></div> | |||
}} | }} | ||
| Linia 611: | Linia 628: | ||
b \, ::= \,\, | b \, ::= \,\, | ||
\mathbf{true} \,\,|\,\, | \mathbf{true} \,\,|\,\, | ||
\mathbf{ | \mathbf{false} \,\,|\,\, | ||
e_1 \leq e_2 \,\,|\,\, | e_1 \leq e_2 \,\,|\,\, | ||
\neg b \,\,|\,\, | \neg b \,\,|\,\, | ||
| Linia 630: | Linia 647: | ||
Rozważ różne strategie obliczania wyrażeń boolowskich, oraz podejście leniwe. | Rozważ różne strategie obliczania wyrażeń boolowskich, oraz podejście leniwe. | ||
Na przykład w strategii lewostronnej dla <math>b_1 \land b_2</math>, | Na przykład w strategii lewostronnej dla <math>b_1 \land b_2</math>, | ||
gdy <math>b_1</math> zostało obliczone do <math>\mathbf{ | gdy <math>b_1</math> zostało obliczone do <math>\mathbf{false}</math>, nie ma wogóle potrzeby | ||
obliczania <math>b_2</math>. | obliczania <math>b_2</math>. | ||
Wersja z 07:56, 8 sie 2006
Zawartość
Tematem tych zajęć jest semantyka operacyjna wyrażeń (małe kroki).
Zadania z rozwiązaniami
Ćwiczenie 1
Rozważmy bardzo prosty język wyrażeń, którego składnia opisana jest następującą gramatyką:
Wynikiem wyrażenienia warunkowego jest wartość wyrażenia , o ile wyrażenie oblicza się do wartości różnej od zera; w przeciwnym przypadku wynikiem jest wartość wyrażenia .
Zaproponuj semantykę operacyjną (małe kroki) dla tego języka.
Rozwiązanie
Ćwiczenie 2
Rozszerzmy język wyrażeń z poprzedniego zadania o jedną konstrukcję
Wyrażenie zawiera w sobie deklarację , która stanowi mechanizm wiązania identyfikatorów w naszym języku. Deklaracja wprowadza nową zmienną oraz przypisuje jej wartość. Wartość wyrażenia obliczamy następująco: najpierw oblicza się wartość , podstawia ją na zmienna , a następnie oblicza wyrażenie . Zakresem zmiennej jest wyrażenie , czyli wewnątrz można odwoływać się (wielokrotnie) do zmiennej ; Ogólniej, odwołania do zmiennej w wyrażeniu odnoszą się do najbliższej (najbardziej zagnieżdzonej) deklaracji tej zmiennej. Taki mechanizm wiązania identyfikatorów nazywamy wiązaniem statycznym. Przyjmujemy zwykłe reguły przesłaniania zmiennych. Np., jeśli w występuje podwyrażenie to odwołania do wewnątrz odnoszą się do najbliższej deklaracji zmiennej .
Zakładamy, że na początku wartości wszystkich zmiennych są nieokreślone, czyli zmienne są niezainicjowane, a odwołanie do niezainicjowanej zmiennej jest uważane za niepoprawne.
Przykład
Parser nie mógł rozpoznać (błąd składni): {\displaystyle \mathbf{let}\, z = 5 \,\mathbf{in}\, x+z \quad \quad \mapsto \quad \quad \mbox{brak wyniku; odwołanie do niezainicjowanej zmiennej}\, x }
Rozwiązanie
Zadania domowe
Zadanie 1
Zapisz wariant 2 semantyki z poprzedniego zadania.
Zadanie 2
Dotychczas wystąpienie błędu podczas obliczania wyrażenia, np. odwołanie do niezainicjowanej zmiennej, powodowało, że wyrażenie nie posiadało wartości (nie było ciągu tranzycji prowadzących do konfiguracji końcowej). Zmodyfikuj którąś z semantyk z poprzednich zadań tak, aby błąd był komunikowany jako jedna z konfiguracji końcowych. To znaczy: jeśli obliczenie wyrażenia w stanie jest niemożliwe bo wystąpił błąd, to
Zadanie 3
Rozważ rozszerzenie języka wyrażeń o wyrażenia boolowskie:
Zaproponuj semantykę małych kroków dla tego języka. Rozważ różne strategie obliczania wyrażeń boolowskich, oraz podejście leniwe. Na przykład w strategii lewostronnej dla , gdy zostało obliczone do , nie ma wogóle potrzeby obliczania .
