SW wykład 1 - Programy, sprzeczne oczekiwania
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ęć
Jak słuchacze tego wykładu z pewnością wiedzą, do zapisu programów służą języki programowania. Dobry język programowania powinien mieć wiele cech, które często są z pozoru ze sobą w sprzeczności. Z jednej strony, język programowania powinien być łatwy w użyciu: przez zaoferowanie programiście wielu mocnych konstrukcji programistycznych powinien on uczynić pisanie programów stosunkowo łatwym, umożliwiając programiście zakodowanie algorytmu bez zbędnych łamańców i sztuczek formalnych. Z drugiej strony, język powinien zapewniać efektywną realizację zapisanych w nim programów i łatwość kodowania programów efektywnie działających. Jednak złożoność konstrukcji językowych, ważna dla wygody i zwięzłości zapisywania programów, łatwo wpada w sprzeczność z efektywnością ich automatycznej realizacji.
Z punktu widzenia tych zajęć, język powinien mieć dobrze opracowane podstawy formalne, tak by zapisane w nim programy miały precyzyjnie określoną semantykę i mogły być formalnie analizowane. Ten wymóg opracowania na przykład ścisłej (i zrozumiałej) semantyki języka wydaje się być w sprzeczności zarówno z oczekiwaną złożonością dostępnych konstrukcji językowych, jak i z dostępnością konstrukcji, umożliwiających zapisywania efektywnych programów, często wykorzystujących programistyczne "sztuczki" (jak traktowanie liczb jako wartości logicznych, itp).
Warto zapewne spróbować umieścić Państwa ulubione języki programowania w przestrzeni wyznaczonej przez trójkąt tych i podobnych sprzeczności.
W naszym odczuciu, są to jednak sprzeczności tylko pozorne. Względna prostota, przejrzystość i dostępność precyzyjnego opisu semantycznego i formalnych narzędzi analizy dla udostępnianych konstrukcji językowych sprzyja bowiem na dłuższą metę nie tylko łatwości konstruowania dobrych programów, ale i ich efektywnej realizacji (choćby przez budowanie dobrych i niezawodnych, bo dobrze wspartych precyzyjną analizą formalną, optymalizujących kompilatorów języka).
