SW wykład 2 - Slajd8: Różnice pomiędzy wersjami
Nie podano opisu zmian |
mNie 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:sw0207.png|frame|center|]] | [[Grafika:sw0207.png|frame|center|]] | ||
Zanim przejdziemy do definiowania semantyki języka TINY, jeszcze | Zanim przejdziemy do definiowania semantyki języka TINY, jeszcze | ||
komentarz o notacji wykorzystywanej do opisu składni -- na przykładzie | komentarz o notacji wykorzystywanej do opisu składni -- na przykładzie |
Wersja z 11:09, 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 przejdziemy do definiowania semantyki języka TINY, jeszcze komentarz o notacji wykorzystywanej do opisu składni -- na przykładzie składni wyrażeń arytmetycznych, ale oczywiście komentarz odnosi się także do pozostałych kategorii składniowych.
Podana wyżej definicja składni wyrażeń arytmetycznych formalnie może być zastąpiona w oczywisty sposób szeregiem produkcji gramatyki bezkontekstowej (po jednej dla każdego z przypadków składniowych tej kategorii, oddzielanych od siebie symbolem "|"). Każdy z tych przypadków (każda z tych produkcji) identyfikuje konstrukcję językową, budującą wyrażenia arytmetyczne z ich bezpośrednich składowych, które są albo frazami innych kategorii składniowych (tu: stałe liczbowe, zmienne) albo też wyrażeniami arytmetycznymi. Notacja ta oznacza też, że każde wyrażenie arytmetyczne jest zbudowane przez stosowanie tych konstrukcji skończenie wiele razy. Jak wspominaliśmy wcześniej, zakładamy także, że zawsze możemy jednoznacznie zidentyfikować kolejne konstrukcje użyte do budowy danego wyrażenia.
Zwróćmy też uwagę, że powyższa definicja wprowadza także standardową meta-zmienną, która (być może z dodatkowymi indeksami, primami, akcentami, itp) zawsze w tych materiałach przebiegać będzie dowolne wyrażenia arytmetyczne, zbudowane zgodnie z podaną tu składnią.
Założenie o skończonej generowalności wyrażeń przez konstrukcje językowe implikuje też dopuszczalność indukcji strukturalnej dla definiowania i dowodzenia własności wyrażeń arytmetycznych.