Semantyka i weryfikacja programów/Ćwiczenia 7

From Studia Informatyczne

Semantyka bezpośrednia instrukcji. Konstrukcje iteracyjne.

Pętle while i repeat

Ćwiczenie 1

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

n \, ::= \ldots \,\, -1\,\,|\,\, 0 \,\,|\,\, 1 \,\,|\,\, \ldots

x \, ::= \,\, \ldots \, (identyfikatory) \, \ldots

e \,  ::=  \,\,           n   \,\,|\,\,         x   \,\,|\,\,         e_1\,\, + \,\, e_2

b \,  ::=  \,\,           e_1\, = \, e_2   \,\,|\,\,         \mathbf{not}\,\, b    \,\,|\,\,         b_1\,\, \mathbf{or}\,\, b_2

i \, ::= \,\,          x\, :=\, e     \,\,|\,\,          i_1; i_2   \,\,|\,\,          \mathbf{if}\,\, b \,\,\mathbf{then}\,\, i_1 \,\,\mathbf{else}\,\, i_2 \,\,|\,\,          \mathbf{skip} \,\,|\,\,          \mathbf{while}\,\, b \,\,\mathbf{do}\,\, i \,\,|\,\,          \mathbf{repeat}\,\, i \,\mathbf{until}\,\, b

Pętla \mathbf{repeat}\,\, i \,\,\mathbf{until}\,\, 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 \, ::= \mathbf{for}\, x\, :=\, e_1\, \mathbf{to}\, e_2\, \mathbf{do}\, i

Wykonanie takiej pętli polega na:

  1. Wyliczeniu wartości n wyrażenia e_1.
  2. Przypisaniu wartości n na zmienną x.
  3. Wyliczeniu wartości m wyrażenia e_2.
  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 e_1 jest tu wyliczane tylko raz, ale e_2 oblicza się przy każdym obrocie pętli.

Rozwiązanie

Jeszcze nie ma.

Ć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 e_1.
  2. Przypisaniu wartości n na zmienną x.
  3. Wyliczeniu wartości m wyrażenia e_2.
  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

Jeszcze nie ma.

Ć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

Jeszcze nie ma.

Ćwiczenie 5

W języku C pętla for ma następującą postać: i \, ::= \mathbf{for}\, (i_1;\, b;\, i_2)\, i_3

Jej wykonanie polega na:

  1. Wykonaniu instrukcji i_1.
  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ę i_3.
    • Wykonujemy instrukcję i_2.
    • Powracamy do punktu 2.

Rozwiązanie

Jeszcze nie ma.