Semantyka i weryfikacja programów/Ćwiczenia 1: 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
Sl (dyskusja | edycje)
101 edycji
Nie podano opisu zmian
Linia 1: Linia 1:


== Zawartość ==
== Zawartość ==
Linia 96: Linia 95:
to <math>\mathbf{Num} \times \mathbf{State}</math>.
to <math>\mathbf{Num} \times \mathbf{State}</math>.
}}
}}
<!--
'''Uwaga:'''
Tranzycje pierwszej postaci mogłyby również wyglądać
następująco:
<math>
e, s \,\Longrightarrow\, e'.
</math>
Wtedy zbiorem konfiguracji byłby zbiór
<math>
( \mathbf{Exp} \times \mathbf{State} ) \, \cup \, \mathbf{Exp}
</math>
a konfiguracje końcowe pozostałyby bez zmian.
'''(koniec uwagi)'''
-->


Najprostsze są tranzycje prowadzące do konfiguracji końcowej:
Najprostsze są tranzycje prowadzące do konfiguracji końcowej:
Linia 267: Linia 251:
''nieokreślone'', czyli zmienne są niezainicjowane, a odwołanie do  
''nieokreślone'', czyli zmienne są niezainicjowane, a odwołanie do  
niezainicjowanej zmiennej jest uważane za niepoprawne.
niezainicjowanej zmiennej jest uważane za niepoprawne.
}}




===== Przykład =====
{{przyklad|||


<math>
<math>
Linia 275: Linia 260:
\quad \quad \mapsto \quad \quad \mbox{wynik} = 24
\quad \quad \mapsto \quad \quad \mbox{wynik} = 24
</math>  
</math>  
<math>
<math>
\mathbf{let}\, y = 5 \,\mathbf{in}\, \mathbf{let}\, x = (\, \mathbf{let}\, y = 3 \,\mathbf{in}\, y+y \,) \,\mathbf{in}\, x+y
\mathbf{let}\, y = 5 \,\mathbf{in}\, \mathbf{let}\, x = (\, \mathbf{let}\, y = 3 \,\mathbf{in}\, y+y \,) \,\mathbf{in}\, x+y
\quad \quad \mapsto \quad \quad \mbox{wynik} = 11
\quad \quad \mapsto \quad \quad \mbox{wynik} = 11
</math>
</math>
<math>
<math>
\mathbf{let}\, z = 5 \,\mathbf{in}\, x+z
\mathbf{let}\, z = 5 \,\mathbf{in}\, x+z
Linia 284: Linia 271:
zmiennej}\, x
zmiennej}\, x
</math>
</math>
<math>
<math>
\mathbf{let}\, x = 1 \,\mathbf{in}\, \mathbf{let}\, x = x+x \,\mathbf{in}\, x+x
\mathbf{let}\, x = 1 \,\mathbf{in}\, \mathbf{let}\, x = x+x \,\mathbf{in}\, x+x
Linia 399: Linia 387:
'''Wariant 1'''
'''Wariant 1'''
<br>
<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 481: Linia 468:
'''Wariant 2'''
'''Wariant 2'''
<br>
<br>


Zanim przejdziemy do kolejnego wariantu, zastanówmy się czy  
Zanim przejdziemy do kolejnego wariantu, zastanówmy się czy  

Wersja z 08:08, 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ą:

n::=0|1|…

x::=…(identyfikatory)…

e::=n|x|e1+e2|𝐢𝐟e1𝐭𝐡𝐞𝐧e2𝐞𝐥𝐬𝐞e3

Wynikiem wyrażenienia warunkowego 𝐢𝐟e1𝐭𝐡𝐞𝐧e2𝐞𝐥𝐬𝐞e3 jest wartość wyrażenia e2, o ile wyrażenie e1 oblicza się do wartości różnej od zera; w przeciwnym przypadku wynikiem jest wartość wyrażenia e3.

Zaproponuj semantykę operacyjną (małe kroki) dla tego języka.


Rozwiązanie

{{{3}}}


Ćwiczenie 2

Rozszerzmy język wyrażeń z poprzedniego zadania o jedną konstrukcję

e::=…|𝐥𝐞𝐭x=e1𝐢𝐧e2

Wyrażenie 𝐥𝐞𝐭x=e1𝐢𝐧e2 zawiera w sobie deklarację x=e1, która stanowi mechanizm wiązania identyfikatorów w naszym języku. Deklaracja x=e1 wprowadza nową zmienną x oraz przypisuje jej wartość. Wartość wyrażenia 𝐥𝐞𝐭x=e1𝐢𝐧e2 obliczamy następująco: najpierw oblicza się wartość e1, podstawia ją na zmienna x, a następnie oblicza wyrażenie e2. Zakresem zmiennej x jest wyrażenie e2, czyli wewnątrz e2 można odwoływać się (wielokrotnie) do zmiennej x; 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 e2 występuje podwyrażenie 𝐥𝐞𝐭x=…𝐢𝐧e to odwołania do x wewnątrz e odnoszą się do najbliższej deklaracji zmiennej x.

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

𝐥𝐞𝐭x=0𝐢𝐧𝐥𝐞𝐭y=7𝐢𝐧𝐥𝐞𝐭x=y+3𝐢𝐧x+x+y↦wynik=24

𝐥𝐞𝐭y=5𝐢𝐧𝐥𝐞𝐭x=(𝐥𝐞𝐭y=3𝐢𝐧y+y)𝐢𝐧x+y↦wynik=11

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 }

𝐥𝐞𝐭x=1𝐢𝐧𝐥𝐞𝐭x=x+x𝐢𝐧x+x↦wynik=4


Rozwiązanie

{{{3}}}


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 e w stanie s jest niemożliwe bo wystąpił błąd, to

e,s⟹*Blad


Zadanie 3

Rozważ rozszerzenie języka wyrażeń o wyrażenia boolowskie:

n::=0|1|…

x::=…(identyfikatory)…

b::=𝐭𝐫𝐮𝐞|𝐟𝐚𝐥𝐬𝐞|e1≤e2|¬b|b1∧b2

e::=n|x|e1+e2|𝐢𝐟b𝐭𝐡𝐞𝐧e2𝐞𝐥𝐬𝐞e3|𝐥𝐞𝐭x=e1𝐢𝐧e2

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 b1∧b2, gdy b1 zostało obliczone do 𝐟𝐚𝐥𝐬𝐞, nie ma wogóle potrzeby obliczania b2.

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