Semantyka i weryfikacja programów/Ćwiczenia 7: Różnice pomiędzy wersjami
Nie podano opisu zmian |
m Zastępowanie tekstu – „<math> ” na „<math>” |
||
(Nie pokazano 42 wersji utworzonych przez 4 użytkowników) | |||
Linia 1: | Linia 1: | ||
== Semantyka bezpośrednia instrukcji. Konstrukcje iteracyjne. == | == Semantyka bezpośrednia instrukcji. Konstrukcje iteracyjne. == | ||
=== | === Pętle '''while''' i '''repeat''' === | ||
{{cwiczenie|1|cw1| | |||
Zdefiniuj semantykę denotacyjną następującego języka: | Zdefiniuj semantykę denotacyjną następującego języka: | ||
<math> | <math> | ||
n \, ::= \,\, 0 \,\,|\,\, 1 \,\,|\,\, \ldots | n \, ::= \ldots \,\, -1\,\,|\,\, 0 \,\,|\,\, 1 \,\,|\,\, \ldots | ||
</math> | </math> | ||
Linia 16: | Linia 18: | ||
n \,\,|\,\, | n \,\,|\,\, | ||
x \,\,|\,\, | x \,\,|\,\, | ||
e_1 | e_1\,\, + \,\, e_2 | ||
</math> | </math> | ||
<math> | <math> | ||
b \, ::= \,\, | b \, ::= \,\, | ||
e_1 = e_2 \,\,|\,\, | e_1\, = \, e_2 \,\,|\,\, | ||
\mathbf{not}\, b \,\,|\,\, | \mathbf{not}\,\, b \,\,|\,\, | ||
b_1\, \mathbf{or} | b_1\,\, \mathbf{or}\,\, b_2 | ||
</math> | </math> | ||
<math> | <math> | ||
i \, ::= \,\, | i \, ::= \,\, | ||
x := e \,\,|\,\, | x\, :=\, e \,\,|\,\, | ||
i_1; i_2 \,\,|\,\, | i_1; i_2 \,\,|\,\, | ||
\mathbf{if}\, b \,\mathbf{then}\, i_1 \,\mathbf{else}\, i_2 \,\,|\,\, | \mathbf{if}\,\, b \,\,\mathbf{then}\,\, i_1 \,\,\mathbf{else}\,\, i_2 \,\,|\,\, | ||
\mathbf{skip} \,\,|\,\, | \mathbf{skip} \,\,|\,\, | ||
\mathbf{while}\, b \,\mathbf{do}\, i \,\,|\,\, | \mathbf{while}\,\, b \,\,\mathbf{do}\,\, i \,\,|\,\, | ||
\mathbf{repeat}\, i \,\mathbf{until} | \mathbf{repeat}\,\, i \,\mathbf{until}\,\, b | ||
</math> | </math> | ||
Pętla <math> \mathbf{repeat}\, i \,\mathbf{until}\, b </math> polega na wykonaniu instrukcji ''i'', a następnie wyliczeniu warunku logicznego ''b''. Jeśli warunek jest prawdziwy wykonanie pętli kończy się, w przeciwnym razie powracamy do wykonania instrukcji ''i''. | Pętla <math>\mathbf{repeat}\,\, i \,\,\mathbf{until}\,\, b</math> polega na wykonaniu instrukcji ''i'', a następnie wyliczeniu warunku logicznego ''b''. Jeśli warunek jest prawdziwy, wykonanie pętli kończy się, w przeciwnym razie powracamy do wykonania instrukcji ''i''. | ||
}} | |||
<!-- | |||
Powyższy język to tak naprawdę TINY z wykładu rozszerzony o jedną | |||
konstrukcję: pętlę '''repeat'''. Spróbuj wykonać to ćwiczenie nie | |||
sięgając do notatek z wykładu. Jeśli napotkasz trudności, odkrywaj | |||
kolejne elementy poniższego opisu. | |||
Kategorie składniowe występujące w tym języku to: | |||
* wyrażenia Exp | |||
* wyrażenia logiczne BExp | |||
* instrukcje Stmt | |||
* oraz, jak zwykle, stałe liczbowe Num | |||
Zaczynamy jak zwykle od opisu dziedzin semantycznych. Nie przejmujemy | |||
się na razie szczegółami związanymi z konstrukcjami stałopunktowymi | |||
oraz umieszczeniem pinezki we właściwych dziedzinach. Zakładamy, że | |||
wszystkie zmienne są zainicjowane na zero. | |||
Użyjemy elementarnych dziedzin z wykładu: | |||
* Int <nowiki>=</nowiki> ..., -1, 0, 1, ... zawierający denotacje stałych | |||
liczbowych | |||
* Bool <nowiki>=</nowiki> {tt}, {ff} zawierający wartości logiczne | |||
* Var zawierający wszystkie dozwolone identyfikatory | |||
<div class="mw-collapsible mw-made=collapsible mw-collapsed"> | |||
Przypomnijmy, że wartość wyrażenia arytmetycznego <math>e</math> zależy od | |||
<div class="mw-collapsible-content" style="display:none"> | |||
wartości wszystkich występujących w nim zmiennych. | |||
</div> | |||
</div> | |||
Wartości te są "pamiętane" w stanie, który jest funkcją ze zbioru | |||
Var w zbiór Int. Zbiór wszystkich stanów to: | |||
<center><math>State = Var \rightarrow Int</math></center> | |||
Zdefiniujmy następnie niezbędne funkcje semantyczne. | |||
* Dla wyrażeń mamy | |||
<center><math>\mathcal{E} & : & \mathrm Exp \rightarrow \mathrm State \rightarrow \mathrm Int</math></center> | |||
* Dla wyrażeń logicznych: | |||
<center><math>\mathcal{B} & : & \mathrm BExp \rightarrow \mathrm State \rightarrow \mathrm Bool</math></center> | |||
* Dla instrukcji: | |||
<center><math>\mathcal{I} & : & \mathrm Stmt \rightarrow \mathrm State \rightarrow \mathrm State</math></center> | |||
* Oraz oczywistą funkcję dla stałych całkowitych: | |||
<center><math>\mathcal{Z} & : & \mathrm Num \rightarrow \mathcal{Z}</math></center> | |||
Funkcji {Z} nie definiujemy, przyjmując jak zwykle, że jej wynikiem | |||
jest wartość stałej liczbowej. | |||
Rozpocznijmy od funkcji semantycznej dla wyrażeń. Musimy zdefiniować | |||
znaczenie (wartość) wyrażenia <math>e</math> w pewnym stanie <math>s</math>. Ową wartość | |||
zapisujemy jako <math>\mathcal{E} [\![e]\!] s</math>, czyli wartość funkcji E zastosowanej do | |||
dwóch argumentów: wyrażenia <math>e</math> oraz stanu <math>s</math>. Przypomnijmy, że taka | |||
"dziwna" notacja z nawiasami służy oddzieleniu składni od elementów | |||
z metajęzyka. | |||
Funkcje semantyczne definiujemy dla każdej postaci wyrażenia, | |||
odpowiadając na standardowe pytania: | |||
# Co jest wartością wyrażenia <math>x</math> w stanie <math>s</math>? Odpowiedź: wartość | |||
zmiennej <math>x</math> w tym stanie, czyli wartość uzyskana przez zastosowanie | |||
funkcji <math>s</math> do identyfikatora <math>x</math>. Zapisujemy to następująco: | |||
<center><math>\mathcal{E} [\![x]\!] s = s (x)</math></center> | |||
Często będziemy pomijać nawiasy przy aplikacji funkcji pisząc po | |||
prostu <math>s\,x</math> zamiast <math>s(x)</math>. To samo można zapisać stosując notację | |||
"lambda": | |||
=== | <center><math>\mathcal{E} [\![x]\!] = \l s \in \mathrm State.s (x)</math></center> | ||
--> | |||
=== Pętla '''for''' === | |||
{{cwiczenie|2|cw2| | |||
Rozszerzmy język z poprzedniego zadania o instrukcję: | Rozszerzmy język z poprzedniego zadania o instrukcję: | ||
Linia 51: | Linia 130: | ||
# Jeśli <math>x > m</math>, to pętla kończy się. | # Jeśli <math>x > m</math>, to pętla kończy się. | ||
# W przeciwnym razie: | # W przeciwnym razie: | ||
#* Wykonujemy instrukcję <math> i </math>. | #* Wykonujemy instrukcję <math>i</math>. | ||
#* Zwiększamy zmienną <math>x</math> o 1. | #* Zwiększamy zmienną <math>x</math> o 1. | ||
#* Powracamy do punktu 3. | #* Powracamy do punktu 3. | ||
Zauważmy, że wyrażenie <math>e_1</math> jest tu wyliczane tylko raz, ale <math>e_2</math> oblicza się przy każdym obrocie pętli. | Zauważmy, że wyrażenie <math>e_1</math> jest tu wyliczane tylko raz, ale <math>e_2</math> oblicza się przy każdym obrocie pętli. | ||
}} | |||
<div class="mw-collapsible mw-made=collapsible mw-collapsed"> | |||
<span class="mw-collapsible-toogle mw-collapsible-toogle-default style="font-variant:small-caps">Rozwiązanie</span> | |||
<div class="mw-collapsible-content" style="display:none"> | |||
Jeszcze nie ma. | |||
</div> | |||
</div> | |||
{{cwiczenie|3|cw3| | |||
Zmieńmy semantykę instrukcji for z poprzedniego zadania tak, aby | Zmieńmy semantykę instrukcji for z poprzedniego zadania tak, aby | ||
oba wyrażenia obliczały się tylko raz. Tym razem wyliczenie pętli polega na: | oba wyrażenia obliczały się tylko raz. Tym razem wyliczenie pętli polega na: | ||
Linia 67: | Linia 156: | ||
#* Zwiększamy zmienną <math>x</math> o 1. | #* Zwiększamy zmienną <math>x</math> o 1. | ||
#* Powracamy do punktu 4. | #* Powracamy do punktu 4. | ||
}} | |||
<div class="mw-collapsible mw-made=collapsible mw-collapsed"> | |||
<span class="mw-collapsible-toogle mw-collapsible-toogle-default style="font-variant:small-caps">Rozwiązanie</span> | |||
<div class="mw-collapsible-content" style="display:none"> | |||
Jeszcze nie ma. | |||
</div> | |||
</div> | |||
{{cwiczenie| 4|cw4| | |||
O pętli '''for''' można jednak myśleć jeszcze inaczej. Można wymagać, aby wszelkie zmiany wartości zmiennej sterującej <math>x</math> wewnątrz wykonania pętli nie miały wpływu na liczbę iteracji tej pętli. Przykładowo przy semantyce z poprzedniego zadania pętla: | |||
'''for''' x :<nowiki>=</nowiki> 1 '''to''' 10 '''do''' | |||
x:<nowiki>=</nowiki> x + 1; | |||
y:<nowiki>=</nowiki> y + x; | |||
wykonuje się pięć razy, a zmienna <math>y</math> jest zwiększana łącznie o 2+4+6+8+10. Jeśli uznamy, że zmiany zmiennej <math>x</math> wewnątrz pętli nie wpływają na liczbę iteracji, to pętla wykona się 10 razy, a zmienna <math>y</math> zostanie zwiększona o 2+3+4+5+6+7+8+9+10+11. | |||
Zdefiniuj taką semantykę. | |||
}} | |||
<div class="mw-collapsible mw-made=collapsible mw-collapsed"> | |||
<span class="mw-collapsible-toogle mw-collapsible-toogle-default style="font-variant:small-caps">Rozwiązanie</span> | |||
<div class="mw-collapsible-content" style="display:none"> | |||
Jeszcze nie ma. | |||
</div> | |||
</div> | |||
{{cwiczenie|5|cw5| | |||
W języku C pętla '''for''' ma następującą postać: | W języku C pętla '''for''' ma następującą postać: | ||
<math> | <math> | ||
Linia 86: | Linia 196: | ||
# Jeśli wyrażenie wylicza się do fałszu, to pętla kończy się. | # Jeśli wyrażenie wylicza się do fałszu, to pętla kończy się. | ||
# W przeciwnym razie: | # W przeciwnym razie: | ||
#* Wykonujemy instrukcję <math> i_3 </math>. | #* Wykonujemy instrukcję <math>i_3</math>. | ||
#* Wykonujemy instrukcję <math> i_2 </math>. | #* Wykonujemy instrukcję <math>i_2</math>. | ||
#* Powracamy do punktu 2. | #* Powracamy do punktu 2. | ||
}} | |||
<div class="mw-collapsible mw-made=collapsible mw-collapsed"> | |||
<span class="mw-collapsible-toogle mw-collapsible-toogle-default style="font-variant:small-caps">Rozwiązanie</span> | |||
<div class="mw-collapsible-content" style="display:none"> | |||
Jeszcze nie ma. | |||
</div> | |||
</div> |
Aktualna wersja na dzień 22:13, 11 wrz 2023
Semantyka bezpośrednia instrukcji. Konstrukcje iteracyjne.
Pętle while i repeat
Ćwiczenie 1
Zdefiniuj semantykę denotacyjną następującego języka:
Pętla polega na wykonaniu instrukcji i, a następnie wyliczeniu warunku logicznego b. Jeśli warunek jest prawdziwy, wykonanie pętli kończy się, w przeciwnym razie powracamy do wykonania instrukcji i.
Pętla for
Ćwiczenie 2
Rozszerzmy język z poprzedniego zadania o instrukcję:
Wykonanie takiej pętli polega na:
- Wyliczeniu wartości wyrażenia .
- Przypisaniu wartości na zmienną .
- Wyliczeniu wartości wyrażenia .
- Jeśli , to pętla kończy się.
- W przeciwnym razie:
- Wykonujemy instrukcję .
- Zwiększamy zmienną o 1.
- Powracamy do punktu 3.
Zauważmy, że wyrażenie jest tu wyliczane tylko raz, ale oblicza się przy każdym obrocie pętli.
Rozwiązanie
Ćwiczenie 3
Zmieńmy semantykę instrukcji for z poprzedniego zadania tak, aby oba wyrażenia obliczały się tylko raz. Tym razem wyliczenie pętli polega na:
- Wyliczeniu wartości wyrażenia .
- Przypisaniu wartości na zmienną .
- Wyliczeniu wartości wyrażenia .
- Jeśli , to pętla kończy się.
- W przeciwnym razie:
- Wykonujemy instrukcję .
- Zwiększamy zmienną o 1.
- Powracamy do punktu 4.
Rozwiązanie
Ćwiczenie 4
O pętli for można jednak myśleć jeszcze inaczej. Można wymagać, aby wszelkie zmiany wartości zmiennej sterującej wewnątrz wykonania pętli nie miały wpływu na liczbę iteracji tej pętli. Przykładowo przy semantyce z poprzedniego zadania pętla:
for x := 1 to 10 do x:= x + 1; y:= y + x;
wykonuje się pięć razy, a zmienna jest zwiększana łącznie o 2+4+6+8+10. Jeśli uznamy, że zmiany zmiennej wewnątrz pętli nie wpływają na liczbę iteracji, to pętla wykona się 10 razy, a zmienna zostanie zwiększona o 2+3+4+5+6+7+8+9+10+11. Zdefiniuj taką semantykę.
Rozwiązanie
Ćwiczenie 5
W języku C pętla for ma następującą postać:
Jej wykonanie polega na:
- Wykonaniu instrukcji .
- Wyliczeniu wartości wyrażenia .
- Jeśli wyrażenie wylicza się do fałszu, to pętla kończy się.
- W przeciwnym razie:
- Wykonujemy instrukcję .
- Wykonujemy instrukcję .
- Powracamy do punktu 2.
Rozwiązanie