Czego dotyczy projekt

Utworzono: wtorek, 30 kwiecień 2019 05:59

Poprawiono: środa, 01 maj 2019 15:13

Odsłony: 4823

Projekt Inżynieria Denotacyjna rozpoczął się praktycznie w roku 2015, gdy postanowiłem podsumować wyniki moich wcześniejszych prac w książce pod obecnym tytułem Denotacyjna inżynieria języków programowania. Aktualnie jest to mój „prywatny” projekt, a więc nie związany z żadną instytucją.

Z perspektywy matematycznej jest to kontynuacja projektu MetaSoft realizowanego w latach 1970-1990 w Instytucie Podstaw Informatyki Polskiej Akademii Nauk. Lista najważniejszych prac związanych z MetaSoftem jest widoczna na stronie References to MetaSoft.

Obecny projekt obejmuje dwa obszary badawcze:

1. Denotacyjne modele języków programowania budowane w „odwrotnym porządku”, a więc od denotacji do składni. Ta metoda gwarantuje, że budowane języki mają w pełni sformalizowaną semantykę denotacyjną.
2. Budowanie programów poprawnych w miejsce dowodzenia poprawności programów. Dla języka z pełną semantyką denotacyjną można zdefiniować tzw. zdrowe konstruktory programów, które otrzymując poprawne programy na wejściu, „zwracają” poprawne programy na wyjściu. Przy programowaniu wstępującym (bottom up) ta technika pozwala ograniczać konieczność dowodzenia poprawności programów do ich początkowych modułów.

Podstawowe narzędzia matematyczne wykorzystywane w projekcie są następujące:

1. Semantyka denotacyjna gdzie dziedziny są zbiorami, a nie dziedzinami zwrotnymi Scotta-Strachey’a.
2. Algebry wielorodzajowe. Na denotacyjny model języka programowania składają się trzy algebry: algebra denotacji, algebra składni abstrakcyjnej (drzew parsingu) i algebra składni konkretnej (składni programisty). Model jest budowany w taki sposób, aby istniał homomorfizm ze składni konkretnej w denotacje, który stanowi semantykę denotacyjną tej składni.
3. Rachunek trójwartościowych predykatów oparty na trójwartościowym rachunku zdań J. McCarthy’ego. Ten rachunek pozwala opisać w modelu denotacyjnym mechanizm obsługi błędów.
4. Konstruktory programów oparte na logice Hoare’a z tzw. czystą terminacją, tj. terminacją bez komunikatu błędu. Tu właśnie wykorzystywane są predykaty trójwartościowe.
5. Gramatyki równaniowe jako pewne uogólnienie gramatyk bezkontekstowych.

Aktualnie pracuję nad tworzeniem modelu denotacyjnego dla wirtualnego języka programowania Lingua, dla którego buduję też konstruktory programów poprawnych.

W warstwie aplikatywnej Lingua operuje na strukturach danych obejmujących wartości boolowskie, liczby, teksty, listy, rekordy i wielowymiarowe tablice oraz dowolne kombinacje tych struktur. W języku są też dostępne dane i typy SQL-owe: wiersze, tabele i bazy danych. Wszystkie dane są powiązane z typami, które stanowią niezależne byty definiowalne przez użytkownika i składowalne w pamięci. Typy SQL-owe pozwalają m.in. na opisywanie więzów integralności.

W warstwie imperatywnej Lingua oferuje typowe konstrukcje strukturalne (a w tym konstrukcje SQL-owe) oraz procedury z rekurencją i rekurencją wzajemną. Programowanie obiektowe zostało jedynie naszkicowane, a współbieżność nie została na tym etapie uwzględniona.

Aktualnie poszukuję potencjalnych partnerów, którzy byliby gotowi rozwijać ze mną projekt zarówno w obszarze teorii, jak i implementacji. Ta druga dotyczyłaby nie tylko zbudowania interpretera lub kompilatora dla Lingua, ale też tworzenia środowiska narzędziowego zarówno dla budowniczych języków, jak i dla programistów. Więcej w artykułach Co jest jeszcze do zrobienia oraz Zaproszenie do projektu.

Projekt jest na bieżąco dokumentowany na niniejszej witrynie oraz na platformie ResearchGate.