Formalne metody inżynierii oprogramowania

(głos w sprawie powołania nowej sekcji PTI)

Jak powszechnie wiadomo, proces uruchamiania systemu oprogramowania konsumuje nierzadko połowę ceny całego systemu, po czym użytkownik i tak otrzymuje produkt z wieloma błędami. Jest to wynikiem stosowania dalece nieformalnych metod przy specy-fikowaniu, projektowaniu, tworzeniu i wreszcie dokumentowaniu dużych programów. Tam, gdzie inżynier mechanik lub elektronik posługują się rachunkiem matematycznym i rysunkiem technicznym, inżynier informatyk tworzy swój, i ileż bardziej złożony produkt niemalże z wyobraźni. Zamiast rysunku technicznego popartego obliczeniami otrzymuje on mętną i najczęściej niekompletną specyfikację w języku potocznym. Tę samą specyfikację przekazuje później użytkownikowi, który spędza wiele bezsennych nocy na odkrywaniu w systemie tego wszystkiego, co jego Twórca nie znalazłszy w specyfikacji musiał sobie dopowiedzieć. Opisana tutaj dość dramatyczna sytuacja nie pozostaje bez echa w środowisku praktyków i teoretyków. Od wielu lat prowadzi się na świecie (również w Polsce) liczne badania zmierzające do jej poprawy. Pierwszy sukces odnotowano ok. roku 1960, gdy w definicji Algolu użyto metody BNF do opisu syntaktyki. Od tego czasu metoda ta nie tylko stała się podstawowym narzędziem przy projektowaniu języków programowania, lecz także weszła na stałe do kompendium wiedzy informatycznej. Nadal pozostał jednak nie rozwiązany bardzo trudny problem opisu semantyki języków oprogramowania.

Zagadnieniami związanymi z semantyką języków programowania zaczęto się zajmować w końcu lat sześćdziesiątych, ale dopiero jakieś 10 lat później pojawiły się pierwsze wyniki mogące mieć zastosowanie praktyczne. Opracowanie metody semantyki deno-tacyjnej i odpowiednich metajęzyków do jej użycia w praktyce doprowadziło do powstania nowej metody wiedeńskiej (Vienna Development Method, w skrócie VDM). Jej zastosowania obejmują obecnie definiowanie (składni i semantyki) języków programowania, systematyczne tworzenie implementacji, projektowanie i implementację systemów operacyjnych, systemów obsługi baz danych, itp., a także projektowanie architektury sprzętu. Oprócz tej metody istnieją także inne, mniej znane, o podobnych zastosowaniach.

Wprowadzenie metod formalnych do opisu systemów programowania nie tylko uczyniło te opisy precyzyjnymi i kompletnymi, lecz także pozwoliło na zastosowanie wielu innych metod formal-