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

Z Studia Informatyczne
Przejdź do nawigacjiPrzejdź do wyszukiwania
WizualnieWikikod
Mengel (dyskusja | edycje)
1013 edycji
Nie podano opisu zmian
 
 
(Nie pokazano 8 wersji utworzonych przez 3 użytkowników)
Linia 1: Linia 1:
== Obliczanie funkcji semantycznych. Punkty stałe. ==
== Obliczanie funkcji semantycznych. Punkty stałe. ==


=== Zadanie 1 ===  
=== Obliczanie prostych funkcji semantycznych ===
Rozpatrzmy język z pierwszego zadania poprzednich ćwiczeń. Przypuśćmy, że w stanie początkowym wszystkie zmienne mają wartość zero. Pokaż jak wygląda obliczenie semantyki programu:


Rozpatrzmy język z pierwszego zadania poprzednich ćwiczeń. Przypuśćmy, że w stanie początkowym wszystkie zmienne mają wartość zero. Dla programu:
   x := 5;
   x := 5;
   '''if''' x + 1 + 8 '''then'''
   '''if''' x + 1 + 8 '''then'''
Linia 9: Linia 9:
   '''else'''
   '''else'''
     x := x + 10
     x := x + 10
{{cwiczenie|1|cw1|
Pokaż jak wygląda obliczenie semantyki programu:
}}


=== Zadanie 2 ===
<div class="mw-collapsible mw-made=collapsible mw-collapsed">
Równania semantyczne dla konstrukcji iteracyjnych, które zapisaliśmy w poprzednich ćwiczeniach nie są do końca poprawne. Występuje w nich rekurencja, która nie musi się kończyć, więc w pewnych sytuacjach (programów zapętlających się) równania te nie definiują poprawnie żadnej wartości. Zmienimy to teraz posługując się konstrukcją punktu stałego.  
<span class="mw-collapsible-toogle mw-collapsible-toogle-default style="font-variant:small-caps">Rozwiązanie</span>
<div class="mw-collapsible-content" style="display:none">
Jeszcze nie ma
</div>
</div>
 
=== Stosowanie konstrukcji stałopunktowych ===
 
{{cwiczenie|2|cw2|
Równania semantyczne dla konstrukcji iteracyjnych, które zapisaliśmy w poprzednich ćwiczeniach, nie są do końca poprawne. Występuje w nich rekurencja, która nie musi się kończyć, więc w pewnych sytuacjach (programów zapętlających się) równania te nie definiują poprawnie żadnej wartości. Zmienimy to teraz posługując się konstrukcją punktu stałego.  
}}
 
 
<div class="mw-collapsible mw-made=collapsible mw-collapsed">
<span class="mw-collapsible-toogle mw-collapsible-toogle-default style="font-variant:small-caps">Rozwiązanie</span>
<div class="mw-collapsible-content" style="display:none">
Jeszcze nie ma
</div>
</div>


Tutaj definicje stałopunktowe dla kolejnych konstrukcji stałopunktowych po uprzednim przykładzie dla '''while'''
Tutaj definicje stałopunktowe dla kolejnych konstrukcji stałopunktowych po uprzednim przykładzie dla '''while'''


=== Zadanie 3 ===
=== Obliczanie punktów stałych ===
Dany jest program
'''while''' 0 = 0 '''do''' '''skip'''
 
{{cwiczenie|3|cw3|
Korzystając z konstrukcji punktu stałego z dowodu twierdzenia o punkcie stałym, oblicz semantykę programu:
Korzystając z konstrukcji punktu stałego z dowodu twierdzenia o punkcie stałym, oblicz semantykę programu:
}}


'''while''' 0 = 0 '''do''' '''skip'''


=== Zadanie 4 ===
<div class="mw-collapsible mw-made=collapsible mw-collapsed">
Korzystając z konstrukcji punktu stałego z dowodu twierdzenia o punkcie stałym, oblicz semantykę programu:
<span class="mw-collapsible-toogle mw-collapsible-toogle-default style="font-variant:small-caps">Rozwiązanie</span>
<div class="mw-collapsible-content" style="display:none">
Jeszcze nie ma
</div>
</div>
 


Dany jest program
  x := 1;
  x := 1;
  '''while''' '''not''' x = 3 '''do''' y := y + x;
  '''while''' '''not''' x = 3 '''do''' y := y + x;
{{cwiczenie|4|cw4|
Korzystając z konstrukcji punktu stałego z dowodu twierdzenia o punkcie stałym, oblicz semantykę programu:
}}
<div class="mw-collapsible mw-made=collapsible mw-collapsed">
<span class="mw-collapsible-toogle mw-collapsible-toogle-default style="font-variant:small-caps">Rozwiązanie</span>
<div class="mw-collapsible-content" style="display:none">
Jeszcze nie ma
</div>
</div>

Aktualna wersja na dzień 13:26, 1 cze 2020

Obliczanie funkcji semantycznych. Punkty stałe.

Obliczanie prostych funkcji semantycznych

Rozpatrzmy język z pierwszego zadania poprzednich ćwiczeń. Przypuśćmy, że w stanie początkowym wszystkie zmienne mają wartość zero. Dla programu: 

 x := 5;
 if x + 1 + 8 then
   x := x + 4
 else
   x := x + 10

Ćwiczenie 1

Pokaż jak wygląda obliczenie semantyki programu:

Rozwiązanie

Stosowanie konstrukcji stałopunktowych

Ćwiczenie 2

Równania semantyczne dla konstrukcji iteracyjnych, które zapisaliśmy w poprzednich ćwiczeniach, nie są do końca poprawne. Występuje w nich rekurencja, która nie musi się kończyć, więc w pewnych sytuacjach (programów zapętlających się) równania te nie definiują poprawnie żadnej wartości. Zmienimy to teraz posługując się konstrukcją punktu stałego.


Rozwiązanie

Tutaj definicje stałopunktowe dla kolejnych konstrukcji stałopunktowych po uprzednim przykładzie dla while

Obliczanie punktów stałych

Dany jest program 

while 0 = 0 do skip

Ćwiczenie 3

Korzystając z konstrukcji punktu stałego z dowodu twierdzenia o punkcie stałym, oblicz semantykę programu:


Rozwiązanie


Dany jest program 

x := 1;
while not x = 3 do y := y + x;

Ćwiczenie 4

Korzystając z konstrukcji punktu stałego z dowodu twierdzenia o punkcie stałym, oblicz semantykę programu:

Rozwiązanie

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