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

Z Studia Informatyczne
Przejdź do nawigacjiPrzejdź do wyszukiwania
Linia 169: Linia 169:
 
{{cwiczenie| 4|cw4|
 
{{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 :<nowiki>=</nowiki> 1 '''to''' 10 '''do'''  
   x ::<nowiki>=</nowiki> x + 1;
+
   x:<nowiki>=</nowiki> x + 1;
   y ::<nowiki>=</nowiki> y + x;
+
   y:<nowiki>=</nowiki> 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.  
 
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ę.
 
Zdefiniuj taką semantykę.

Wersja z 14:04, 10 sie 2006

Semantyka bezpośrednia instrukcji. Konstrukcje iteracyjne.

Pętle while i repeat

Ćwiczenie 1

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

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

Powyższy język to tak naprawdę Tiny z wykładu rozszerzony o jedną konstrukcję: pętlę repeat. Spróbuj wykonać to ćwiczenie nie sięgając do notatek z wykładu. Jeśli napotkasz trudności, odkrywaj kolejne elementy poniższego opisu.

Kategorie składniowe występujące w tym języku to:

  • wyrażenia Exp
  • wyrażenia logiczne BExp
  • instrukcje Stmt
  • oraz, jak zwykle, stałe liczbowe Num

Zaczynamy jak zwykle od opisu dziedzin semantycznych. Nie przejmujemy się na razie szczegółami związanymi z konstrukcjami stałopunktowymi oraz umieszczeniem pineski we właściwych dziedzinach. Zakładamy, że wszystkie zmienne są zainicjowane na zero.

Użyjemy elementarnych dziedzin z wykładu:

  • Int = ..., -1, 0, 1, ... zawierający denotacje stałych

liczbowych

  • Bool = {tt}, {ff} zawierający wartości logiczne
  • Var zawierający wszystkie dozwolone identyfikatory

Przypomnijmy, że wartość wyrażenia arytmetycznego zależy od

Wartości te są "pamiętane" w stanie, który jest funkcją ze zbioru Var w zbiór Int. Zbiór wszystkich stanów to:

Zdefiniujmy następnie niezbędne funkcje semantyczne.

  • Dla wyrażeń mamy
Parser nie mógł rozpoznać (błąd składni): {\displaystyle \mathcal{E} & : & \mathrm Exp \rightarrow \mathrm State \rightarrow \mathrm Int }
  • Dla wyrażeń logicznych:
Parser nie mógł rozpoznać (błąd składni): {\displaystyle \mathcal{B} & : & \mathrm BExp \rightarrow \mathrm State \rightarrow \mathrm Bool }
  • Dla instrukcji:
Parser nie mógł rozpoznać (błąd składni): {\displaystyle \mathcal{I} & : & \mathrm Stmt \rightarrow \mathrm State \rightarrow \mathrm State }
  • Oraz oczywistą funkcję dla stałych całkowitych:
Parser nie mógł rozpoznać (błąd składni): {\displaystyle \mathcal{Z} & : & \mathrm Num \rightarrow \mathcal{Z} }

Funkcji {Z} nie definiujemy, przyjmując jak zwykle, że jej wynikiem jest wartość stałej liczbowej.

Rozpocznijmy od funkcji semantycznej dla wyrażeń. Musimy zdefioniować znaczenie (wartość) wyrażenia w pewnym stanie . Ową wartość zapisujemy jako , czyli wartość funkcji E zastosowanej do dwóch argumentów: wyrażenia oraz stanu . Przypomnijmy, że taka "dziwna" notacja z nawiasami służy oddzieleniu składni od elementów z metajęzyka.

Funkcje semantyczne definiujemy dla każdej postaci wyrażenia, odpowiadając na standardowe pytania:

  1. Co jest wartością wyrażenia w stanie , Odpowiedź: wartość

zmiennej w tym stanie, czyli wartość uzyskana przez zastosowanie funkcji do identyfikatora . Zapisujemy to następująco

Często będziemy powijać nawiasy przy aplikacji funkcji pisząc po prostu zamiast . To samo można zapisać stosując notację "lambda":

Parser nie mógł rozpoznać (nieznana funkcja „\l”): {\displaystyle \mathcal{E} [\![x]\!] = \l s \in \mathrm State.s (x)}

Pętla for

Ćwiczenie 2

Rozszerzmy język z poprzedniego zadania o instrukcję:

Wykonanie takiej pętli polega na:

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

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

Rozwiązanie

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

Rozwiązanie

{{{3}}}

Ćwiczenie 4

O pętli for można jednak myśleć jeszcze inaczej. Można wymagać, aby wszelkie zmiany wartości zmiennej sterującej 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

{{{3}}}

Ćwiczenie 5

W języku C pętla for ma następującą postać:

Jej wykonanie polega na:

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

Rozwiązanie

{{{3}}}