SW wykład 2 - Slajd16: Różnice pomiędzy wersjami
Nie podano opisu zmian |
Nie podano opisu zmian |
||
Linia 1: | Linia 1: | ||
{{Szablon:Semantyka i weryfikacja programów/Wykład 2}} | {{Szablon:Semantyka i weryfikacja programów/Wykład 2}} | ||
[[Grafika:sw0215.png|frame|center|]] | [[Grafika:sw0215.png|frame|center|]] | ||
Zanim jednak przejdziemy do opisu różnych metod definiowania semantyki | |||
instrukcji, kilka prostych faktów o wyrażeniach. Przede wszystkim | |||
zwróćmy jednak uwagę,że ścisłe sformułowanie tych faktów i ich | |||
precyzyjny dowód możliwe są dzięki ścisłej i precyzyjnej definicji | |||
semantyki wyrażeń powyżej. Bez tej definicji, waga i dokładny sens | |||
poniższych stwierdzeń byłyby niewielkie. | |||
Na początek, prosty fakt, że wartość wyrażenia (arytmetycznego: | |||
zachęcamy Państwa do sformułowania podobnego faktu i jego dowodu dla | |||
wyrażeń logicznych) nie zależy od wartościowania tych zmiennych, które | |||
nie są jego zmiennymi wolnymi, czyli że wartości wyrażenia w dwóch | |||
stanach, które jego zmiennym wolnym przypisują te same wartości | |||
liczbowe, są zawsze takie same. |
Wersja z 11:05, 22 sie 2006
Składnia Składnia konkretna Składnia abstrakcyjna Przyjmowane założenia Przykład wiodący Kategorie składniowe Kategorie składniowe, c.d. Uwagi Indukcja strukturalna Definicje indukcyjne Kategorie semantyczne Wartościowanie zmiennych Semantyka wyrażeń Semantyka wyrażeń logicznych Semantyka instrukcji Prosty fakt Dowód Przezroczystość odwołań Semantyka operacyjna Obliczenia Semantyka operacyjna Tiny Własności Własności, c.d. Warianty definicji

Zanim jednak przejdziemy do opisu różnych metod definiowania semantyki instrukcji, kilka prostych faktów o wyrażeniach. Przede wszystkim zwróćmy jednak uwagę,że ścisłe sformułowanie tych faktów i ich precyzyjny dowód możliwe są dzięki ścisłej i precyzyjnej definicji semantyki wyrażeń powyżej. Bez tej definicji, waga i dokładny sens poniższych stwierdzeń byłyby niewielkie.
Na początek, prosty fakt, że wartość wyrażenia (arytmetycznego: zachęcamy Państwa do sformułowania podobnego faktu i jego dowodu dla wyrażeń logicznych) nie zależy od wartościowania tych zmiennych, które nie są jego zmiennymi wolnymi, czyli że wartości wyrażenia w dwóch stanach, które jego zmiennym wolnym przypisują te same wartości liczbowe, są zawsze takie same.