Propozycja wykładu seminaryjnego

Utworzono: wtorek, 30 kwiecień 2019 11:20

Poprawiono: środa, 01 maj 2019 15:49

Odsłony: 4352

Eksperyment z semantyką denotacyjną (odwracając tradycyjną kolej rzeczy)  Pobierz prezentację

Wykład w wymiarze minimalnym (60 min) obejmuje strony od 1 do 15 prezentacji. Na pełen wykład trzeba przeznaczyć co najmniej 120 min plus odpowiednią ilość czasu na dyskusję.

Zapowiedź:

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?

Moim zdaniem 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 — przynajmniej na skalę praktyczną — 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 badania 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. Jednocześnie, od lat 1970. dla większości matematyków było raczej oczywiste, że matematyczne semantyki powinny być kompozycyjne, co oznacza, że znaczenie całości jest funkcją znaczeń jej części. W literaturze takie semantyki nazwano denotacyjnymi.

Niestety w żadnym z obu obszarów — semantyki i poprawność — 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 moje):

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 mojej ocenie 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 do tej pory 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 seminarium przedstawiam własną propozycję podjęcia problemów budowania semantyki denotacyjnej oraz poprawności programów, a także wyjaśniam, dlaczego wymaga ona „odwrócenia tradycyjnej kolei rzeczy”. Choć moja propozycja jest oparta na dość specyficznej matematyce, postaram się przedstawić ją w sposób strawny dla osób, które tej matematyki mogą nie znać. A tym, którzy chcieliby do niej sięgnąć, proponuję książkę (patrz: Książka).

Istnieją również wersje angielskie zarówno książki (The book), jak i wykładu (A proposal of a seminar). .

Za wszelkie opinie o metodzie, książce i wykładzie będę niezmiernie wdzięczny. Można do mnie pisać na adres Ten adres pocztowy jest chroniony przed spamowaniem. Aby go zobaczyć, konieczne jest włączenie w przeglądarce obsługi JavaScript..

Zaproszenie do projektu

Utworzono: wtorek, 30 kwiecień 2019 11:26

Poprawiono: wtorek, 30 kwiecień 2019 12:10

Odsłony: 4893

Gdyby znalazła się grupa osób zainteresowanych rozwijaniem projektu, mogę jej zaoferować pomoc merytoryczną w tym obszarze, a także — być może — jakąś pomoc organizacyjną. Mogę się podjąć promotorstwa prac magisterskich i doktorskich oraz przeprowadzenia kursów na różnych poziomach matematycznej szczegółowości w zależności od tego, czy słuchaczami byliby teoretycy zamierzający dalej rozwijać denotacyjny model Lingua, czy też praktycy zainteresowani budowaniem narzędzi wspomagających pracę projektanta języka lub programisty (patrz: Co jest jeszcze do zrobienia)

W dalszej perspektywie można by też myśleć o powołaniu startupu, który oferowałby wdrożenia narzędzi środowiska projektanta języków oraz programistycznego w technologii Lingua oraz opiekę na tymi narzędziami. Analogicznie jak w przypadkach implementacji Linuxa, same narzędzia pozostawałyby bezpłatne, natomiast komercjalizacji podlegałoby wsparcie w ich stosowaniu i aktualizowaniu. Firma mogłaby też oferować produkty IT zbudowane zgodnie z metodologią oferowaną przez środowisko programistyczne dla Lingua.

Osoby zainteresowane porozmawianiem o szczegółach projektu bardzo proszę o kontakt ze mną na adres Ten adres pocztowy jest chroniony przed spamowaniem. Aby go zobaczyć, konieczne jest włączenie w przeglądarce obsługi JavaScript. 

Dwa nowe kierunki badawcze

Utworzono: wtorek, 30 kwiecień 2019 11:17

Poprawiono: wtorek, 30 kwiecień 2019 11:17

Odsłony: 4296

Niezależnie od wskazanej powyżej problematyki, są jeszcze dwa ważne kierunki badawcze, którymi z pewności warto się zająć.

Pierwszy dotyczy rozbudowania naszego modelu denotacyjnego o mechanizmy współbieżności. W pełni denotacyjne modele dla współbieżności nie są dziś chyba znane, choć istnieją próby łączenia w takim przypadku semantyki denotacyjnej z operacyjną.

Drugi problem nie był chyba w ogóle eksploatowany, a dotyczy budowy na wpół formalnych języków dla opisu adresowanych do przyszłych użytkowników programów. Jak na razie wszystkie podejścia do problemu poprawności programów — włączywszy w to nasz projekt — ograniczają się do zgodności kodu programu z jego specyfikacją formalną. Nie wyczerpuje to jednak problemu wiarygodności produktów przemysłu IT, gdyż wiele błędów w produktach zawdzięcza swoje istnienie złej komunikacji pomiędzy budowniczym aplikacji, a jej przyszłymi użytkownikami. W tym przypadku trzeba by zapewne myśleć o wielu językach specyfikacji tworzonych pod poszczególne obszary zastosowań.