Dostosuj preferencje dotyczące zgody

Używamy plików cookie, aby pomóc użytkownikom w sprawnej nawigacji i wykonywaniu określonych funkcji. Szczegółowe informacje na temat wszystkich plików cookie odpowiadających poszczególnym kategoriom zgody znajdują się poniżej.

Pliki cookie sklasyfikowane jako „niezbędne” są przechowywane w przeglądarce użytkownika, ponieważ są niezbędne do włączenia podstawowych funkcji witryny.... 

Zawsze aktywne

Niezbędne pliki cookie mają kluczowe znaczenie dla podstawowych funkcji witryny i witryna nie będzie działać w zamierzony sposób bez nich. Te pliki cookie nie przechowują żadnych danych umożliwiających identyfikację osoby.

Brak plików cookie do wyświetlenia.

Funkcjonalne pliki cookie pomagają wykonywać pewne funkcje, takie jak udostępnianie zawartości witryny na platformach mediów społecznościowych, zbieranie informacji zwrotnych i inne funkcje stron trzecich.

Brak plików cookie do wyświetlenia.

Analityczne pliki cookie służą do zrozumienia, w jaki sposób użytkownicy wchodzą w interakcję z witryną. Te pliki cookie pomagają dostarczać informacje o metrykach liczby odwiedzających, współczynniku odrzuceń, źródle ruchu itp.

Brak plików cookie do wyświetlenia.

Wydajnościowe pliki cookie służą do zrozumienia i analizy kluczowych wskaźników wydajności witryny, co pomaga zapewnić lepsze wrażenia użytkownika dla odwiedzających.

Brak plików cookie do wyświetlenia.

Reklamowe pliki cookie służą do dostarczania użytkownikom spersonalizowanych reklam w oparciu o strony, które odwiedzili wcześniej, oraz do analizowania skuteczności kampanii reklamowej.

Brak plików cookie do wyświetlenia.

Strona głównaAktualnościAndrzej Blikle o pozyskiwaniu matematycznych gwarancji poprawności programów

Andrzej Blikle o pozyskiwaniu matematycznych gwarancji poprawności programów

-

KATEGORIE:

Członek Honorowy PTI prof. Andrzej Blikle przedstawi w Instytucie Podstaw Informatyki PAN wykład pt. „Odwróćmy tradycyjną kolej rzeczy (eksperyment z inżynierii języków programowania)”. Seminarium odbędzie się 10 grudnia, o godz. 13 na parterze Instytutu, w sali nr 5 (ul. ul. Jana Kazimierza 5, Warszawa).

Profesor Andrzej Blikle tak wyjaśnia przedmiot swojego zainteresowania:

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 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 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 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 seminarium 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ć 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ę moją książkę (w stanie surowym) „Denotacyjna inżynieria języków programowania”, którą mogę udostępnić w wersji cyfrowej. Z jej wydaniem na razie się nie spieszę, by zebrać jak najwięcej opinii czytelników. I oczywiście, za wszelkie takie opinie będę niezmiernie wdzięczny.

Najważniejsze informacje

Informacje z oddziałów