SW wykład 1 - Slajd6

<<powrót do strony wykładu

Wstęp Literatura Programy Programy, sprzeczne oczekiwania WielkiCel Składnia Semantyka Pragmatyka Logika Metodyka Implementacja Formalna semantyka Przykład Przykład, c.d. Przykład, reguła dowodzenia Uzasadnianie poprawności Plan zajęć

Składnia (syntaktyka) określa poprawnie (syntaktycznie) zbudowane programy i napisy reprezentujące dobrze zbudowane frazy innych kategorii syntaktycznych języka.

Mówimy tu często o składni konkretnej, określającej po prostu zbiór dobrze zbudowanych napisów (dla typowych języków programowania: ciągów znaków), które są programami, czy frazami poszczególnych kategorii składniowych języka mogących w programach występować. Formalna prezentacja tak rozumianej składni, określającej z dokładnością do każdego przecinka i kropki, co jest, a co nie jest programem w danym języku, jest już dziś standardem. Standardem są też metody formalnej analizy składniowej. Warto jednak pamiętać, że przecież jeszcze stosunkowo niedawno (lata 70.) był to intensywnie uprawiany dział matematycznych podstaw informatyki, a wykorzystywane dziś rutynowo pojęcia i narzędzia mają u podstaw lata pracy teoretyków.

Analiza składniowa programów prowadzona jest oczywiście dla zapisanych w składni konkretnej programów. Jej oczekiwanym wynikiem (po usunięciu wskazanych błędów składniowych) jest składnia abstrakcyjna, rozumiana jako jednoznaczny opis kolejnych konstrukcji językowych wykorzystywanych do budowania danego programu i jego poszczególnych fraz. Na tę "drzewiastą" strukturę składni abstrakcyjnej programu nakłada się dodatkowe wymagania narzucające pewne kontekstowe warunki, które programy danego języka muszą spełniać. Ich sprawdzanie jest przedmiotem szeroko rozumianej analizy statycznej programu, której typową częścią jest na przykład analiza typów, ale która może też obejmować proste własności związane z poprawnością programu.