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 7: / Linia 7: @@
 <math>
-n \, ::= \,\, 0 \,\,|\,\, 1 \,\,|\,\, \ldots
+n \, ::= \ldots \,\, -1\,\,|\,\, 0 \,\,|\,\, 1 \,\,|\,\, \ldots
 </math>
@@ 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
+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">
-Jeszcze nie ma.
+wartości wszystkich występujących w nim zmiennych.
+</div>
 </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|
@@ Linia 65: / 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 71: / 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 93: / 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||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 131: / 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