SW wykład 4 - Slajd8: Różnice pomiędzy wersjami
Nie podano opisu zmian |
Nie podano opisu zmian |
||
| Linia 1: | Linia 1: | ||
{{Semantyka i weryfikacja programów/Wykład 4}} | {{Semantyka i weryfikacja programów/Wykład 4}} | ||
[[Grafika:sw0407.png|center|frame]] | [[Grafika:sw0407.png|center|frame]] | ||
Kolejną operacją, którą wygodnie jest wykorzystywać w poniższych | |||
klauzulach semantycznych jest "podniesienie" funkcji: mając daną | |||
funkcję, "podnosimy" ją do funkcji wyższego rzędu, która operuje na | |||
funkcjach ze wspólnej dziedziny "indeksów", wykorzystując pierwotnie | |||
daną funkcję dla zdefiniowania wyniku dla każdego "indeksu" osobno. | |||
Wersja z 10:32, 2 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
Kolejną operacją, którą wygodnie jest wykorzystywać w poniższych klauzulach semantycznych jest "podniesienie" funkcji: mając daną funkcję, "podnosimy" ją do funkcji wyższego rzędu, która operuje na funkcjach ze wspólnej dziedziny "indeksów", wykorzystując pierwotnie daną funkcję dla zdefiniowania wyniku dla każdego "indeksu" osobno.
