Co jest w projekcie nowego

Utworzono: wtorek, 30 kwiecień 2019 06:09

Poprawiono: środa, 01 maj 2019 15:15

Odsłony: 4420

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:

1. Projektowanie i budowanie języków programowania:
   
   1. Formalna metoda (w dużej części algorytmizowalna) wyprowadzania składni z denotacji oraz semantyki denotacyjnej z obu.
   2. Idea składni kolokwialnej, która pozwala uczynić składnię przyjazną dla programisty bez zbytniego naruszania modelu denotacyjnego.
   3. Wprowadzenie do modelu denotacyjnego mechanizmu obsługi błędów wspomaganego trójwartościowym rachunku predykatów.
   4. Model denotacyjny oparty na klasycznej teorii mnogości w miejsce dziedzin zwrotnych D. Scotta, co czyni go znacznie prostszym.
   5. 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.
2. Tworzenie programów poprawnych:
   
   1. 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.
   2. 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.
3. Ogólne narzędzia matematyczne:
   
   1. Gramatyki równaniowe jako narzędzie opisu składni.
   2. 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.