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

Z Studia Informatyczne
Przejdź do nawigacjiPrzejdź do wyszukiwania
 
(Nie pokazano 3 wersji utworzonych przez 3 użytkowników)
Linia 38: Linia 38:
 
</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ą
+
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ę '''repeat'''. Spróbuj wykonać to ćwiczenie nie
 
sięgając do notatek z wykładu. Jeśli napotkasz trudności, odkrywaj
 
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
 
Zaczynamy jak zwykle od opisu dziedzin semantycznych. Nie przejmujemy
 
się na razie szczegółami związanymi z konstrukcjami stałopunktowymi
 
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.  
 
wszystkie zmienne są zainicjowane na zero.  
  
Linia 95: Linia 95:
 
jest wartość stałej liczbowej.  
 
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ść
 
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
 
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,
 
Funkcje semantyczne definiujemy dla każdej postaci wyrażenia,
 
odpowiadając na standardowe pytania:
 
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
 
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>
 
<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ę
 
prostu <math>s\,x</math> zamiast <math>s(x)</math>. To samo można zapisać stosując notację
 
"lambda":  
 
"lambda":  
  
 
<center><math>\mathcal{E} [\![x]\!] = \l s \in \mathrm State.s (x)</math></center>
 
<center><math>\mathcal{E} [\![x]\!] = \l s \in \mathrm State.s (x)</math></center>
 
+
-->
 
=== Pętla '''for''' ===
 
=== Pętla '''for''' ===
 
{{cwiczenie|2|cw2|
 
{{cwiczenie|2|cw2|
Linia 136: Linia 136:
 
}}
 
}}
  
{{rozwiazanie||roz2|
+
 
 
<div class="mw-collapsible mw-made=collapsible mw-collapsed">
 
<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">
 
<div class="mw-collapsible-content" style="display:none">
 
Jeszcze nie ma.
 
Jeszcze nie ma.
 
</div>
 
</div>
 
</div>
 
</div>
}}
+
 
  
 
{{cwiczenie|3|cw3|
 
{{cwiczenie|3|cw3|
Linia 158: Linia 158:
 
}}
 
}}
  
{{rozwiazanie||roz3|
+
 
 
<div class="mw-collapsible mw-made=collapsible mw-collapsed">
 
<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">
 
<div class="mw-collapsible-content" style="display:none">
 
Jeszcze nie ma.
 
Jeszcze nie ma.
 
</div>
 
</div>
 
</div>
 
</div>
}}
+
 
  
 
{{cwiczenie| 4|cw4|
 
{{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 ::<nowiki>=</nowiki> x + 1;
+
   x:<nowiki>=</nowiki> x + 1;
   y ::<nowiki>=</nowiki> 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ę.
 
Zdefiniuj taką semantykę.
 
}}
 
}}
  
{{rozwiazanie||roz4|
+
 
 
<div class="mw-collapsible mw-made=collapsible mw-collapsed">
 
<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">
 
<div class="mw-collapsible-content" style="display:none">
 
Jeszcze nie ma.
 
Jeszcze nie ma.
 
</div>
 
</div>
 
</div>
 
</div>
}}
+
 
  
 
{{cwiczenie|5|cw5|
 
{{cwiczenie|5|cw5|
Linia 201: Linia 201:
 
}}
 
}}
  
{{rozwiazanie||roz5|
+
 
 
<div class="mw-collapsible mw-made=collapsible mw-collapsed">
 
<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">
 
<div class="mw-collapsible-content" style="display:none">
 
Jeszcze nie ma.
 
Jeszcze nie ma.
 
</div>
 
</div>
 
</div>
 
</div>
}}
 

Aktualna wersja na dzień 13:24, 1 cze 2020

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:

  1. Wyliczeniu wartości wyrażenia .
  2. Przypisaniu wartości na zmienną .
  3. Wyliczeniu wartości wyrażenia .
  4. Jeśli , to pętla kończy się.
  5. 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:

  1. Wyliczeniu wartości wyrażenia .
  2. Przypisaniu wartości na zmienną .
  3. Wyliczeniu wartości wyrażenia .
  4. Jeśli , to pętla kończy się.
  5. 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:

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


Rozwiązanie