SW wykład 1 - Literatura
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ęć
Formalne metody opisu semantyki i dowodzenia poprawności programów to dziś już klasyczna dziedzina informatyki, która dorobiła się niezwykle bogatej literatury, od podręczników i monografii po całą gamę artykułów naukowych publikowanych przez lata w czasopismach i materiałach konferencji naukowych.
Tu wybraliśmy kilka pozycji, dość losowo, ale zapewniając dobrą ilustrację prezentowanego na tych zajęciach materiału. Ważnym kryterium był gust autorów tych materiałów, a także dostępność polskich wersji tych pozycji. Są to często pozycje sprzed wielu już lat, które jednak nie straciły swojej aktualności --- choć niekiedy oczywiście należy je czytać przez pryzmat późniejszych badań i doświadczeń praktycznych.
Książka polskich autorów, Dembińskiego i Małuszyńskiego, to zgrabny przegląd metod definiowania semantyki języków programowania, niekiedy dziś już dość ezoterycznych, ale zawsze interesujących, dobrze opisanych i wartych choć powierzchownego poznania.
Książka Gordona to cykl kilkunastu bardzo przystępnie prowadzonych wykładów dotyczących podstawowych technik denotacyjnego opisu semantyki języków programowania, prezentujących kolejne konstrukcje językowe, przy okazji przemycające idee dotyczące dobrego projektowania konstrukcji językowych i całych języków programowania. Polskie wydanie tej książki jest wzbogacone o bardo dobry dodatek autorstwa prof. Blikle, przedstawiający pominięte przez Gordona problemy matematycznych podstaw semantyki denotacyjnej.
Książka małżeństwa Nielsonów to nieco bardziej współczesna wersja tego samego wykładu: prezentacji metod opisu semantyki języków programowania i ich wykorzystania do definiowania poprawności programów i metod jej dowodzenia.
Książka Griesa, o ile nam wiadomo, niedostępna w języku polskim, to świetny przegląd metod dowodzenia poprawności różnych klas programów.
I w końcu książka Dijkstry, w wyśmienitym tłumaczeniu prof. Turskiego, to klasyka literatury podstaw informatyki autorstwa klasyka metody systematycznego, niezwykle pięknego programowania, a raczej konstruowania programów. Wykorzystuje się tu kilkanaście z pozoru prostych, ale niezwykle pięknie i wnikliwie pokazanych przykładów, które ilustrują propagowaną przez autora metodę systematycznego wyprowadzenia programów poprawnych względem żądanej specyfikacji problemu.
