SW wykład 2 - Slajd10: Różnice pomiędzy wersjami
Nie podano opisu zmian |
Nie podano opisu zmian |
||
| (Nie pokazano 2 wersji utworzonych przez jednego użytkownika) | |||
| Linia 1: | Linia 1: | ||
{{Szablon:Semantyka i weryfikacja programów/Wykład 2}} | {{Szablon:Semantyka i weryfikacja programów/Wykład 2}} | ||
[[Grafika:sw0209.png|frame|center|]] | [[Grafika:sw0209.png|frame|center|]] | ||
Powyższy przykład definicji indukcyjnej określa zbiór zmiennych | |||
wolnych każdego wyrażenia arytmetycznego (wobec braku wiązania | |||
zmiennych czy deklarowania zmiennych lokalnych w wyrażeniach, na | |||
przykład przez kwantyfikatory, jest to po prostu zbiór zmiennych, | |||
które w tym wyrażeniu występują). | |||
Na przykład, łatwo teraz pokazać, że zbiór zmiennych wolnych każdego | |||
wyrażenia arytmetycznego jest skończony. Własność ta zachodzi bowiem | |||
wprost z definicji dla wyrażeń, będących stałymi numerycznymi lub | |||
zmiennymi, oraz jeśli zachodzi ona dla dwóch wyrażeń arytmetycznych, | |||
to zachodzi też dla wyrażeń będących ich sumą, iloczynem lub różnicą. | |||
Zatem, na mocy zasady indukcji strukturalnej, własność ta zachodzi | |||
dla wszystkich wyrażeń arytmetycznych. | |||
Aktualna wersja na dzień 10:35, 27 wrz 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
Powyższy przykład definicji indukcyjnej określa zbiór zmiennych wolnych każdego wyrażenia arytmetycznego (wobec braku wiązania zmiennych czy deklarowania zmiennych lokalnych w wyrażeniach, na przykład przez kwantyfikatory, jest to po prostu zbiór zmiennych, które w tym wyrażeniu występują).
Na przykład, łatwo teraz pokazać, że zbiór zmiennych wolnych każdego wyrażenia arytmetycznego jest skończony. Własność ta zachodzi bowiem wprost z definicji dla wyrażeń, będących stałymi numerycznymi lub zmiennymi, oraz jeśli zachodzi ona dla dwóch wyrażeń arytmetycznych, to zachodzi też dla wyrażeń będących ich sumą, iloczynem lub różnicą. Zatem, na mocy zasady indukcji strukturalnej, własność ta zachodzi dla wszystkich wyrażeń arytmetycznych.
