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

@@ 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ą
-Powyższy język to tak naprawdę Tiny z wykładu rozszerzony o jedną
+konstrukcję: pętlę '''repeat'''. Spróbuj wykonać to ćwiczenie nie
-konstrukcję: pętlę {\bf 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.
@@ Linia 55: / Linia 54: @@
 Zaczynamy jak zwykle od opisu dziedzin semantycznych. Nie przejmujemy
 się na razie szczegółami związanymi z konstrukcjami stałopunktowymi
-oraz umieszczeniem pineski we właściwych dziedzinach. Zakładamy, że
+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 = \{\ldots, -1, 0, 1, \ldots\} zawierający denotacje stałych
+* Int <nowiki>=</nowiki> ..., -1, 0, 1, ... zawierający denotacje stałych
 liczbowych
-* Bool = \{\tt, \ff\} zawierający wartości logiczne
+* 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 $e$ zależy od
+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.
@@ Linia 71: / Linia 70: @@
 </div>
-Wartości te są ,,pamiętane'' w stanie, który jest funkcją ze zbioru
+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:
-\[ State = Var \ra Int \]
+<center><math>State = Var \rightarrow Int</math></center>
 Zdefiniujmy następnie niezbędne funkcje semantyczne.
 * Dla wyrażeń mamy
-\[\E & : & Exp \ra State \ra Int  \]
+<center><math>\mathcal{E} & : & \mathrm Exp \rightarrow \mathrm State \rightarrow \mathrm Int</math></center>
 * Dla wyrażeń logicznych:
-\[\B & : & BExp \ra State \ra Bool  \]
+<center><math>\mathcal{B} & : & \mathrm BExp \rightarrow \mathrm State \rightarrow \mathrm Bool</math></center>
 * Dla instrukcji:
-\[\I & : & Stmt \ra Stmt \ra Stmt  \]
+<center><math>\mathcal{I} & : & \mathrm Stmt \rightarrow \mathrm State \rightarrow \mathrm State</math></center>
 * Oraz oczywistą funkcję dla stałych całkowitych:
-\[\Z & : & Num \ra Z  \]
+<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|
@@ Linia 99: / 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 105: / 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 127: / 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 166: / 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>
-}}

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