Skąd ten projekt

Utworzono: wtorek, 30 kwiecień 2019 05:40

Poprawiono: poniedziałek, 31 styczeń 2022 18:08

Odsłony: 22579

W każdej inżynierii, poza inżynierią oprogramowania, projektowanie nowego produktu rozpoczyna się od stworzenia opisu tego produktu w specyficznym dla danej inżynierii języku, który posługuje się z jednej strony wyspecjalizowanym aparatem pojęciowym, a z drugiej — aparatem matematycznym. Do tego dochodzi najczęściej rysunek techniczny. W tych trzech językach — branżowym, matematycznym i graficznym — powstaje opis przyszłego produktu uzupełniony o komentarze pisane w języku potocznym. Matematyczna część tego opisu, zwana zwykle „obliczeniami”, stanowi gwarancję, że wytworzony na jej podstawie produkt będzie miał oczekiwane przez jego twórców właściwości.

W inżynierii oprogramowania sytuacja jest inna. Projekt przyszłego produktu jest najczęściej opisany w języku zbliżonym do potocznego, co prawda wzbogaconym o terminologię techniczną, jednak nie zapewniającym matematycznej gwarancji poprawności, czyli zgodności z oczekiwaniami użytkownika. Ten stan rzeczy powoduje, że użytkownik nabywający jakąkolwiek aplikację musi zaakceptować tzw. „wyłączenie odpowiedzialności” (ang. disclaimer) ze strony producenta aplikacji. A oto typowy przykład takiego wyłączenia (nazwa firmy została zastąpiona słowem „Firma”):

O ile nie zaznaczono inaczej w „Warunkach dodatkowych”, Usługi i Oprogramowanie są udostępniane w stanie, w jakim się znajdują („AS-IS”). W maksymalnym zakresie dozwolonym przez prawo, Firma wyłącza wszelkie gwarancje wyraźne lub domniemane, w tym domniemane gwarancje nienaruszania praw, przydatności handlowej i przydatności do określonego celu. Firma nie przyjmuje żadnych zobowiązań dotyczących treści zawartej w Usługach.

To wyłączenie pochodzi z 2018 roku i dotyczy nie małej lokalnej firmy, ale dużej i międzynarodowej.

W moje ocenie przyczyną tego stanu rzeczy jest brak dostatecznie rozwiniętych modeli matematycznych, które pozwalałyby w procesie projektowania produktu programistycznego uzyskiwać gwarancje jego funkcjonalnej poprawności. Zresztą ten brak ma wpływ nie tylko na aplikacje z obszaru IT, ale też i na podręczniki języków programowania, co znów pośrednio wpływa na jakość aplikacji.

Wydany w roku 1960 definicyjny raport języka Algolu 60 — języka, który w dużej mierze wytyczył drogę rozwoju informatyki dla kilku pokoleń informatyków — wg. mnie znacznie przewyższał dzisiejsze podręczniki pod względem nie tylko precyzji i pełności wypowiedzi, ale też i zwartości.

W mojej ocenie niepowodzenie prób zbudowania formalnego i praktycznego zarazem systemu uzyskiwania gwarancji poprawności programów, a więc tzw. logiki programów, miało źródła w dwóch grupach problemów.

Pierwsza wiąże się z faktem, że zbudowanie logiki programów dla konkretnego języka wymaga opisania semantyki tego języka na gruncie matematyki. Mimo wielu prób w tym obszarze żadna z nich nie doprowadziła do wprowadzenia modeli matematycznych do praktyki inżynierii oprogramowania. W moim przekonaniu nie mogło być inaczej, gdyż dla istniejących języków sensownych semantyk matematycznych zbudować się raczej nie da. Przyczyną tego stanu rzeczy jest fakt, że języki programowania budowano rozpoczynając od składni, a nie od denotacji, czyli znaczeń. Innymi słowy najpierw decydowano, jak będziemy wyrażać treści, a dopiero później, jakie to będą treści. To oczywiście prosta konsekwencją historycznego faktu, że gdy zaczęto się zastanawiać nad tworzeniem semantyk, składnie języków już istniały.

Druga grupa problemów wiąże się z milczącym założeniem, że budowanie programów matematycznie poprawnych powinno przebiegać w kolejności — najpierw program, a później dowód jego poprawności. Ta kolejność jest oczywista w matematyce — najpierw hipoteza, a później jej dowód — jednak dla każdego inżyniera absurdalny musi być pomysł, aby najpierw zbudować most, a dopiero później wykonać jego projekt wraz z obliczeniami.

Wobec wskazanych wyżej argumentów podjąłem próbę zaproponowania narzędzi matematycznych pozwalających na zbudowanie języka programowania opartego na pewnym szczególnym modelu matematycznym — zwanym denotacyjnym — a następnie zdefiniowania dla tego języka takich reguł programowania, które gwarantowałyby poprawność tworzonych programów.

Zamiast więc najpierw pisać program „intuicyjnie”, by później uzyskiwać (ograniczone) gwarancje jego poprawności przy pomocy testowania, budujemy program w sposób, który tę poprawność gwarantuje. Tym ideom poświęciłem moje badania prowadzone w latach 1970-1996, nigdy jednak nie doprowadziłem ich do poziomu na tyle praktycznego, aby można było podjąć eksperymenty w obszarze inżynierii oprogramowania.

Zobacz krótkie video-zaproszenie do projektu (ca. 4 min.) Zobacz.

Zobacz nieco pełniejsze video-zaproszenie do projektu (ca. 24 min.) Zobacz.

Zobacz rozmowę o projekcie ze scrum-masterem (ca. 55 min) Zobacz