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

Z Studia Informatyczne
Przejdź do nawigacjiPrzejdź do wyszukiwania
Mengel (dyskusja | edycje)
Nie podano opisu zmian
 
Dorota (dyskusja | edycje)
Nie podano opisu zmian
 
(Nie pokazano 3 wersji utworzonych przez 2 użytkowników)
Linia 1: Linia 1:
{{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
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.

Aktualna wersja na dzień 10:33, 27 wrz 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 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.