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

Z Studia Informatyczne
Przejdź do nawigacjiPrzejdź do wyszukiwania
← poprzednia edycjanastępna edycja →
WizualnieWikikod
Mengel (dyskusja | edycje)
1013 edycji
Mengel (dyskusja | edycje)
1013 edycji
Linia 1: Linia 1:
== Semantyka bezpośrednia instrukcji. Konstrukcje iteracyjne. ==
== Semantyka bezpośrednia instrukcji. Konstrukcje iteracyjne. ==
=== Zadanie 1 ===
=== Pętle '''while''' i '''repeat''' ===


{{cwiczenie|1|cw1|
{{cwiczenie|1|cw1|
Linia 23: Linia 23:
<math>
<math>
b \,  ::=  \,\,   
b \,  ::=  \,\,   
         e_1\,\, = \,\, e_2  \,\,|\,\,
         e_1\, = \, e_2  \,\,|\,\,
         \mathbf{not}\,\, b    \,\,|\,\,
         \mathbf{not}\,\, b    \,\,|\,\,
         b_1\,\, \mathbf{or}\,\, b_2
         b_1\,\, \mathbf{or}\,\, b_2
Linia 30: Linia 30:
<math>
<math>
i \, ::= \,\,
i \, ::= \,\,
         x := e    \,\,|\,\,
         x\, :=\, e    \,\,|\,\,
         i_1; i_2  \,\,|\,\,
         i_1; i_2  \,\,|\,\,
         \mathbf{if}\,\, b \,\,\mathbf{then}\,\, i_1 \,\,\mathbf{else}\,\, i_2 \,\,|\,\,
         \mathbf{if}\,\, b \,\,\mathbf{then}\,\, i_1 \,\,\mathbf{else}\,\, i_2 \,\,|\,\,
Linia 51: Linia 51:
}}
}}


=== Zadanie 2 ===
=== Pętla '''for''' ===
{{cwiczenie|2|cw2|
Rozszerzmy język z poprzedniego zadania o instrukcję:
Rozszerzmy język z poprzedniego zadania o instrukcję:


Linia 68: Linia 69:
#* Powracamy do punktu 3.
#* Powracamy do punktu 3.
Zauważmy, że wyrażenie <math>e_1</math> jest tu wyliczane tylko raz, ale <math>e_2</math> oblicza się przy każdym obrocie pętli.
Zauważmy, że wyrażenie <math>e_1</math> jest tu wyliczane tylko raz, ale <math>e_2</math> oblicza się przy każdym obrocie pętli.
}}


{{rozwiazanie|2|roz2|
<div class="mw-collapsible mw-made=collapsible mw-collapsed">
<div class="mw-collapsible mw-made=collapsible mw-collapsed">
'''Rozwiązanie'''  
   
<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>
}}


=== Zadanie 3 ===
{{cwiczenie|3|cw3|
Zmieńmy semantykę instrukcji for z poprzedniego zadania tak, aby  
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:
oba wyrażenia obliczały się tylko raz. Tym razem wyliczenie pętli polega na:
Linia 87: Linia 91:
#* Zwiększamy zmienną <math>x</math> o 1.
#* Zwiększamy zmienną <math>x</math> o 1.
#* Powracamy do punktu 4.
#* Powracamy do punktu 4.
}}


{{rozwiazanie|3|roz3|
<div class="mw-collapsible mw-made=collapsible mw-collapsed">
<div class="mw-collapsible mw-made=collapsible mw-collapsed">
'''Rozwiązanie'''  
   
<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>
}}


=== Zadanie 4 ===
{{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 := 1 '''to''' 10 '''do'''  
Linia 101: Linia 108:
   y := y + x;
   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ę.  
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ę.  
}}


{{rozwiazanie|4|roz4|
<div class="mw-collapsible mw-made=collapsible mw-collapsed">
<div class="mw-collapsible mw-made=collapsible mw-collapsed">
'''Rozwiązanie'''  
   
<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>
}}


=== Zadanie 5 ===
{{cwiczenie|5|cw5|
W języku C pętla '''for''' ma następującą postać:
W języku C pętla '''for''' ma następującą postać:
<math>
<math>
Linia 123: Linia 133:
#* Wykonujemy instrukcję <math> i_2 </math>.
#* Wykonujemy instrukcję <math> i_2 </math>.
#* Powracamy do punktu 2.
#* Powracamy do punktu 2.
}}


{{rozwiazanie|5|roz5|
<div class="mw-collapsible mw-made=collapsible mw-collapsed">
<div class="mw-collapsible mw-made=collapsible mw-collapsed">
'''Rozwiązanie'''  
   
<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>
}}

Wersja z 14:01, 5 sie 2006

Semantyka bezpośrednia instrukcji. Konstrukcje iteracyjne.

Pętle while i repeat

Ćwiczenie 1

Zdefiniuj semantykę denotacyjną następującego języka:

n::=0|1|…

x::=…(identyfikatory)…

e::=n|x|e1+e2

b::=e1=e2|𝐧𝐨𝐭b|b1𝐨𝐫b2

i::=x:=e|i1;i2|𝐢𝐟b𝐭𝐡𝐞𝐧i1𝐞𝐥𝐬𝐞i2|𝐬𝐤𝐢𝐩|𝐰𝐡𝐢𝐥𝐞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.

Rozwiązanie

{{{3}}}

Pętla for

Ćwiczenie 2

Rozszerzmy język z poprzedniego zadania o instrukcję:

i::=𝐟𝐨𝐫x:=e1𝐭𝐨e2𝐝𝐨i

Wykonanie takiej pętli polega na:

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

Zauważmy, że wyrażenie e1 jest tu wyliczane tylko raz, ale e2 oblicza się przy każdym obrocie pętli.

Rozwiązanie 2

{{{3}}}

Ć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 n wyrażenia e1.
  2. Przypisaniu wartości n na zmienną x.
  3. Wyliczeniu wartości m wyrażenia e2.
  4. Jeśli x>m, to pętla kończy się.
  5. W przeciwnym razie:
    • Wykonujemy instrukcję i.
    • Zwiększamy zmienną x o 1.
    • Powracamy do punktu 4.

Rozwiązanie 3

{{{3}}}

Ćwiczenie 4

{{{3}}}

Rozwiązanie 4

{{{3}}}

Ćwiczenie 5

W języku C pętla for ma następującą postać: i::=𝐟𝐨𝐫(i1;b;i2)i3

Jej wykonanie polega na:

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

Rozwiązanie 5

{{{3}}}
Źródło: „https://wazniak.mimuw.edu.pl/index.php?title=Semantyka_i_weryfikacja_programów/Ćwiczenia_7&oldid=9630”