Semantyka i weryfikacja programów/Ćwiczenia 7

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.