SW wykład 1 - Slajd12

<<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ęć

Właściwie niemal wszystko, o czym mowa była powyżej, odnosi się do semantyki programów bez względu na sposób jej określenia. Można by pomyśleć, że wobec tego wystarczy opis tej semantyki w języku naturalnym, zapewniający wystarczające jej zrozumienie przez czytelnika-programistę. Tak jednak nie jest. Rozumienie opisów w języku naturalnym bywa bardzo powierzchowne, a z pewnością niezwykle związane z kontekstem, indywidualną wiedzą i doświadczeniami. Aby zapewnić niezbędną pełność i jednoznaczność rozumienia konstrukcji językowych przez wszystkich użytkowników języka (nie tylko przecież programistów, ale też na przykład jego implementatorów), niezbędny jest sformalizowany, obiektywny, niezależny od czytelnika, ścisły opis matematyczny. Tylko taki opis jest w stanie zapewnić w pełni precyzyjny, jednoznaczny i dokładny opis konstrukcji językowych, pełną niezależność od jakiejkolwiek konkretnej implementacji i sposobu realizacji języka (w tym od intuicji implementacyjnych z taką realizacją związanych). Warto też dodać, że taki formalny matematyczny opis stwarza świetne podstawy do szybkiej, prototypowej implementacji języka. A przede wszystkim, tylko taki opis może dać niezbędne podstawy dla opracowania i wiarygodnego uzasadnienia metod wnioskowania o budowanych w tym języku programach.