Projekt dotyczy zagadnień: konstruowania, specyfikowania i weryfikowania oprogramowania, dedukcyjnych systemów opisu tych zagadnień oraz metod komputerowego wsparcia.

Proponowane podejście opiera się na idei, że zagadnienia programistyczne stawiające na pierwszym miejscu problem poprawności oprogramowania, można i należy traktować jako rodzaj działalności dedukcyjnej. Do opisu tych zagadnień wykorzystany zostanie formalizm Etykietowanych Systemów Dedukcyjnych.

Badaniami mają zostać objęte matematyczno-logiczne podstawy oraz szczególne obszary tegoż formalizmu zastosowań: obszar programów imperatywnych, obszar procesów reaktywnych i obszar typowania programów funkcyjnych.

Integralną częścią projektu mają być eksperymenty polegające na wykorzystaniu generycznych systemów kodowania logik i dowodzenia twierdzeń do kodowania opracowanych logik programistycznych/systemów typów. Planujemy też eksperymentalną produkcję, weryfikację i specyfikację prostego oprogramowania przez studentów Instytutu Matematycznego Uniwersytetu Gdańskiego pod nadzorem realizatorów.

W podejściu proponowanym przez niniejszy projekt systemy kodowania logik i dowodzenia twierdzeń stanowić mają uniwersalne środowiska programistyczne, tzn. wszelka działalność prowadząca do powstania poprawnego oprogramowania odbywać się będzie w interakcji z Isabelle, HOL, LEGO, ALF lub podobnym systemem.

---

Pełny opis

---

Comments to webmaster@ipipan.gda.pl.
Last modified: 16 September 1999

---