Semantyka i weryfikacja programów/Ćwiczenia 8: Różnice pomiędzy wersjami
Nie podano opisu zmian |
Nie podano opisu zmian |
||
| Linia 13: | Linia 13: | ||
}} | }} | ||
{{rozwiazanie|| | {{rozwiazanie||roz1| | ||
<div class="mw-collapsible mw-made=collapsible mw-collapsed"> | <div class="mw-collapsible mw-made=collapsible mw-collapsed"> | ||
| Linia 27: | Linia 27: | ||
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. | 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. | ||
}} | }} | ||
{{rozwiazanie||roz2| | |||
<div class="mw-collapsible mw-made=collapsible mw-collapsed"> | |||
<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''' | ||
| Linia 36: | Linia 45: | ||
{{cwiczenie|3|cw3| | {{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: | ||
}} | |||
{{rozwiazanie||roz3| | |||
<div class="mw-collapsible mw-made=collapsible mw-collapsed"> | |||
<div class="mw-collapsible-content" style="display:none"> | |||
Jeszcze nie ma | |||
</div> | |||
</div> | |||
}} | }} | ||
| Linia 43: | Linia 61: | ||
{{cwiczenie|4|cw4| | {{cwiczenie|4|cw4| | ||
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: | ||
}} | |||
{{rozwiazanie||roz4| | |||
<div class="mw-collapsible mw-made=collapsible mw-collapsed"> | |||
<div class="mw-collapsible-content" style="display:none"> | |||
Jeszcze nie ma | |||
</div> | |||
</div> | |||
}} | }} | ||
Wersja z 22:38, 5 sie 2006
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
