Semantyka i weryfikacja programów/Ćwiczenia 8: Różnice pomiędzy wersjami
Z Studia Informatyczne
Przejdź do nawigacjiPrzejdź do wyszukiwania
Nie podano opisu zmian |
Nie podano opisu zmian |
||
| Linia 1: | Linia 1: | ||
== Obliczanie funkcji semantycznych. Punkty stałe. == | == Obliczanie funkcji semantycznych. Punkty stałe. == | ||
=== | === Obliczanie prostych funkcji semantycznych === | ||
{{cwiczenie|1|cw1| | |||
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. Pokaż jak wygląda obliczenie semantyki programu: | ||
| Linia 9: | Linia 11: | ||
'''else''' | '''else''' | ||
x := x + 10 | x := x + 10 | ||
}} | |||
=== | === 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. | 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. | ||
}} | |||
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''' | ||
=== | === Obliczanie punktów stałych === | ||
{{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''' | '''while''' 0 = 0 '''do''' '''skip''' | ||
}} | |||
{{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: | ||
x := 1; | x := 1; | ||
'''while''' '''not''' x = 3 '''do''' y := y + x; | '''while''' '''not''' x = 3 '''do''' y := y + x; | ||
}} | |||
Wersja z 22:34, 5 sie 2006
Obliczanie funkcji semantycznych. Punkty stałe.
Obliczanie prostych funkcji semantycznych
Ćwiczenie 1
{{{3}}}
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.
Tutaj definicje stałopunktowe dla kolejnych konstrukcji stałopunktowych po uprzednim przykładzie dla while
Obliczanie punktów stałych
Ćwiczenie 3
{{{3}}}
Ćwiczenie 4
{{{3}}}
