Semantyka i weryfikacja programów/Ćwiczenia 7

Z Studia Informatyczne
Przejdź do nawigacjiPrzejdź do wyszukiwania

Semantyka bezpośrednia instrukcji. Konstrukcje iteracyjne.

Zadanie 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.

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.

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.

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ę.

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.