Logogram strony

Myśliciel A.Rodin

Narodziny gwiazdy

Rozmiar tekstu

Książka

Denotacyjna inżynieria języków programowania, preprint 2019

DOI: 10.13140/RG.2.2.12561.07527

Od września 2019 r. pracuję nad przygotowaniem prezentacji do mojego kursu akademickiego na Wydziale Matematyki, Informatyki i Mechaniki Uniwersytetu Warszawskiego, który będę prowadził w semestrze wiosennym 2019/2020. Kurs obejmie 30 godzin wykładowych oraz 30 godzin laboratorium. Laburatorium poprowadzi prof. Aleksy Schubert. 

Ponieważ moje prezentacje przygotowuję w wersji angielskiej, do takiejż wersji mojej książki wprowadzam dość liczbe poprawki i uzupełnienia. Nie starcza mi jednak już czasu na wprowadzanie poprawek do wersji polskojęzycznej. W tej sytuacji zdecydowałem nie udostępniać jej do czasu wprowadzenia zmian. Wersję angielską można pobrać ze strony The Book.

Aktualnie książka stanowi najbogatsze źródło wiedzy o projekcie i jest poświęcona dwóm obszarom badawczym:

  1. Projektowanie języków programowania wraz z ich modelem denotacyjnym. 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. Ten efekt jest osiągany przez zdefiniowanie algebry denotacji w pierwszym rzędzie, by później wygenerować z niej składnię.
  2. Tworzenie zdrowych konstruktorów programów w językach z semantyką denotacyjną. W moim ujęciu programy składniowo zawierają swoje specyfikacje w sensie całkowitej poprawności z czystą terminacją (bez komunikatu błędu). Program nazywamy poprawnym, gdy jest poprawny względem zawartej w nim specyfikacji. Konstruktor programów jest zdrowy, gdy z programów poprawnych tworzy programy poprawne.

Obie metody są ilustrowane na przykładzie wirtualnego języka Lingua.

Aspekt 1. jest również skrótowo przedstawiony w pracy opisanej na stronie On the development of a denotational model.