SW wykład 1 - Programy
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ęć
Na tych zajęciach, mówiąc o programach będziemy mieli na myśli sformalizowane napisy w języku programowania. Choć na ogół zajmować się będziemy programami stosunkowo niewielkimi (tylko takie łatwo przedstawić w ramach wykładu czy ćwiczeń), zajmując się głównie programami "in-the-small" (jak choćby te zapisane powyżej), to trzeba pamiętać, że omawiana problematyka odnosi się w równym stopniu, a może nawet bardziej, do dużych systemów oprogramowania, mierzonych przynajmniej w setkach modułów czy setkach tysięcy linii kodu. Nie starczy nam tu jednak czasu i miejsca na omówienie ważnych problemów metod opisu semantyki, analizy i systematycznego konstruowania złożonych systemów oprogramowania.
Mówiąc o programach (bez względu na ich wielkość i złożoność), należy podkreślać ich cechy najważniejsze dla ich prawidłowego wykorzystywania. Niewątpliwie musimy zapewniać, by programy były niezawodne, łatwe do wykorzystania przez użytkownika, dobrze udokumentowane, odporne na błędy itp. Przede wszystkim jednak musimy zadbać o ich poprawność --- żaden, najlepszy nawet program, nie spełni swojej roli, gdy nie będzie wykonywał oczekiwanych od niego zadań. Oczywiście, nacisk tu musi być położony zarówno na wykonywanie tych zadań (program musi działać!), jak i na ich właściwe wykonywanie (program musi być poprawny!). Dwa podstawowe punkty widzenia, które opisują pojęcie programu, to bowiem z jednej strony ścisły opis obliczeń, które ma wykonywać "bezmyślny" komputer, a z drugiej strony ścisły opis algorytmu, który ma być realizowany. W tej drugiej, nie mniej ważnej roli, program musi być zrozumiały dla człowieka. Dużą rolę dla zapewnienia tej cechy odgrywa oczywiście sam sposób jego zapisu (por. binarny fragment programu w zapisie szesnastkowym i fragment programu w Pascalu powyżej). Ale najważniejsze jest, by wykorzystywana notacja (język programowania) była dobrze i ściśle opisana, tak by wszelkie wątpliwości można było wyjaśnić na gruncie precyzyjnych i dostatecznie abstrakcyjnych pojęć formalnych, nie odwołujących się bezpośrednio do konkretnych obliczeń programu, przy konkretnej jego implementacji w środowisku komputerowym.
