Oddział Mazowiecki Polskiego Towarzystwa Informatycznego zaprasza już teraz na pierwszy po Nowym Roku 2019 Klub Informatyka. Ponoworoczny KI będzie miał zaszczyt gościć prof. Andrzeja Jacka Bliklego (AJB) z prezentacją zatytułowaną Odwróćmy tradycyjną kolej rzeczy (eksperyment z inżynierii języków programowania). Klub odbędzie się we wtorek 8 stycznia 2019, w godz. 18-21, w gmachu Wydziału Matematyki i Nauk Informacyjnych Politechniki Warszawskiej (tu mapka) w sali 103. Sam wykład rozpocznie się o godz. 18:30.
Czy można sobie wyobrazić, by klient kupujący samochód podpisywał zrzeczenie się wszelkich praw do roszczeń (ang. disclosure), gdyby wady techniczne samochodu miały narazić go na szkody? Chyba nie. To dlaczego w przemyśle IT jest to powszechny standard? Zdaniem Andrzeja Blikle ten paradoks bierze się stąd, że podczas gdy każdy produkt techniczny powstaje na gruncie matematycznych obliczeń stanowiących swoisty „dowód jego poprawności”, to w informatyce takich dowodów przeprowadzać nie umiemy.
Problem pozyskiwania matematycznych gwarancji poprawności programów pojawił się po raz pierwszy w pracy Alana Turinga w roku 1949. Później przez kilka dekad podejmowano ten temat pod hasłem dowodzenia poprawności programów, a równolegle też próby definiowania takich semantyk języków programowania, które byłyby podstawą do prowadzenia dowodów poprawności. Niestety w żadnym z obu obszarów nie dopracowano się metod, które weszłyby na stałe do repertuaru narzędzi inżynierii oprogramowania. Wreszcie zaniechano tych badań, co autorzy monografii Deductive Software Verification z roku 2016 podsumowali stwierdzając (tłumaczenie AJB): Przez wiele lat pojęcie formalnej weryfikacji było niemalże synonimem weryfikacji funkcjonalnej. W ostatnich latach staje się coraz bardziej jasne, że pełna funkcjonalna weryfikacja programu jest dla prawie wszystkich zastosowań celem iluzorycznym.
W ocenie AJB niepowodzenie opisanych wyżej prób miało dwa źródła: Po pierwsze, dla większości istniejących języków programowania zapewne nie da się zbudować takiej semantyki, która mogłaby służyć do praktycznego dowodzenia poprawności programów. To oczywiście tylko opinia, ale fakt, że od 1949 roku tego nie udało się tego dokonać, o czymś jednak świadczy.
Po drugie, nawet gdyby taką semantykę zbudowano, to dla większości programów dowodów poprawności nie da się przeprowadzić z prostego powodu, że one poprawne nie są! Stąd też praktyczną wartość dowodzenia poprawności upatrywano w nadziei, że próba dowodzenia poprawności programu wskaże na zawarte w nim błędy.
W trakcie wykładu Andrzej Blikle przedstawi pewną nową propozycję podjęcia problemu poprawności programów, a także wyjaśni, dlaczego wymaga to „odwrócenia tradycyjnej kolei rzeczy”. Choć propozycja ta jest oparta na dość specyficznej matematyce, prezentujący postara się przedstawić ją w sposób przystępny dla osób, które tej matematyki mogą nie znać. Tym, którzy chcieliby do niej sięgnąć, AJB udostępnia swoją książkę (w stanie surowym) „Denotacyjna inżynieria języków programowania”, w wersji cyfrowej.
Wstęp na Klub jest wolny. Ze względów logistyczno-aprowizacyjnych Oddział Mazowiecki prosi o zgłoszenia (z podaniem liczby osób) pod adres omaz[at]pti.org.pl. Klub będzie filmowany. Wiąże się to z wyrażeniem przez uczestników Klubu zgody na wykorzystanie ich wizerunku w relacjach wideo, które można znaleźć w kanale PTI portalu Youtube, a także w portalu Oddziału Mazowieckiego PTI, w szczególności w informacjach noszących tag wideo.
Zobacz także
- wersja bieżąca książki: Andrzej Blikle, Denotacyjna inżynieria języków programowania
- prezentacja autorska wykładu związanego z tematyką książki
O prelegencie
Andrzej Jacek Blikle – matematyk, informatyk, biznesmen. Profesor zwyczajny w Instytucie Podstaw Informatyki PAN, członek Sekcji Informatyki w Europejskiej Akademii Nauk (Academia Europaea). Członek założyciel PTI, członek Prezydium Zarządu Głównego (1981-1987), prezes Zarządu Głównego (1987-1993), od roku 1993 członek honorowy. Honorowy prezes Centrum im. Adama Smitha, honorowy prezes stowarzyszenia Inicjatywa Firm Rodzinnych, członek Rady Języka Polskiego przy Prezydium PAN, Rady Strategicznej wydawnictwa Thinktank, Komitetu Obywatelskiego przy Prezydencie Lechu Wałęsie oraz ponad 20 innych organizacji. W latach 1970–1989 prowadził kursy akademickie z zakresu matematycznej teorii programowania na uniwersytetach w Warszawie, Waterloo (Kanada), Berkeley (USA), Linköping (Szwecja), Lyngby i Kopenhadze (Dania). Jego książka Automaty i Gramatyki; Wstęp do lingwistyki matematycznej, PWN, Warszawa 1971 była pierwszą w Polsce i drugą na świecie monografią z zakresu teorii języków formalnych. W latach 1990–2010 prowadził rodzinną firmę cukierniczą (zał. 1869), a od roku 1998 zaczął również nauczać zarządzania kompleksową jakością. Jego książka „Doktryna jakości” dostępna na www.moznainaczej.com.pl zajęła I miejsce w kategorii „Najlepszy poradnik ekonomiczny” w konkursie Economicus 2015 organizowanym przez „Dziennik Gazeta Prawna”, a także otrzymała nagrodę Kolegium Nauk o Przedsiębiorstwie Szkoły Głównej Handlowej w Warszawie „za najlepszą pracę z zakresu nauk o przedsiębiorstwie w latach 2014–2015”.