SW wykład 2 - Slajd16: Różnice pomiędzy wersjami

Z Studia Informatyczne
Przejdź do nawigacjiPrzejdź do wyszukiwania
Arturas (dyskusja | edycje)
Nie podano opisu zmian
Tarlecki (dyskusja | edycje)
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

<<powrót do strony wykładu

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.