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
 sięgając do notatek z wykładu. Jeśli napotkasz trudności, odkrywaj
@@ Linia 54: / 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.
@@ Linia 73: / Linia 73: @@
 Var w zbiór Int. Zbiór wszystkich stanów to:
-<center><math>State = Var \rightarrow Int </math></center>
+<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>
+<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>
+<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>
+<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>
+<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 zdefioniować
+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
@@ Linia 104: / Linia 104: @@
 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ść
+# 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
+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 powijać nawiasy przy aplikacji funkcji pisząc po
+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 130: / 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 136: / 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 158: / 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:
+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'''
+  '''for''' x :<nowiki>=</nowiki> 1 '''to''' 10 '''do'''
-    x := x + 1;
+    x:<nowiki>=</nowiki> x + 1;
-    y := y + x;
+    y:<nowiki>=</nowiki> 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.
+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ę.
 }}
-{{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 196: / 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