SW wykład 2 - Slajd9: 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:sw0208.png|frame|center|]] | [[Grafika:sw0208.png|frame|center|]] | ||
Sformułowana powyżej zasada indukcji strukturalnej dla wyrażeń | |||
arytmetycznych naszego języka to oczywiście tylko przykład. Może | |||
najłatwiej będzie go zrozumieć przedstawiając zwykłą indukcję dla | |||
liczb naturalnych jako indukcję strukturalną właśnie, gdzie liczby | |||
naturalne budowane są przez dwie konstrukcje: stałą zero i | |||
jednoargumentową konstrukcję następnika. | |||
Zachęcamy też Państwa do sformułowania zasad indukcji strukturalnej | |||
dla wyrażeń logicznych i dla instrukcji naszego języka TINY. | |||
Wersja z 11:02, 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
Sformułowana powyżej zasada indukcji strukturalnej dla wyrażeń arytmetycznych naszego języka to oczywiście tylko przykład. Może najłatwiej będzie go zrozumieć przedstawiając zwykłą indukcję dla liczb naturalnych jako indukcję strukturalną właśnie, gdzie liczby naturalne budowane są przez dwie konstrukcje: stałą zero i jednoargumentową konstrukcję następnika.
Zachęcamy też Państwa do sformułowania zasad indukcji strukturalnej dla wyrażeń logicznych i dla instrukcji naszego języka TINY.
