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
Nie podano opisu zmian
Mengel (dyskusja | edycje)
1013 edycji
Linia 18: Linia 18:
         n  \,\,|\,\,
         n  \,\,|\,\,
         x  \,\,|\,\,
         x  \,\,|\,\,
         e_1 + e_2  \,\,|\,\,
         e_1\,\, + \,\, e_2
</math>
</math>


<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
</math>
</math>


Linia 32: Linia 32:
         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 \,\,|\,\,
         \mathbf{skip} \,\,|\,\,
         \mathbf{skip} \,\,|\,\,
         \mathbf{while}\, b \,\mathbf{do}\, i \,\,|\,\,
         \mathbf{while}\,\, b \,\,\mathbf{do}\,\, i \,\,|\,\,
         \mathbf{repeat}\, i \,\mathbf{until}\, b \,\,|\,\,
         \mathbf{repeat}\,\, i \,\mathbf{until}\,\, b
</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''.
}}
}}


Wersja z 13:56, 5 sie 2006

Semantyka bezpośrednia instrukcji. Konstrukcje iteracyjne.

Zadanie 1

Ć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}}}

Zadanie 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

Zadanie 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

Zadanie 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

Zadanie 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

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