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

← poprzednia edycja

WizualnieWikikod

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:

$n : : = \dots - 1 | 0 | 1 | \dots$

$x : : = \dots (i d e n t y f i k a t o r y) \dots$

$e : : = n | x | e_{1} + e_{2}$

$b : : = e_{1} = e_{2} | 𝐧 𝐨 𝐭 b | b_{1} 𝐨 𝐫 b_{2}$

$i : : = x : = e | i_{1}; i_{2} | 𝐢 𝐟 b 𝐭 𝐡 𝐞 𝐧 i_{1} 𝐞 𝐥 𝐬 𝐞 i_{2} | 𝐬 𝐤 𝐢 𝐩 | 𝐰 𝐡 𝐢 𝐥 𝐞 b 𝐝 𝐨 i | 𝐫 𝐞 𝐩 𝐞 𝐚 𝐭 i 𝐮 𝐧 𝐭 𝐢 𝐥 b$

Pętla $𝐫 𝐞 𝐩 𝐞 𝐚 𝐭 i 𝐮 𝐧 𝐭 𝐢 𝐥 b$ 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ę:

$i : : = 𝐟 𝐨 𝐫 x : = e_{1} 𝐭 𝐨 e_{2} 𝐝 𝐨 i$

Wykonanie takiej pętli polega na:

Wyliczeniu wartości $n$ wyrażenia $e_{1}$ .
Przypisaniu wartości $n$ na zmienną $x$ .
Wyliczeniu wartości $m$ wyrażenia $e_{2}$ .
Jeśli $x > m$ , to pętla kończy się.
W przeciwnym razie:
- Wykonujemy instrukcję $i$ .
- Zwiększamy zmienną $x$ o 1.
- Powracamy do punktu 3.

Zauważmy, że wyrażenie $e_{1}$ jest tu wyliczane tylko raz, ale $e_{2}$ 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 $n$ wyrażenia $e_{1}$ .
Przypisaniu wartości $n$ na zmienną $x$ .
Wyliczeniu wartości $m$ wyrażenia $e_{2}$ .
Jeśli $x > m$ , to pętla kończy się.
W przeciwnym razie:
- Wykonujemy instrukcję $i$ .
- Zwiększamy zmienną $x$ 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 $x$ 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 $y$ jest zwiększana łącznie o 2+4+6+8+10. Jeśli uznamy, że zmiany zmiennej $x$ wewnątrz pętli nie wpływają na liczbę iteracji, to pętla wykona się 10 razy, a zmienna $y$ 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ć: $i : : = 𝐟 𝐨 𝐫 (i_{1}; b; i_{2}) i_{3}$

Jej wykonanie polega na:

Wykonaniu instrukcji $i_{1}$ .
Wyliczeniu wartości wyrażenia $b$ .
Jeśli wyrażenie wylicza się do fałszu, to pętla kończy się.
W przeciwnym razie:
- Wykonujemy instrukcję $i_{3}$ .
- Wykonujemy instrukcję $i_{2}$ .
- Powracamy do punktu 2.

Rozwiązanie

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

Aktualna wersja na dzień 22:13, 11 wrz 2023

Semantyka bezpośrednia instrukcji. Konstrukcje iteracyjne.

Pętle while i repeat

Pętla for

Menu nawigacyjne

Działania na stronie

Opcje strony

Narzędzia osobiste

Nawigacja

Szukaj

Narzędzia

@@ Linia 38: / Linia 38: @@
 </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.
-{{rozwiazanie||roz1|
+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
-<div class="mw-collapsible mw-made=collapsible mw-collapsed">
+Zaczynamy jak zwykle od opisu dziedzin semantycznych. Nie przejmujemy
-<div class="mw-collapsible-content" style="display:none">
+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.
-<div class="mw-collapsible mw-made=collapsible mw-collapsed">
+Użyjemy elementarnych dziedzin z wykładu:
-'''Funkcje semantyczne:'''
+* 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">
-__HIDE__
+wartości wszystkich występujących w nim zmiennych.
+</div>
-<math>\begin{array} {lcl}
-\mathcal{E} & : & Exp \to Env \to S \to EV + \{err\}\\
-\mathcal{D} & : & Dec \to Env \to S \to Env\times S + \{(err,err)\}\\
-\mathcal{I} & : & Ins \to Env \to S \to S_{\bot} + \{err\}_{\bot}\\
-\end{array} </math>
 </div>
-'''R"ownania:'''<br>
-<math>\mathcal{E}[\![ n ]\!] = \lambda \varrho\in Env \cdot \lambda s\in S \cdot n</math><br>
+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:
-<math>\mathcal{E}[\![ x ]\!] = \lambda \varrho\in Env\cdot\lambda s\in S\cdot\\
+<center><math>State = Var \rightarrow Int</math></center>
-\hspace*{1.5cm}\ \mathrm{if}\  x\not\in
-dom(\varrho)\ \mathrm{then}\ err\\
-\hspace*{1.5cm}\ \mathrm{else}\ \mathrm{if}\ \varrho x\not\in Loc\ \mathrm{then}\ err\\
-\hspace*{1.5cm}\ \mathrm{else}\ \mathrm{if}\  s(\varrho x)
-\not\in\mathbb{N}\ \mathrm{then}\ err\\
-\hspace*{1.5cm}\ \mathrm{else}\  s(\varrho x)</math><br>
-<math>\mathcal{E}[\![ e_1\ {\tt +}\ e_2 ]\!] = \lambda\varrho\in Env\cdot\lambda s\in S\cdot\\
+Zdefiniujmy następnie niezbędne funkcje semantyczne.
-\hspace*{1.5cm}\ \mathrm{if}\ \mathcal{E}[\![ e_1 ]\!]\varrho s\not\in\mathbb{N}\ \mathrm{or}\
+* Dla wyrażeń mamy
-\mathcal{E}[\![ e_2 ]\!]\varrho s\not\in\mathbb{N}\ \mathrm{then}\ err\\
-\hspace*{1.5cm}\ \mathrm{else}\  \mathcal{E}[\![ e_1 ]\!]\varrho s +\mathcal{E}[\![ e_2 ]\!]\varrho s</math><br>
-<math>\mathcal{D}[\![ {\tt var}\ x\ {\tt = 0} ]\!] = \lambda\varrho\in Env\cdot\lambda s\in S\cdot\\
+<center><math>\mathcal{E} & : & \mathrm Exp \rightarrow \mathrm State \rightarrow \mathrm Int</math></center>
-\hspace*{1.5cm}\ \mathrm{if}\  s^{-1}(\{free\})=\emptyset\ \mathrm{then}\ (err,err)\\
-\hspace*{1.5cm}\ \mathrm{else}\ \mathrm{let}\ l = \mathrm{min}(s^{-1}(\{free\}))\\
-\hspace*{1.5cm}\mathrm{in}\ (\varrho[l/x],s[0/l])</math><br>
-<math>\mathcal{D}[\![ {\tt proc}\ x{\tt (}y{\tt )}\ {\tt \{}\ i\ {\tt \}} ]\!] =
+* Dla wyrażeń logicznych:
-\lambda\varrho\in Env\cdot\lambda s_0\in S\cdot\\
-\hspace*{1.5cm}\ \mathrm{if}\  x=y\ \mathrm{then}\ (err,err)\\
-\hspace*{1.5cm}\ \mathrm{else}\ \mathrm{let}\ F = \lambda f\in Proc\cdot\\
-\hspace*{1.5cm}\hspace*{0.5cm}\lambda l\in Loc\cdot\lambda s\in S\cdot\\
-\hspace*{1.5cm}\hspace*{1.5cm}\ \mathrm{if}\  s l\not\in\mathbb{N}\ \mathrm{then}\ err\\
-\hspace*{1.5cm}\hspace*{1.5cm}\ \mathrm{else}\ \mathrm{if}\  s^{-1}(\{free\})=\emptyset\ \mathrm{then}\ err\\
-\hspace*{1.5cm}\hspace*{1.5cm}\ \mathrm{else}\ \mathrm{let}\ l'=\mathrm{min}(s^{-1}(\{free\}))\\
-\hspace*{1.5cm}\hspace*{1.5cm}\mathrm{in}\ \mathcal{I}[\![ i ]\!]\varrho[f/x][l'/y]s[s l / l']\\
-\hspace*{1.5cm}\mathrm{in}\ (\varrho[FIX(F)/x],s_0)</math><br>
-<math>\mathcal{D}[\![ d_1\ {\tt ;}\ d_2 ]\!] = \lambda\varrho\in Env\cdot\lambda s\in S\cdot\\
+<center><math>\mathcal{B} & : & \mathrm BExp \rightarrow \mathrm State \rightarrow \mathrm Bool</math></center>
-\hspace*{1.5cm}\mathrm{let}\ (\varrho',s') = \mathcal{D}[\![ d_1 ]\!]\\
-\hspace*{1.5cm}\mathrm{in}\ \ \mathrm{if}\ \varrho'=err\ \mathrm{then}\ (err,err)\\
-\hspace*{1.5cm}\ \mathrm{else}\  \mathcal{D}[\![ d_2 ]\!]\varrho' s'</math><br>
-<math>\mathcal{I}[\![ x\ {\tt :=}\ e ]\!] = \lambda\varrho\in Env\cdot\lambda s\in S\cdot\\
+* Dla instrukcji:
-\hspace*{1.5cm}\ \mathrm{if}\  x\not\in dom(\varrho)\ \mathrm{then}\ err\\
-\hspace*{1.5cm}\ \mathrm{else}\ \mathrm{if}\  \varrho x\not\in Loc\ \mathrm{then}\ err\\
-\hspace*{1.5cm}\ \mathrm{else}\ \mathrm{if}\  s(\varrho x)\not\in\mathbb{N}\ \mathrm{then}\ err\\
-\hspace*{1.5cm}\ \mathrm{else}\ \mathrm{if}\  \mathcal{E}[\![ e ]\!]\varrho s\not\in\mathbb{N}\ \mathrm{then}\ err\\
-\hspace*{1.5cm}\ \mathrm{else}\  s[\mathcal{E}[\![ e ]\!]\varrho s/ \varrho x]</math><br>
-<math>\mathcal{I}[\![ i_1\ {\tt ;}\ i_2 ]\!] = \lambda\varrho\in Env\cdot\lambda s\in S\cdot\\
+<center><math>\mathcal{I} & : & \mathrm Stmt \rightarrow \mathrm State \rightarrow \mathrm State</math></center>
-\hspace*{1.5cm}\ \mathrm{if}\  \mathcal{I}[\![ i_1 ]\!]\varrho s = err\ \mathrm{then}\ err\\
-\hspace*{1.5cm}\ \mathrm{else}\  \mathcal{I}[\![ i_2 ]\!]\varrho(\mathcal{I}[\![ i_1 ]\!]\varrho s)</math><br>
-<math>\mathcal{I}[\![ {\tt skip} ]\!] = \lambda\varrho\in Env\cdot\lambda s\in S\cdot s</math><br>
+* Oraz oczywistą funkcję dla stałych całkowitych:
-<math>\mathcal{I}[\![ {\tt begin}\ d\ {\tt in}\ i\ {\tt end} ]\!] = \lambda\varrho\in
+<center><math>\mathcal{Z} & : & \mathrm Num \rightarrow \mathcal{Z}</math></center>
-Env\cdot\lambda s\in S\cdot\\
-\hspace*{1.5cm}\mathrm{let}\ (\varrho',s') = \mathcal{D}[\![ d ]\!]\\
-\hspace*{1.5cm}\mathrm{in}\ \mathrm{if}\  \varrho'=err\ \mathrm{then}\ err\\
-\hspace*{1.5cm}\ \mathrm{else}\  \mathcal{I}[\![ i ]\!]\varrho' s'</math><br>
-<math>\mathcal{I}[\![ {\tt if}\ e\ {\tt = 0\ then\ }i{\tt\ fi} ]\!] = \lambda\varrho\in
+Funkcji {Z} nie definiujemy, przyjmując jak zwykle, że jej wynikiem
-Env\cdot\lambda s\in S\cdot\\
+jest wartość stałej liczbowej.
-\hspace*{1.5cm}\ \mathrm{if}\  \mathcal{E}[\![ e ]\!]\varrho s\not\in\mathbb{N}\ \mathrm{then}\ err\\
-\hspace*{1.5cm}\ \mathrm{else}\ \mathrm{if}\  \mathcal{E}[\![ e ]\!]\varrho s = 0\ \mathrm{then}\ \mathcal{I}[\![ i ]\!]\varrho s\\
-\hspace*{1.5cm}\ \mathrm{else}\  s</math><br>
-<math>\mathcal{I}[\![ {\tt while}\ e\ {\tt \ne 0\ do}\ i\ {\tt done} ]\!] =
+Rozpocznijmy od funkcji semantycznej dla wyrażeń. Musimy zdefiniować
-\lambda\varrho\in Env\cdot\lambda s_0\in S\cdot\\
+znaczenie (wartość) wyrażenia <math>e</math> w pewnym stanie <math>s</math>. Ową wartość
-\hspace*{1.5cm}\mathrm{let}\ F = \lambda f\in S\to S_{\bot}+\{err\}_{\bot}\cdot\\
+zapisujemy jako <math>\mathcal{E} [\![e]\!] s</math>, czyli wartość funkcji E zastosowanej do
-\hspace*{1.5cm}\hspace*{0.5cm} \lambda s\in S\cdot\\
+dwóch argumentów: wyrażenia <math>e</math> oraz stanu <math>s</math>. Przypomnijmy, że taka
-\hspace*{1.5cm}\hspace*{1.5cm}\mathrm{let}\ n=\mathcal{E}[\![ e ]\!]\varrho s\\
+"dziwna" notacja z nawiasami służy oddzieleniu składni od elementów
-\hspace*{1.5cm}\hspace*{1.5cm}\mathrm{in}\ \mathrm{if}\  n\not\in\mathbb{N}\ \mathrm{then}\ err\\
+z metajęzyka.
-\hspace*{1.5cm}\hspace*{1.5cm}\ \mathrm{else}\ \mathrm{if}\  n = 0\ \mathrm{then}\  s\\
-\hspace*{1.5cm}\hspace*{1.5cm}\ \mathrm{else}\  f s\\
-\hspace*{1.5cm}\mathrm{in} FIX(F) s_0</math><br>
-<math>\mathcal{I}[\![ {\tt call}\ x_1{\tt (}x_2{\tt )} ]\!] = \lambda \varrho\in
+Funkcje semantyczne definiujemy dla każdej postaci wyrażenia,
-Env\cdot\lambda s\in S\cdot\\
+odpowiadając na standardowe pytania:
-\hspace*{1.5cm}\ \mathrm{if}\  x_1\not\in dom(\varrho)\ \mathrm{then}\  err\\
+# Co jest wartością wyrażenia <math>x</math> w stanie <math>s</math>? Odpowiedź: wartość
-\hspace*{1.5cm}\ \mathrm{else}\ \mathrm{if}\  \varrho x_1\not\in Proc\ \mathrm{then}\  err\\
+zmiennej <math>x</math> w tym stanie, czyli wartość uzyskana przez zastosowanie
-\hspace*{1.5cm}\ \mathrm{else}\ \mathrm{if}\  x_2\not\in dom(\varrho)\ \mathrm{then}\ err\\
+funkcji <math>s</math> do identyfikatora <math>x</math>. Zapisujemy to następująco:
-\hspace*{1.5cm}\ \mathrm{else}\ \mathrm{if}\  \varrho x_2\not\in Loc\ \mathrm{then}\  err\\
-\hspace*{1.5cm}\ \mathrm{else}\ \mathrm{if}\  s(\varrho x_2)\not\in\mathbb{N}\ \mathrm{then}\ err\\
-\hspace*{1.5cm}\ \mathrm{else}\  \varrho x_1 (\varrho x_2)</math><br>
+<center><math>\mathcal{E} [\![x]\!] s = s (x)</math></center>
-</div>
+Często będziemy pomijać nawiasy przy aplikacji funkcji pisząc po
-</div>
+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|
@@ Linia 161: / Linia 130: @@
 # Jeśli <math>x > m</math>, to pętla kończy się.
 # W przeciwnym razie:
-#* Wykonujemy instrukcję <math> i </math>.
+#* Wykonujemy instrukcję <math>i</math>.
 #* Zwiększamy zmienną <math>x</math> o 1.
 #* Powracamy do punktu 3.
@@ Linia 167: / Linia 136: @@
 }}
-{{rozwiazanie||roz2|
 <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|
@@ Linia 189: / Linia 158: @@
 }}
-{{rozwiazanie||roz3|
 <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ę.
 }}
-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 := 1 '''to''' 10 '''do'''
-   x := x + 1;
-   y := y + x;
-wykonuje}} się pięć razy, a zmienna y jest zwiększana łącznie o 2+4+6+8+10. Jeśli uznamy, że zmiany zmiennej x wewnątrz pętli nie wpływają na liczbę iteracji, to pętla wykona się 10 razy, a zmienna y zostanie zwiększona o 2+3+4+5+6+7+8+9+10+11.
-{{cwiczenie|4|cw4|
-Zdefiniuj taką semantykę.
-}}
-{{rozwiazanie||roz4|
 <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|
@@ Linia 228: / Linia 196: @@
 # Jeśli wyrażenie wylicza się do fałszu, to pętla kończy się.
 # 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.
 }}
-{{rozwiazanie||roz5|
 <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>
-}}