-
Utworzono: wtorek, 30 kwiecień 2019 06:09
-
Poprawiono: środa, 01 maj 2019 15:15
-
Odsłony: 4429
Projekt opiera się na ideach i technikach opisanych w moich pracach publikowanych w latach 1971-1996, które zostały podsumowane i rozszerzone w książce Denotacyjna inżynieria języków programowania. Wszystkie te idee opierają się na znanych od dawna pojęciach i narzędziach:
- semantyki denotacyjne D. Scotta i Ch. Strachey’a,
- gramatyki generacyjne N. Chomskiego,
- logiki programów T. Hoare’a,
- algebry wielorodzajowe wprowadzone do matematycznych podstaw informatyki przez J. A Goguena, J.W, Thatchera, E.G Wagnera oraz J.B Wrighta,
- trójwartościowy rachunek zdań McCarthy’ego.
Natomiast, co jest — jak sądzę — w moim ujęciu nowe, to:
- Projektowanie i budowanie języków programowania:
- Formalna metoda (w dużej części algorytmizowalna) wyprowadzania składni z denotacji oraz semantyki denotacyjnej z obu.
- Idea składni kolokwialnej, która pozwala uczynić składnię przyjazną dla programisty bez zbytniego naruszania modelu denotacyjnego.
- Wprowadzenie do modelu denotacyjnego mechanizmu obsługi błędów wspomaganego trójwartościowym rachunku predykatów.
- Model denotacyjny oparty na klasycznej teorii mnogości w miejsce dziedzin zwrotnych D. Scotta, co czyni go znacznie prostszym.
- Model typów danych, który obejmuje nie tylko typy strukturalne i definiowane przez użytkownika, ale też występujące w SQL więzy integralności.
- Tworzenie programów poprawnych:
- Metoda systematycznego budowania programów poprawnych względem zawartych w nich specyfikacji, w miejsce budowania specyfikacji i programu niezależnie od siebie, by następnie starać się udowodnić poprawność programu względem tej specyfikacji.
- Wykorzystanie predykatów trójwartościowych do rozszerzenia logiki Hoare’a o dowodzenie czystej terminacji programów oraz do opisania mechanizmów obsługi błędów.
- Ogólne narzędzia matematyczne:
- Gramatyki równaniowe jako narzędzie opisu składni.
- Trójwartościowy rachunek predykatów w zastosowaniu do budowania języków programowania oraz do definiowania zdrowych reguł budowania programów w tych językach.