SW wykład 4 - Slajd12: Różnice pomiędzy wersjami
Nie podano opisu zmian |
Nie podano opisu zmian |
||
| (Nie pokazano 2 wersji utworzonych przez 2 użytkowników) | |||
| Linia 1: | Linia 1: | ||
{{Semantyka i weryfikacja programów/Wykład 4}} | |||
[[Grafika:sw0411.png|center|frame]] | [[Grafika:sw0411.png|center|frame]] | ||
Klauzula określająca znaczenie pętli jest więc równaniem | |||
stałopunktowym (w dziedzinie semantycznej dla instrukcji, czyli w | |||
dziedzinie funkcji częściowych ze stanów w stany). | |||
Równania stałopunktowe sprawiają jednak przynajmniej dwa podstawowe | |||
problemy. | |||
Po pierwsze, nie każdy operator ma jakikolwiek punkt stały. | |||
Przykładowy operator na slajdzie, który dowolnej funkcji częściowej | |||
przyporządkowuje funkcję z pewnością od niej różną (bo dla dowolnego | |||
stanu, jeśli wartość funkcji będącej argumentem jest nieokreślona, to | |||
wartość wyniku operatora na tym stanie jest określona, a w przeciwnym | |||
przypadku wartość ta też jest określona, ale różna od wartości | |||
argumentu na tym stanie), oczywiście nie ma żadnego punktu | |||
stałego. Musimy więc jakoś zapewnić, że z takimi operatorami nie | |||
będziemy mieli do czynienia i precyzyjnie opisać własność rozważanych | |||
operatorów, która zapewni istnienie dla nich (przynajmniej jednego) | |||
punktu stałego. | |||
Po drugie zaś, istnieją operatory, które mają wiele punktów | |||
stałych. Najprostszy przykład to operator identycznościowy, dla | |||
którego każda funkcja ze stanów w stany jest punktem stałym. Inny | |||
przykład na slajdzie to operator, którego jednym z punktów stałych | |||
jest funkcja zawsze nieokreślona, a drugim funkcja, która modyfikuje | |||
dowolny stan przez przypisanie wskazanej zmiennej zera. Który z | |||
punktów stałych danego operatora powinniśmy jakoś wskazać jako | |||
definiowaną równaniem stałopunktowym wartość? Poszukamy jednolitej | |||
metody wskazania "właściwego" punktu stałego dla praktycznie nas | |||
interesującej (na potrzeby semantyki denotacyjnej) klasy operatorów. | |||
Aktualna wersja na dzień 12:57, 29 wrz 2006
Semantyka denotacyjna Dziedziny składniowe i semantyczne Funkcje semantyczne Kompozycjonalność Tiny. Semantyka denotacyjna Tiny. Semantyka denotacyjna, c.d. Pojęcia pomocnicze Pojęcia pomocnicze, c.d. |Tiny. Semantyka denotacyjna, c.d. Tiny. Semantyka denotacyjna, c.d. Problem z while Konstrukcje stałopunktowe Konstrukcje stałopunktowe, c.d. Konstrukcje stałopunktowe, c.d. Przykład Przykład, c.d. Dowód Dowód Zgodność semantyki denotacyjnej
Klauzula określająca znaczenie pętli jest więc równaniem stałopunktowym (w dziedzinie semantycznej dla instrukcji, czyli w dziedzinie funkcji częściowych ze stanów w stany).
Równania stałopunktowe sprawiają jednak przynajmniej dwa podstawowe problemy.
Po pierwsze, nie każdy operator ma jakikolwiek punkt stały. Przykładowy operator na slajdzie, który dowolnej funkcji częściowej przyporządkowuje funkcję z pewnością od niej różną (bo dla dowolnego stanu, jeśli wartość funkcji będącej argumentem jest nieokreślona, to wartość wyniku operatora na tym stanie jest określona, a w przeciwnym przypadku wartość ta też jest określona, ale różna od wartości argumentu na tym stanie), oczywiście nie ma żadnego punktu stałego. Musimy więc jakoś zapewnić, że z takimi operatorami nie będziemy mieli do czynienia i precyzyjnie opisać własność rozważanych operatorów, która zapewni istnienie dla nich (przynajmniej jednego) punktu stałego.
Po drugie zaś, istnieją operatory, które mają wiele punktów stałych. Najprostszy przykład to operator identycznościowy, dla którego każda funkcja ze stanów w stany jest punktem stałym. Inny przykład na slajdzie to operator, którego jednym z punktów stałych jest funkcja zawsze nieokreślona, a drugim funkcja, która modyfikuje dowolny stan przez przypisanie wskazanej zmiennej zera. Który z punktów stałych danego operatora powinniśmy jakoś wskazać jako definiowaną równaniem stałopunktowym wartość? Poszukamy jednolitej metody wskazania "właściwego" punktu stałego dla praktycznie nas interesującej (na potrzeby semantyki denotacyjnej) klasy operatorów.
