Uniwersytet Warszawski

Praca magisterska z informatyki

Analiza statyczna w Extended ML

Mikołaj Konarski 22 sierpnia 1997

Praca napisana pod kierunkiem dra hab. Andrzeja Tarleckiego

Spis rzeczy

I Wst_{}ep 4

1 Rzut oka na dziedzin_{}e 4 1.1 Standard ML . . . . . . . . . . . . . . . . . . . . . . . . . . . 4 1.2 Extended ML . . . . . . . . . . . . . . . . . . . . . . . . . . . 5 1.3 Semantyka naturalna . . . . . . . . . . . . . . . . . . . . . . . 6 1.4 EML Kit . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 7 1.5 Podsumowanie i diagram zależności . . . . . . . . . . . . . . . 8

2 Analiza statyczna 9 2.1 Objaśnienie terminu . . . . . . . . . . . . . . . . . . . . . . . 9 2.2 Podstawowe poj_{}ecia . . . . . . . . . . . . . . . . . . . . . . . . 10

2.2.1 Obiekt semantyczny . . . . . . . . . . . . . . . . . . . 10 2.2.2 Os _{}ad . . . . . . . . . . . . . . . . . . . . . . . . . . . . 11 2.2.3 Obiekt główny . . . . . . . . . . . . . . . . . . . . . . . 11

2.3 Ciekawsze zjawiska . . . . . . . . . . . . . . . . . . . . . . . . 12 2.3.1 Niedeterminizm . . . . . . . . . . . . . . . . . . . . . . 12 2.3.2 Wymuszanie . . . . . . . . . . . . . . . . . . . . . . . . 12

2.4 Analiza statyczna w Extended ML . . . . . . . . . . . . . . . 13

II Teoria 15

3 Jak badać poprawność aksjomatów 15

3.1 Szkic algorytmu . . . . . . . . . . . . . . . . . . . . . . . . . . 15 3.1.1 Sygnatury z aksjomatami . . . . . . . . . . . . . . . . 15 3.1.2 Analiza statyczna modułów w QUASI-EML . . . . . . 16 3.1.3 Naiwna próba rozwi _{}azania problemu . . . . . . . . . . 17 3.1.4 Pocieszaj _{}acy lemat . . . . . . . . . . . . . . . . . . . . 18 3.1.5 Poprawne rozwi _{}azanie . . . . . . . . . . . . . . . . . . 18 3.1.6 Badanie dopuszczalności aksjomatów . . . . . . . . . . 19

3.2 Interludium . . . . . . . . . . . . . . . . . . . . . . . . . . . . 20 3.2.1 Semantyka statyczna sygnatur . . . . . . . . . . . . . . 20 3.2.2 Elaboracja sygnatur . . . . . . . . . . . . . . . . . . . 21

3.3 W poszukiwaniu bazy B_{e} . . . . . . . . . . . . . . . . . . . . . 22 3.3.1 Baza pocz _{}atkowa . . . . . . . . . . . . . . . . . . . . . 22 3.3.2 Baza bież _{}aca . . . . . . . . . . . . . . . . . . . . . . . 22 3.3.3 Baza końcowa . . . . . . . . . . . . . . . . . . . . . . . 23

3.3.4 Spostrzeżenie . . . . . . . . . . . . . . . . . . . . . . . 23

4 Jak gromadzić ślady 24

4.1 Preludium . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 24 4.1.1 Semantyka statyczna wyrażeń . . . . . . . . . . . . . . 24 4.1.2 Elaboracja wyrażeń . . . . . . . . . . . . . . . . . . . . 24

4.2 Ślady . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 25 4.2.1 Ślad elaboracji . . . . . . . . . . . . . . . . . . . . . . 26 4.2.2 Ślad jako obiekt semantyczny . . . . . . . . . . . . . . 26

4.3 Zbieranie śladów . . . . . . . . . . . . . . . . . . . . . . . . . 27 4.3.1 Lokalna i globalna główność . . . . . . . . . . . . . . . 27 4.3.2 Konkretyzacja śladu . . . . . . . . . . . . . . . . . . . 29

III Implementacja 32

5 Aksjomaty w sygnaturach 32

6 Ślady j_{}ezyka Modułów 34

7 Ślady j_{}ezyka J _{}adra 37

8 Anegdota 39

IV Podsumowanie 40

Dodatki 42

A System EML Kit 42

B Obiekty semantyczne 43

Bibliografia 46

Cz_{}eść I

Wst_{}ep

1 Rzut oka na dziedzin_{}e

W ostatnich latach programowanie funkcyjne i metody specyfikacji, czerpi _{}ac z siebie nawzajem, szybko si_{}e rozwijały. Owocami tego pożytecznego zbliżenia s _{}a mi_{}edzy innymi formalizm Extended ML, a w dalszym rz_{}edzie system EML Kit. W tym rozdziale postaram si_{}e je opisać na tle środowiska, w którym si_{}e uformowały.

1.1 Standard ML

Standard ML (SML) [16] jest funkcyjnym j_{}ezykiem programowania, co oznacza, że działanie programu nie polega na stopniowej zmianie stanu maszyny, jak to jest w przypadku j_{}ezyków imperatywnych, lecz na obliczaniu wartości wyrażeń. Do opisywania wyrażeń służy cz_{}eść Standard ML zwana j_{}ezykiem J _{}adra.

Matematyczn _{}a podstaw _{}a modelu obliczeń SML jest rachunek λ [1] wraz z rozszerzonym systemem typów ML [3]. Uczynienie aplikowania funkcji głównym motorem ewaluacji ułatwia ”matematyczne” myślenie o działaniu programu. Z kolei silny system typów SML, dzi_{}eki swojej elastyczności i ogólności nie kr_{}epuj _{}ac użytkownika, pozwala wykrywać zdecydowan _{}a wi_{}ekszość bł_{}edów jeszcze przed wykonaniem programu, podczas procesu zwanego analiz _{}a statyczn _{}a.

SML posiada bardzo silne mechanizmy modularyzacji, do których można si_{}e odwoływać przy pomocy j_{}ezyka Modułów. Do budowania globalnej struktury programu służ _{}a struktury, które s _{}a atomowymi modułami, i funktory, wyrażaj _{}ace hierarchiczne zależności mi_{}edzy modułami i służ _{}ace do ich składania.

Podstawowym narz_{}edziem do opisu własności modułów, czyli do ich specyfikacji, s _{}a sygnatury:

signature TOTAL_PREORDER =
sig
    type elem
   val leq : elem * elem -> bool
    (* leq should be a total preorder *)
end

TOTAL_PREORDER to nazwa sygnatury, zdanie ”type elem” postuluje istnienie typu o nazwie elem, zaś zdanie ”val leq : elem * elem -> bool” stwierdza, że powinna istnieć funkcja leq o typie elem * elem -> bool. Komentarz w j_{}ezyku naturalnym zamykaj _{}acy sygnatur_{}e opisuje ż _{}adane własności funkcji leq.

Zarówno struktury jak i funktory mog _{}a być opatrzone sygnaturami. Ta przykładowa struktura jest zadeklarowana jako pasuj _{}aca do zdefiniowanej wcześniej sygnatury TOTAL_PREORDER:

structure OddRational : TOTAL_PREORDER =
struct
    type elem = int * int
    fun leq ((m, n), (k, l)) =
        if n = 0 andalso l = 0
            then m < 0 orelse (m > 0 andalso k > 0)
        else if (n < 0 andalso l >= 0)
                orelse (n >= 0 andalso l < 0)
                 then k * n <= m * l
             else m * l <= k * n
end

Typ elem jest tu par _{}a liczb całkowitych, zaś funkcja leq ma pewne cechy naturalnego porz _{}adku na liczbach wymiernych. Można pokazać, że wszystkie wymogi wyrażone w TOTAL_PREORDER zostały spełnione (również te opisane w komentarzu).

1.2 Extended ML

Poł _{}aczenie prostoty modelu obliczeń J _{}adra z sił _{}a j_{}ezyka Modułów czyni z SML wspaniałe narz_{}edzie do tworzenia i piel_{}egnowania dużych i złożonych systemów oprogramowania. Narzucaj _{}acymi si_{}e sposobami pracy z SML s _{}a warianty metodologii specyfikacji algebraicznych, choćby takie w których używa si_{}e j_{}ezyka naturalnego, jak w przykładzie powyżej.

Dzi_{}eki prostocie J _{}adra SML istnieje duża swoboda wyboru j_{}ezyków do wyrażania własości programów. Można używać j_{}ezyków bardzo słabych, jak na przykład logika równościowa, które w wypadku programowania imperatywnego nie miałyby szans zastosowania. Można używać także j_{}ezyków silnych, pozwalaj _{}acych wyrażać skomplikowane własności w sposób bardzo zwarty. Do takich j_{}ezyków należy na przykład bardzo mocne rozszerzenie logiki pierwszego rz_{}edu, za pomoc _{}a którego buduje si_{}e ciała aksjomatów w Extended ML.

Extended ML (EML) [10] jest formalizmem do wywodzenia programów w Standard ML z ich specyfikacji. Proces konstrukcji oprogramowania odbywa si_{}e stopniowo, pocz _{}awszy od czystej specyfikacji, poprzez stadia, w których przeplataj _{}a si_{}e fragmenty specyfikacji i kodu w SML, a skończywszy na w pełni wykonywalnym programie w SML. Wszystkie kroki wyrażane s _{}a w Extended ML, a ich poprawność dowodzona jest według reguł Semantyki Weryfikacyjnej EML.

Jako j_{}ezyk, Extended ML jest rozszerzeniem (dużego podzbioru) Standard ML. Można go podzielić, podobnie jak w przypadku SML, na j_{}ezyk J _{}adra i j_{}ezyk Modułów. Szczególn _{}a rol_{}e w procesie tworzenia oprogramowania odgrywa system modułów EML dopuszczaj _{}acy, oprócz elementów znanych z SML, sygnatury w których wyst_{}epuj _{}a aksjomaty:

signature TOTAL_PREORDER =
sig
    type elem
    val leq : elem * elem -> bool
    axiom forall (a, b) => leq (a, b) orelse leq (b, a)
    and forall (c, d, e) =>
        (leq (c, d) andalso leq (d, e)) implies leq (c, e)
end

Dzi_{}eki swojemu całkowitemu sformalizowaniu oraz sile mechanizmów modularyzacyjnych i j_{}ezyka specyfikacji, Extended ML daje możliwość konstruowania oprogramowania o niezwykłej niezawodności i łatwości rozbudowy oraz piel_{}egnacji. O wygodzie stosowania EML decyduj _{}a dwie rzeczy: czytelność i klarowność formalnej definicji oraz dost_{}epność i jakość narz_{}edzi wspomagaj _{}acych.

1.3 Semantyka naturalna

J_{}ezyk Standard ML jest ściśle opisany w swojej definicji [16]. Opis semantyki składa si_{}e z dwóch głównych cz_{}eści: Semantyki Statycznej i Semantyki Dynamicznej. Każda z nich podzielona jest z kolei na fragment dotycz _{}acy j_{}ezyka J _{}adra oraz fragment dotycz _{}acy j_{}ezyka Modułów.

Formalizm wykorzystany do przedstawienia semantyki SML zwie si_{}e semantyk _{}a naturaln _{}a [5]. W skład definicji wchodz _{}a zbiory reguł postaci:

\frac{ν_{1} ··· ν_{k}}{ϕ}

gdzie konkluzja ϕ jest zdaniem, zaś przesłanki ν_{i} s _{}a albo zdaniami albo regułami. W przypadku Semantyki Statycznej zdania mówi _{}a o możliwości przypisania elementowi j_{}ezyka pewnego typu, w przypadku Semantyki Dynamicznej — wartości.

Extended ML również posiada formaln _{}a definicj_{}e [10]. Podobnie jak EML jest w pewnym sensie rozszerzeniem SML, tak i definicja EML jest niejako nadbudowana na definicji SML. Choć miejscami zmodyfikowany jest sposób prezentacji, wprowadzone nowe elementy, poprawione bł_{}edy, to jednak ogólna struktura odziedziczona z definicji SML pozostaje zachowana. Jedyn _{}a zupełnie now _{}a cz_{}eści _{}a definicji EML jest Semantyka Weryfikacyjna, opisana tym samym formalizmem co Semantyka Statyczna i Semantyka Dynamiczna, a służ _{}aca wyrażeniu własności spełnienia specyfikacji przez implementacj_{}e.

Semantyka naturalna czyni możliwym opisanie tak wielkiego i skomplikowanego formalizmu jak EML we wzgl_{}ednie zwarty i elegancki sposób. Ta forma przezentacji ma jednak również swoje złe strony. Niektóre drobne bł_{}edy w definicji potrafi _{}a długo pozostawać niezauważone. Niektóre mechanizmy wydaj _{}a si_{}e proste i jednoznaczne jedynie dot _{}ad, dopóki nie zostanie podj_{}eta pierwsza próba ich implementacji. Niektóre globalne relacje pomi_{}edzy cz_{}eściami definicji s _{}a niejasne, dopóki jej hierarchia modułów nie zostanie opisana w poważnym formalizmie do definiowania struktury modularnej takim jak na przykład j_{}ezyk Modułów SML.

1.4 EML Kit

O systemie EML Kit można myśleć (z pewn _{}a doz _{}a dobrej woli) jako o w pełni deterministycznym, algorytmicznym i szczegółowym opisie Semantyki Statycznej i Semantyki Dynamicznej EML.

EML Kit zmierza do tego, by pełnić funkcje (podstawy i miejca do testowania) wygodnego środowiska do formalnego wywodzenia programów, przy użyciu j_{}ezyka, formalizmu i metodologii Extended ML.

Wersja 1.0 stworzona przez Marcina Jurdzińskiego, Mikołaja Konarskiego, Sławomira Leszczyńskiego i Aleksego Schuberta, jest kompletn _{}a implementacj _{}a Extended ML jako ”j_{}ezyka programowania”. Pozwala ona dokonywać analizy składniowej, sprawdzać poprawność typow _{}a i wyliczać wartość dowolnych programów EML, czy b_{}edzie to czysty Standard ML, czy też pełny EML z aksjomatami i innymi konstrukcjami specyfikacyjnymi. Proces ten odbywa si_{}e w ścisłej zgodności z Semantyk _{}a Statyczn _{}a i Sematyk _{}a Dynamiczn _{}a EML.

EML Kit bazuje na systemie ML Kit [2]; elastycznym, eleganckim i zmodularyzowanym interpreterze Standard ML, napisanym w Standard ML. ML Kit jest wiern _{}a i tak bezpośredni _{}a, jak to możliwe, implemetacj _{}a j_{}ezyka zdefiniowanego w definicji SML. Składnia abstakcyjna jest niemal dosłownie wzi_{}eta z definicji, a projekt wielu innych detali, takich jak na przykład konwencje nazewnicze, jest ściśle zainspirowany definicj _{}a.

1.5 Podsumowanie i diagram zależności

Dwa fakty — ten, że definicja EML jest rozszerzeniem definicji SML, i ten, że ML Kit jest tak bliski tej ostatniej — pomogły nam w naszych wysiłkach uczynienia systemu EML Kit wiern _{}a i klarown _{}a implementacj _{}a Extended ML. Byliśmy w stanie rozszerzyć ML Kit analogicznie do sposobu w jaki definicja EML rozszerza definicj_{}e SML, zachowuj _{}ac styl programowania właściwy dla systemu ML Kit. W ten sposób stworzyliśmy podstaw_{}e do rozwoju przyszłych narz_{}edzi Środowiska Programistycznego Extended ML, takich jak generatory musików dowodowych, czy prototypowe systemy dowodzenia. Ilustruje to znajomo wygl _{}adaj _{}acy diagram poniżej.

Programistyczne Środowisko EML

EML Kit

ML Kit

[figure]

Definicja EML

[figure]

Definicja SML

[figure]

[figure]

2 Analiza statyczna

Każdy nowoczesny j_{}ezyk programowania oparty jest na właściwym sobie prostym, klarownym matematycznym modelu. Proces analizy statycznej programu, przebiegaj _{}acy mi_{}edzy jego napisaniem a wykonaniem, polega na przetworzeniu go w odpowiadaj _{}acy mu matematyczny obiekt. W tym rozdziale chciałbym przedstawić bliżej to uj_{}ecie analizy statycznej, ilustruj _{}ac je konkretnymi przykładami dotycz _{}acymi specyfiki Extended ML.

2.1 Objaśnienie terminu

W skład analizy statycznej wchodz _{}a działania, dokonywane w z góry ograniczonym czasie, a maj _{}ace za podstaw_{}e tekst programu. Wynika st _{}ad, że w przypadku j_{}ezyków dopuszczaj _{}acych zjawisko nieterminacji, samego procesu wykonywania programu nie można zaliczyć do analizy statycznej.

Analiz_{}e statyczn _{}a wykonuje si_{}e, by sprawdzić poprawność programów, na przykład poprawność składniow _{}a, oraz by przygotować program do wykonania, być może poddaj _{}ac go wyrafinowanym przekształceniom w celu optymalizacji. Jeśli potraktujemy Extended ML jako j_{}ezyk programowania, to na podstawie systemu EML Kit b_{}edziemy mogli obejrzeć elementy przykładowej analizy statycznej tego j_{}ezyka.

Pierwszym stadium analizy statycznej w systemie EML Kit jest analiza składniowa, to znaczy przypisanie programowi jego drzewa rozbioru według gramatyki podanej w definicji Extended ML. Potem nast_{}epuje szereg dodatkowych korekcji tego drzewa, wynikaj _{}acych ze specyfiki składni EML i sposobu jej prezentacji, a w rezultacie powstaje ostateczne drzewo składni abstrakcyjnej programu, które b_{}edzie użyte jako podstawa zarówno do dalszej analizy statycznej jak i procesu wykonywania. Nast_{}epnym etapem jest elaboracja, to znaczy sprawdzanie poprawności programu jeśli chodzi o typy. Elaboracja odbywa si_{}e w oparciu o Semanyk_{}e Statyczn _{}a J _{}adra EML i Semantyk_{}e Statyczn _{}a Modułów EML, a przy przejściu z j_{}ezyka J _{}adra do Modułów dodatkowo odbywa si_{}e proces zwany rozwikływaniem przeładowania (ang.: overloading resolution).

Ponieważ programy napisane w EML mog _{}a si_{}e p_{}etlić, ich wykonywanie, które powinno si_{}e odbywać na podstawie Semantyki Dynamicznej EML, nie może być zaliczone do analizy statycznej. Z podobnych powodów weryfikacja programów w EML, która odbywałaby si_{}e na podstawie Semantyki Weryfikacyjnej EML, nie może być zaliczona do analizy statycznej. Ale już generowanie musików dowodowych (ang.: proof obligations) — pewna operacja wst_{}epna wzgl_{}edem weryfikacji, która być może zostanie w przyszłości zaimplementowana w ramach systemu EML Kit — zdecydowanie ma charakter statyczny i można j _{}a przytoczyć jako przykład analizy statycznej, choć może nieco wyższego, niż si_{}e to zwykle spotyka, rz_{}edu.

W pozostałej cz_{}eści rozdziału (i w całej pracy) skupimy si_{}e na przypadku analizy statycznej w najw_{}eższym rozumieniu tego terminu, to znaczy na sprawdzania poprawności typowej fraz j_{}ezykowych, wzgl_{}edem zadanej sematyki statycznej.

2.2 Podstawowe poj_{}ecia

2.2.1 Obiekt semantyczny

Sematyka statyczna frazom j_{}ezyka, czyli obiektom syntaktycznym, przypisuje pewne twory matematyczne, zwane obiektami semantycznymi. Pełne zestawienie obiektów semantycznych Semantyki Statycznej EML znajduje si_{}e w dodatku B.

Najbardziej oczywistym przykładem obiektu semantycznego jest typ. W Semantyce Statycznej J _{}adra EML wyrażeniom przypisywane s _{}a obiekty semantyczne τ, należ _{}ace do dziedziny semantycznej typów Type. Wyrażeniom b_{}ed _{}acymi rekordami przypisywane s _{}a typy rekordowe, wyrażeniom reprezentuj _{}acym funkcje przypisywane s _{}a typy funkcyjne, itd.

Innym powszechnie spotykanym rodzajem obiektów semantycznych s _{}a środowiska. Reprezentuj _{}a one skończony zbiór nazw, wraz z przypisanymi nazwom obiektami semantycznymi, na przykład typami. W Extended ML wynikiem analizy statycznej deklaracji s _{}a obiekty semantyczne oznaczane E, należ _{}ace do dziedziny semantycznej środowisk Env.

W Semantyce Statycznej Modułów wyst_{}epuj _{}a jeszcze bardziej złożone obiekty semantyczne. Strukturom odpowiadaj _{}a semantyczne struktury, składaj _{}ace si_{}e z nazwy struktury i środowiska opisuj _{}acego komponenty struktury, wraz z odpowiadaj _{}acymi im obiektami semantycznymi:

S lub (m, E) ∈ Str = StrName × Env

gdzie S to meta-zmienna przebiegaj _{}aca dziedzin_{}e Str, b_{}ed _{}ac _{}a produktem dziedzin StrName i Env, po których przebiegaj _{}a z kolei meta-zmienne m i E.

Sygnaturom odpowiadaj _{}a semantyczne sygnatury, składaj _{}ace si_{}e z semantycznej struktury i zbioru nazw, o których należy myśleć, że s _{}a zwi _{}azane:

Σ lub (N)S ∈ Sig = NameSet × Str

gdzie Σ, N i S to znowu meta-zmienne.

2.2.2 Os _{}ad

Os _{}ady to zdania postaci:

C ⊢ fraza ⇒ A

gdzie C i A to obiekty semantyczne, zaś fraza to element j_{}ezyka. Zdanie takie można czytać ”w kontekście C, fraza daje A”.

Przy pomocy Semantyki Statycznej J _{}adra EML można wywodzić na przykład zdania podobne do:

E ⊢ exp ⇒ τ

(”w środowisku E, wyrażenie exp daje typ τ”),

E_{1} ⊢ dec ⇒ E_{2}

(”w środowisku E_{1}, deklaracja dec daje środowisko E_{2}”). Zaś w Semantyce Statycznej Modułów pojawiaj _{}a si_{}e mi_{}edzy innymi os _{}ady postaci:

B ⊢ sigexp ⇒ S, γ

gdzie B to baza zawieraj _{}aca w szczególności środowisko, sigexp to sygnatura, a γ to ślad.

Aby zasygnalizować, czym jest ślad, musimy przypomieć, że w Semantyce Statycznej EML os _{}adami prawdziwymi s _{}a te, które można wywieść przy pomocy reguł. Każdy prawdziwy os _{}ad posiada wi_{}ec (być może wi_{}ecej niż jedno) drzewo wywodu. W pewnym uproszczeniu ślady s _{}a właśnie drzewami wywodu pewnych os _{}adów.

2.2.3 Obiekt główny

Niech S b_{}edzie semantyk _{}a statyczn _{}a i niech ≻ b_{}edzie cz_{}eściowym porz _{}adkiem na zbiorze wywodów S. Wtedy obiekt semantyczny A nazywamy głównym (ang.: principal) dla obiektu syntaktycznego fraza w kontekście obiektu semantycznego C, wzgl_{}edem relacji ≻ , w ramach semantyki S, gdy

• istnieje wywód γ w ramach S os _{}adu C ⊢ fraza ⇒ A,

• jeśli γ′ jest wywodem C ⊢ fraza ⇒ A′ w ramach S, to γ ≻ γ′.

W Semantyce Statycznej EML pojawiaj _{}a si_{}e definicje maj _{}ace charakter definicji obiektu głównego. Przytocz_{}e dwie spośród nich.

Typ τ wraz ze śladem γ jest główny dla wyrażenia exp w kontekście C, gdy (w troch_{}e innym sformułowaniu niż oryginalne)

• C ⊢ exp ⇒ τ, γ,

• jeśli C ⊢ exp ⇒ τ′, γ′, to τ ≻ τ′ i γ ≻ γ′. gdzie ”≻” jest relacj _{}a uogólniania typów (τ ≻ τ′, gdy typ τ jest ogólniejszy niż τ′, czyli gdy typ τ′ jest instancj _{}a typu τ), któr _{}a można w naturalny sposób rozszerzyć na ślady. Można udowodnić, że w SML (a także w EML) każde wyrażenie, które ma typ, ma również typ główny [14].

Mówimy, że sygnatura semantyczna (N)S z γ jest główna dla sygnatury syntaktycznej sigexp w bazie B gdy (w uproszczeniu)

• B ⊢ sigexp ⇒ S, γ,

• jeśli B ⊢ sigexp ⇒ S′, γ′, to (N)S≥S′ i γ ≻ γ′.

gdzie relacja ”≥” jest instancjacj _{}a sygnatur. W dodatku A do ksi _{}ażki [15] zawarty jest dowód istnienia sygnatur głównych w SML. Można pokazać, że również w EML każda sygnatura, dla której można wywieść sygnatur_{}e semantyczn _{}a, posiada sygnatur_{}e semantyczn _{}a główn _{}a.

2.3 Ciekawsze zjawiska

2.3.1 Niedeterminizm

Semantyk_{}e statyczn _{}a S nazywamy niedeterministyczn _{}a, jeśli istnieje taki element j_{}ezyka fraza i takie obiekty semantyczne C, A_{1}, A_{2}, że zarówno os _{}ad C ⊢ fraza ⇒ A_{1} jak i C ⊢ fraza ⇒ A_{2} s _{}a wyprowadzalne w S.

Sematyka Statyczna EML jest niedeterministyczna. St _{}ad na przykład nie każdy typ, jaki można wywieść dla wyrażenia, jest jego typem głównym. W pustym kontekście wyrażeniu:

let
   fun S x y z = (x z) (y z)
in
   S
end

można przypisać zarówno typ (α → α → γ) → (α → α) → α → γ, jak i typ (α → β → β) → (α → β) → α → β, ale żaden z nich nie jest równy głównemu typowi tego wyrażenia: (α → β → γ) → (α → β) → α → γ.

2.3.2 Wymuszanie

Ustalmy semantyk_{}e statyczn _{}a S i operacj_{}e syntaktyczn _{}a insert, która w pewien sposób z dwóch obiektów syntaktycznych tworzy jeden. Niech T i P b_{}ed _{}a obiektami syntaktycznymi. Niech C b_{}edzie obiektem semantycznym i niech ϕ b_{}edzie własności _{}a obiektów semantycznych.

Wtedy mówimy, że P wymusza ϕ w insert(P, T) przy C, gdy jednocześnie • istnieje obiekt semantyczny A taki, że można wywieść C ⊢ T ⇒ A oraz

nie zachodzi własność ϕ dla A,

• dla każdego A′, dla którego można wywieść C ⊢ insert(P, T) ⇒ A′, zachodzi własność ϕ.

Ważnym przypadkiem wymuszania w Semantyce Statycznej EML jest wymuszenie przez aksjomat zrównania typów w sygnaturze. Ilustruje to nast_{}epuj _{}acy przykład:

sig
    type t
    type u
    val f : t -> u
    axiom forall x => f x == f (f x)
end

Niech insert(P, T) b_{}edzie powyższ _{}a sygnatur _{}a, P wyst_{}epuj _{}acym w niej aksjomatem, a T sygnatur _{}a bez aksjomatu. Niech C b_{}edzie pust _{}a baz _{}a, a ϕ własności _{}a obiektu semantycznego, składaj _{}acego si_{}e w szczególności ze środowiska, mówi _{}ac _{}a, że powinno ono przypisywać typom syntaktycznym t i u ten sam typ semantyczny.

Widać, że obiekt powstały w wyniku głównego wywodu dla T nie spełnia własności ϕ. Natomiast obiekt powstały w wyniku głównego wywodu dla sygnatury insert(P, T), a co za tym idzie również każdy obiekt, jaki można wywieść dla tej sygnatury, spełnia ϕ. Tak wi_{}ec, w sygnaturze insert(P, T) aksjomat P wymusza zrównanie typów t i u.

2.4 Analiza statyczna w Extended ML

Semantyka Statyczna EML jest niedeterministyczna. W dodatku niektóre z przesłanek wyst_{}epuj _{}acych w regułach wyrażaj _{}a własności postaci ”dla każdego wywodu takiego że ϕ zachodzi, ψ musi zachodzić” — dobrymi przykładami s _{}a wymagania główności sygnatur pojawiaj _{}ace si_{}e w Semantyce Statycznej Modułów.

Z powodu niedeterminizmu i kwantyfikacji po nieskończonych zbiorach, niemożliwa jest bezpośrednia implementacja Semantyki Statycznej EML. Należy przetłumaczyć j _{}a do bardziej ”denotacyjnej” postaci (niektórzy wol _{}a nazywać t_{}e postać ”deterministyczn _{}a”). Dopiero wtedy może ona zostać niemal dosłownie zaimplementowana w j_{}ezyku programowania, na przykład w SML.

Takie przeformułowanie jest nietrywialnym zadaniem. Na szcz_{}eście, podobny problem dotycz _{}acy SML został rozwi _{}azany już jakiś czas temu. Algorytm Damasa i Milnera [3] jest dobrze znanym szkieletem narz_{}edzia do sprawdzania poprawności typowej programów J _{}adra SML. Zaś dowód twierdzenia o sygnaturach głównych, z rozdziału A.2 klasycznej pozycji [15], jest przewodnikiem w zmaganiach z j_{}ezykiem Modułów SML. W końcu, sam ML Kit jest bardzo klarown _{}a i skromn _{}a reformulacj _{}a i implementacj _{}a Semantyki Statycznej SML, opart _{}a na wymienionych powyżej ideach.

Moja praca nad przeformułowaniem specyficznych dla EML fragmentów Semantyki Statycznej czasami sprowadzała si_{}e do trywialnych rozszerzeń na przykład algorytmu Damasa i Milnera, gdzie jedynym kłopotem było zmaganie z maszyneri _{}a systemu ML Kit. Tak było w przypadku prac nad kwantyfikatorami i pozostałymi konstrukcjami specyfikacyjnymi oraz w przypadku analizy innych niż podstawowe postaci aksjomatów.

Czasami jednak rozszerzenie wymagało dowodu poprawności, albo bardzo dobrej znajomości budowy systemu. Było to potrzebne na przykład przy okazji prac nad semantyk _{}a funktorów EML, oraz nad ustaleniem poprawności rozwi _{}azań dotycz _{}acych rozwikływania przeładowania i zbiorów jawnych zmiennych typowych.

Jeszcze kiedy indziej trzeba było znaleźć zupełnie nowe podejście, udowodnić jego poprawność i zmieścić w ramach systemu ML Kit. Niektóre z takich przedsi_{}ewzi_{}eć doprowadziły do propozycji zmian w samej definicji EML. Tak było w przypadku prac nad zasi_{}egiem zmiennych typowych, nad warunkami poprawności aksjomatów, czy nad reprezentacj _{}a śladów.

Jednak zdecydowanie najwi_{}eksze trudności sprawiały elaboracja aksjomatów w sygnaturach oraz zbieranie śladów analizy statycznej. Te właśnie dwa zagadnienia zostan _{}a omówione ze szczególn _{}a dokładności _{}a w nast_{}epnych rozdziałach. Opis innych nietrywialnych problemów, w szczególności tych wymienionych powyżej, znajduje si_{}e w pracy [4]. Natomiast wyczerpuj _{}acy obraz implementacji analizy statycznej EML, w ramach systemu EML Kit, można uzyskać jedynie poprzez lektur_{}e jego kodu źródłowego, wraz z definicj _{}a Extended ML.

Cz_{}eść II

Teoria

3 Jak badać poprawność aksjomatów

W Extended ML aksjomaty mog _{}a wyst_{}epować zarówno w strukturach, jak i w sygnaturach. Poprawność statyczn _{}a aksjomatów w strukturach można dość prosto sprowadzić do poprawności wyrażenia logicznego, stanowi _{}acego najważniejsz _{}a cz_{}eść ciała tych aksjomatów. Z kolei poprawność tego wyrażenia, choć zawierać ono może konstrukcje j_{}ezykowe specyficzne dla EML, łatwo sprawdzić metodami analogicznymi co w SML.

Dla odmiany poprawności statycznej aksjomatów w sygnaturach nie można sprawdzić metodami analizy statycznej SML. Podstawow _{}a cech _{}a tych metod jest liniowa widoczność, to znaczy ocenianie poprawności frazy tylko na podstawie informacji, uzyskanych z badania programu do tej frazy wł _{}acznie, bez ”wybiegania naprzód”. Natomiast, jak b_{}edzie widać z dalszych rozważań, poprawność aksjomatu może zależeć nie tylko od pocz _{}atkowego fragmentu sygnatury, ale od dowolnie dużej porcji sygnatury za aksjomatem.

3.1 Szkic algorytmu

W tym rozdziale podejm_{}e prób_{}e naszkicowania algorytmu elaboracji sygnatur Extended ML, potencjalnie zawieraj _{}acych aksjomaty.

3.1.1 Sygnatury z aksjomatami

Reguła 65 Semantyki Statycznej EML (rozpatruj_{}e tu nieco uproszczon _{}a wersj_{}e) opisuje znaczenie syntaktycznej sygnatury, jako element dziedziny semantycznej Sig. Ta reguła jest troch_{}e bardziej złożona niż jej odpowiednik w Sematyce Statycznej SML. Jak można łatwo pokazać, dodatkowa druga i trzecia przesłanka zapewnia, że aksjomaty nie wymuszaj _{}a zrównania typów, ani uznania typu za równościowy w sygnaturze. To ograniczenie jest narzucone przy użyciu operacji strip, ”obdzieraj _{}acej” sygnatur_{}e z aksjomatów:

\frac{(N)S with γ principal for sigexp in B strip(sigexp, γ) = (sigexp′, γ′) (N)S with γ′ principal for sigexp′ in B}{B ⊢ sigexp ⇒ (N)S, (N)γ}  (65)

Te specyficzne dla EML, dodatkowe warunki na poprawn _{}a postać sygnatur wprowadzone s _{}a głównie po to, by programy Extended ML po zakończeniu procesu ich konstruowania, automatycznie stawały si_{}e poprawnymi programami j_{}ezyka Standard ML. Inymi słowy, gdy nie ma konstrukcji specyfikacjnych zamiast wykonywalnego kodu, i gdy tylko wszystkie aksjomaty, pełni _{}ace już jedynie rol_{}e komentarzy, zostaj _{}a usuni_{}ete, program EML powinien być jedncześnie programem SML. Rozpatrzmy przykład:

functor F (Arg : sig
                     type t
                     val f : t -> int
                     type u
                     val a : u
                     axiom f a = 0
                 end) :
sig
    val b : int
end =
struct
    val b = Arg.f Arg.a
end

Ten program nie jest poprawny, ponieważ aksjomat w sygnaturze wymusza zrównanie typów t i u. Gdyby nie ograniczenia w regule 65, powyższy program byłby poprawny. Jednak jego wersja ”obdarta” z aksjomatów jest niepoprawnym programem j_{}ezyka SML, z powodu aplikacji funkcji Arg.f, która ma typ t -> int, do argumentu Arg.a o typie u.

3.1.2 Analiza statyczna modułów w QUASI-EML

Niech QUASI-EML b_{}edzie dialektem EML, w którym druga i trzecia przesłanka s _{}a nieobecne w regule 65. W QUASI-EML reguła 65 wygl _{}ada wobec tego nast_{}epuj _{}aco:

\frac{(N)S with γ principal for sigexp in B}{B ⊢ sigexp ⇒ (N)S, (N)γ}

Lemat 3.1. W QUASI-EML skróty typowe (ang.: type abbreviations) mog _{}a zostać zdefiniowane jako formy pochodne (ang.: derived forms).

Zamiast formalnego dowodu rozpatrzmy przykładowy program:

sig
    type 'a t
    type u = int t (* a type abbreviation *)
    sharing type u = int
end

Pochodzi on z ksi _{}ażki [15], strona 66, i zawiera skrót typowy w miejscu oznaczonym komentarzem. W j_{}ezyku QUASI-EML można napisać program równoważny temu programowi, ale z form _{}a pochodn _{}a w miejscu skrótu typowego:

sig
    type 'a t
    type u
    axiom true orelse (forall (c : u, d : int t) => c == d)
    sharing type u = int
end

Wniosek 3.2. W QUASI-EML rekonstrukcja sygnatur głównych jest nierozstrzygalna.

Powodem jest to, że skróty typowe w poł _{}aczeniu z postulatami równości typów (ang.: sharing equations) czyni _{}a rekonstrukcj_{}e sygnatur głównych tak trudn _{}a jak unifikacja drugiego rz_{}edu. (W powyższym przykładzie unifikacja drugiego rz_{}edu byłaby potrzebna by zdecydować czy Λ'a.int, czy też Λ'a.'a jest najogólniejsz _{}a funkcj _{}a typow _{}a, jaka może być przypisana t.) Jako że unifkacja drugiego rz_{}edu jest nierozstrzygalna [15], dostajemy nierozstrzygalność rekonstrukcji sygnatur głównych w QUASI-EML.

3.1.3 Naiwna próba rozwi _{}azania problemu

Teraz powróćmy do problemu elaboracji sygnatur j_{}ezyka EML. Patrz _{}ac na reguł_{}e 65 Semantyki Statycznej EML:

\frac{(N)S with γ principal for sigexp in B strip(sigexp, γ) = (sigexp′, γ′) (N)S with γ′ principal for sigexp′ in B}{B ⊢ sigexp ⇒ (N)S, (N)γ}  (65)

można dojść do wniosku, że poprawny jest najprostszy sposób jej algorytmizacji (dla uproszczenia nie uwzgl_{}edniam tutaj śladów):

1. dokonaj elaboracji oryginalnej sigexp dostaj _{}ac sygnatur_{}e główn _{}a (N)S,

2. obedrzyj sigexp z aksjomatów dostaj _{}ac sigexp′,

3. dokonaj elaboracji sigexp′ uzyskuj _{}ac jej sygnatur_{}e główn _{}a (N′)S′,

4. jeśli (N)S i (N′)S′ s _{}a identyczne wtedy (N)S jest rezultatem, w przeciwnym przypadku sygnatura była niepoprawna.

Niestety implementacja pierwszego kroku jest niemożliwa, gdyż byłaby również rozwi _{}azaniem (nierozstrzygalnego) problemu rekonstrukcji głównych sygnatur w QUASI-EML.

3.1.4 Pocieszaj _{}acy lemat

Na szcz_{}eście zachodzi nast_{}epuj _{}acy lemat.

Lemat 3.3 (Pocieszaj _{}acy Lemat). Aksjomaty nie maj _{}a wkładu w zawartość środowiska powstałego w wyniku elaboracji sygnatury. Co wi_{}ecej, obecność i tożsamość śladów powstałych jako rezultat elaboracji aksjomatów nie wpływa na elaboracj_{}e pozostałych komponentów sygnatury.

Dowód. Prawdziwość pierwszej cz_{}eści lematu wynika z reguły 74.1 Semantyki Statycznej EML:

\frac{B ⊢ axdesc ⇒ γ}{B ⊢ axiom axdesc ⇒ \{\} in Env, γ}

Dowód drugiej cz_{}eści to żmudna indukcja po regułach 63–90.

Wniosek 3.4. Aksjomaty mog _{}a wpływać na elaboracj_{}e sygnatury tylko przez wymuszanie zrównania typów, albo uznania typu za równościowy, a nie przez nietrywialny wkład, to znaczy wkład do wynikowego środowiska, lub zmian_{}e śladu inn _{}a niż proste wstawienie komponentu.

3.1.5 Poprawne rozwi _{}azanie

Bazuj _{}ac na Lemacie 3.3 i Wniosku 3.4 można teraz sformułować szkic algorytmu implementuj _{}acego reguł_{}e 65:

1. obedrzyj sigexp z aksjomatów dostaj _{}ac sigexp′,

2. dokonaj elaboracji sigexp′ dostaj _{}ac sygnatur_{}e główn _{}a (N′)S′ i ślad γ′,

3. sprawdź, że aksjomaty nie wymuszaj _{}a zrównania typów, ani uznania typu za równościowy w sigexp,

4. dokonaj elaboracji aksjomatów zgodnie z reguł _{}a 74.1, uzyskuj _{}ac ślady γ_{1}, …, γ_{n},

5. jeśli wszystko przebiegło poprawnie, wynikiem jest (N′)S′ i dodatkowo γ′ ze śladami γ_{1}, …, γ_{n} wstawionymi w odpowiednich miejscach.

(Intuicje prowadz _{}ace do podobnego rozwi _{}azania zostały sformułowane przez Stefana Kahrsa w [9].)

Twierdzenie 3.5. Powyższa procedura jest poprawna.

Dowód. Ślady elaboracji komponentów sygnatury s _{}a składane w ”wolny” sposób (patrz np. reguła 81 cytowana w rozdziale 3.2.2 poniżej). Dzi_{}eki temu proste wstawienie γ_{1}, …, γ_{n} do γ′ w kroku 5 jest wystarczaj _{}ace, by poprawnie zrekonstruować γ, czyli ślad, jaki powstałby w czasie elaboracji sigexp. W takim razie, gdy kontrola przeprowadzona w kroku 3 upewnia nas, że aksjomaty nie wymuszaj _{}a zrównania typów, ani uznania typu za równościowy, wiemy z Wniosku 3.4, iż sygnatura semantyczna (N′)S′, wynikaj _{}aca z elaboracji sigexp′, wraz ze śladem γ jest główna dla sigexp.

Zanalizujmy kroki naszkicowane powyżej. Krok 1 jest prost _{}a syntaktyczn _{}a operacj _{}a. Ponieważ sigexp′ jest pozbawione aksjomatów, krok 2 jest tak łatwy jak elaboracja sygnatur SML (pomijaj _{}ac zbieranie śladów opisane w rozdziale 4). Wstawianie śladów γ_{1}, …, γ_{n} do γ′ w kroku 5 jest jedynie prostym problemem natury technicznej. Pozostaje implementacja kroków 3 i 4.

3.1.6 Badanie dopuszczalności aksjomatów

Załóżmy, że mamy sygnatur_{}e sigexp ze znajduj _{}acym si_{}e wewn _{}atrz niej aksjomatem. Niech sigexp′ b_{}edzie sygnatur _{}a podobn _{}a do sigexp, ale z pust _{}a specyfikacj _{}a w miejscu, gdzie w sigexp znajdował si_{}e aksjomat. Załóżmy, że istnieje wywód Der′ głównej sygnatury dla sigexp′ i niech Der_{e} b_{}edzie jego podwywodem, odpowiadaj _{}acym pustej specyfikacji. Niech B_{e} b_{}edzie baz _{}a, jaka znajduje si_{}e w korzeniu Der_{e}.

Twierdzenie 3.6. Aksjomat nie wymusza zrównania typów ani uznania typu za równościowy w sigexp wtedy i tylko wtedy, gdy istnieje derywacja Der_{ax} głównego śladu dla aksjomatu w bazie B_{e}.

Dowód (⇐). Przypuśćmy, że istnieje Der_{ax}. Wtedy Der′ z Der_{ax} w miejscu Der_{e} jest szkieletem głównego wywodu Der dla sigexp. Aby ten szkielet przekształcić w formalnie poprawne drzewo wywodu, wystarczy na mocy Lematu 3.3 wykonać dodatkowo dwie operacje na każdym przodku w_{}ezła Der_{e}. Pierwsza operacja to poprawne wstawienie śladu wynikaj _{}acego z Der_{ax} do śladu w_{}ezła. Druga to zast _{}apienie pustej specyfikacji, wyst_{}epuj _{}acej w w_{}eźle, przez aksjomat.

Po tych operacjach Der jest poprawnym wywodem dla sigexp i, co wi_{}ecej, głównym wywodem, gdyż Der′ i Der_{ax} s _{}a główne. Teraz należy zauważyć, że Der ma t_{}e sam _{}a wynikow _{}a sygnatur_{}e co Der′, a jego ślad jest prostym rozszerzeniem śladu Der′. W takim razie z definicji wymuszania wynika, że aksjomat nie wymusza zrównania typów, ani uznania typu za równościowy w sigexp.

(⇒). Skoro sigexp′ ma główny wywód i aksjomat niczego nie wymusza, to z Wniosku 3.4 istnieje główny wywód dla sigexp. Oczywiście jego podwywód odpowiadaj _{}acy aksjomatowi jest również główny. Pozostaje udowodnić, że ten wywód dla aksjomatu zaczyna si_{}e w bazie B_{e}.

Z Lematu 3.3, aksjomat (który jak wiemy niczego nie wymusza) nie może wpływać na bazy, wyst_{}epuj _{}ace w głównym wywodzie dla sigexp. A wi_{}ec wywód główny dla aksjomatu jest wykonywany w tej samej bazie, co wywód dla Der_{e}, czyli w bazie B_{e}.

Sprawdzenie, że istnieje wywód główny dla aksjomatu w danej bazie, nie jest bardziej skomplikowane, niż elaboracja aksjomatu wyst_{}epuj _{}acego w strukturze. W dodatku, jak można było zobaczyć z dowodu, ślady wyprodukowane jako rezultat tej elaboracji s _{}a właśnie tymi wymaganymi w kroku 4 z rozdziału 3.1.5.

Teraz jedyn _{}a pozostaj _{}ac _{}a trudności _{}a w zaimplemetowaniu kroku 3 z rozdziału 3.1.5, a w ten sposób całego już algorytmu, jest obliczanie baz B_{e} dla danych aksjomatów.

3.2 Interludium

Tak naprawd_{}e, wiemy już sk _{}ad dostać baz_{}e B_{e}. Jest ona jednym z komponentów śladu γ′ wynikaj _{}acego z elaboracji sigexp′ (w kroku 2, rozdział 3.1.5). Istniej _{}a jednak dwa problemy.

Po pierwsze, dla prostoty założyliśmy w rozdziale 2.2.2, że ślady s _{}a pełnymi drzewami wywodu. W rzeczywistości, chociaż można zrekonstruować drzewo wywodu dla frazy ze śladu elaboracji tej frazy, to jednak zadanie to jest niewiele łatwiejsze, niż zbudowanie drzewa wywodu dla frazy bez opierania si_{}e na śladzie.

Po drugie ślady s _{}a niezb_{}edne jedynie Semantyce Weryfikacyjnej EML. Jeśli udało by si_{}e znaleźć wygodny sposób obliczania B_{e} bez śladów, nie było by potrzeby wprowadzania śladów do implementacji Sematyki Statycznej. Może to być o tyle pożyteczne, że implementacja śladów jest cokolwiek skomplikowana i kłopotliwa (patrz rozdział 4).

Aby zobaczyć, jak należy obliczać bazy B_{e} bez użycia śladów, powinniśmy najpierw zagł_{}ebić si_{}e w szczegóły elaboracji sygnatur w SML (albo równoważnie, elaboracji sygnatur bez aksjomatów w EML).

3.2.1 Semantyka statyczna sygnatur

Zarówno Semantyka Statyczna Modułów Extended ML jak i Standard ML silnie polega na niedeterminizmie. W ramach budowania wywodu, tożsamość wyst_{}epuj _{}acych w nim typów i struktur jest ”niedeterministycznie zgadywana”. Na przykład w regule 83 (nieco uproszczonej):

\frac{tyvarseq = α^{(k)}  arity θ = k}{C ⊢ tyvarseq tycon ⇒ \{tycon ↦ (θ, \{\})\}}  (83)

θ może być dobrana tak, by spełnione były warunki na równość typów. Albo w regule 63:

\frac{B ⊢ spec ⇒ E, γ}{B ⊢ sig spec end ⇒ (m, E), m · γ}  (63)

m może zostać tak dobrane, by spełniona była równość odpowiednich struktur.

3.2.2 Elaboracja sygnatur

Aby pozbyć si_{}e niedeterminizmu tkwi _{}acego w Semantyce Statycznej Modułów, należy użyć algorytmu do obliczania sygnatury głównej, przypominaj _{}acego algorytm do rekonstrukcji typów głównych opisany przez Damasa i Milnera w pracy [3].

Zamiast być poprawnie ustalane od razu, nazwy typów i struktur należ _{}acych do sygnatury s _{}a uznawane za świeże, czyli różne od wszystkich dotychczas spotkanych. Potem, w procesie elaboracji sygnatury, systematycznie gromadzona jest realizacja, czyli (w uproszczeniu) skończony automorfizm nazw typów i struktur.

Za każdym razem, gdy okazuje si_{}e, że pewne nazwy powinny być równe, na przykład dlatego, że tak stanowi _{}a postulaty równości (ang.: sharing equations), wzbogaca si_{}e realizacj_{}e. Jednocześnie cały czas aplikuje si_{}e bież _{}ac _{}a realizacj_{}e do obiektów semantycznych, co ulepsza pierwsze ostrożne przybliżenia poprzez zrównywanie odpowiednich nazw. Etap ”zgadywania” zostaje w ten sposób odłożony do momentu, gdy wiadomo już dokładnie co powinno być odgadni_{}ete.

Proces gromadzenia i aplikowania realizacji szczególnie dobrze widoczny jest w kroku algorytmu dotycz _{}acym reguły 81, opisuj _{}acej elaboracj_{}e specyfikacji złożonej:

\frac{B ⊢ spec_{1} ⇒ E_{1}, γ_{1} B + E_{1} ⊢ spec_{2} ⇒ E_{2}, γ_{2}}{B ⊢ spec_{1} ⟨;⟩ spec_{2} ⇒ E_{1} + E_{2}, γ_{1} · γ_{2}}  (81)

Ogl _{}adaj _{}ac kod źródłowy implementacji tego kroku w systemie EML Kit, szczególn _{}a uwag_{}e zwróćmy na realizacje (rea1, rea2), ich złożenie (oo) oraz ich aplikacj_{}e do obiektów semantycznych (onB, onE):

fun elab_spec (B: Env.Basis, spec: IG.spec) :
    (Stat.Realisation * Env.Env * OG.spec) =
    case spec of
    ...
    (* Sequential specification *)
    | IG.SEQspec(i, spec1, spec2) =>
        let
            val (rea1, E1, out_spec1) = elab_spec(B, spec1)
            val B' = (rea1 onB B) B_plus_E E1
            val (rea2, E2, out_spec2) = elab_spec(B', spec2)
        in
            (rea2 oo rea1,
             (rea2 onE E1) E_plus_E E2,
             OG.SEQspec(okConv i, out_spec1, out_spec2))
        end
    ...

3.3 W poszukiwaniu bazy B_{e}

Znaj _{}ac podstawy algorytmu elaboracji sygnatur pozbawionych aksjomatów, spróbujmy zgadn _{}ac, jak dostać baz_{}e B_{e} dla danej sygnatury sigexp zawieraj _{}acej aksjomat.

3.3.1 Baza pocz _{}atkowa

Czy powinna to być baza używana przez algorytm, gdy zaczyna on elaboracj_{}e całego sigexp? Nie, i nast_{}epuj _{}acy przykład pokazuje, jakie mog _{}a być tego niedobre skutki:

signature S1 =
sig
    type t
    axiom forall (a : t) => true
end

W tej bazie nie ma typu t, a wi_{}ec aksjomat zostałby niepoprawnie uznany za źle skonstruowany.

3.3.2 Baza bież _{}aca

Może w takim razie użyć bazy, która pojawia si_{}e w miejscu tuż przed aksjomatem? Popatrzmy na przykład:

signature S2 =
sig
    type t
    type u
    axiom forall ( a : t, f : u -> bool) => f a
    sharing type t = u
end

Aksjomat wyst_{}epuj _{}acy tutaj nie wymusza zrównania typów, ponieważ w sygnaturze z aksjomatem usuni_{}etym, typy t i u byłyby zrównane. Niemniej elaboracja aksjomatu w bazie otrzymanej, kiedy algorytm skończy elaborować pierwsze dwie specyfikacje, nie powiedzie si_{}e, gdyż świeże semantyczne typy zostan _{}a przypisane t i u, bez uwzgl_{}ednienia pojawiaj _{}acego si_{}e dalej postulatu równości typów.

3.3.3 Baza końcowa

Wydaje si_{}e wi_{}ec, że baza zebrana na końcu elaboracji b_{}edzie dobrym kandydatem na B_{e}. Rzeczywiście elaboracja aksjomatu z poprzedniego przykładu przebiegnie tu pomyślnie, gdyż typy przypisane t i u s _{}a w niej zrównane. Niestety, w nast_{}epuj _{}acym przykładzie aksjomat, który jest wyraźnie źle skonstruowany, daje si_{}e elaborować w takiej bazie:

signature S3 =
sig
    axiom forall (a : t) => true
    type t
end

3.3.4 Spostrzeżenie

Jak widzimy, w bazie B_{e} powinny być dokładnie te komponenty, co w bazie tuż sprzed aksjomatu, ale ich tożsamość powinna odzwierciedlać informacj_{}e zebran _{}a podczas elaboracji całej sygnatury.

Spostrzeżenie 3.7. Okazuje si_{}e, że aby dostać baz_{}e B_{e} wystarczy zbobyć końcow _{}a realizacj_{}e rea, wykonuj _{}ac standardowy algorytm elaboracji dla sygnatury sigexp′, a nast_{}epnie zaaplikować rea do bazy, pobranej gdy algorytm zakończył analizowanie specyfikacji tuż przed aksjomatem.

Wniosek 3.8. Możliwe jest otrzymywanie bazy B_{e} — a co za tym idzie realizowanie kroku 3 z rozdziału 3.1.5 i dzi_{}eki temu przeprowadzanie poprawnej elaboracji sygnatur zawieraj _{}acych aksjomaty — bez użycia śladów.

4 Jak gromadzić ślady

Skomplikowanie operacji zbierania śladów wynika z faktu, że drzewa wywodu, odpowiadaj _{}ace poszczególnym stadiom elaboracji wyrażenia, nie s _{}a poddrzewami ostatecznego, poprawnego drzewa wywodu tego wyrażenia. Przed przyst _{}apieniem do rozważań na temat śladów spróbuj_{}e wyjaśnić to zjawisko.

4.1 Preludium

Przedstawiane w tym rozdziale przykłady pochodz _{}a z cz_{}eści wspólnej EML i SML. Elaboracj _{}a konstrukcji specyfikacyjnych J _{}adra EML rz _{}adz _{}a podobne do opisanych poniżej zasady.

4.1.1 Semantyka statyczna wyrażeń

Podobnie jak w Semantyce Statycznej Modułów (porównaj rozdział 3.2.1), w Semantyce Statycznej J _{}adra duż _{}a rol_{}e gra niedeterminizm. W wielu w_{}ezłach wywodów, typy przypisywane zmiennym s _{}a ”niedeterministycznie zgadywane”, tak aby mogły być zastosowane reguły, zakładaj _{}ace równość niektórych typów pojawiaj _{}acych si_{}e w przesłankach. Niedeterminizm wyst_{}epuje na przykład w regule 35 (uproszczonej):

\overline{C ⊢ var ⇒ (\{var ↦ τ\}, τ)}  (35)

Formalnemu argumentowi funkcji może tu zostać przypisany dowolny typ. Zaś w regule 2 (nieco uproszczonej):

\frac{C(longvar) ≻ τ}{C ⊢ longvar ⇒ τ}  (2)

typ zmiennej może być dowolnie wybrany spośród instancji typu tej zmiennej przechowywanego w środowisku.

4.1.2 Elaboracja wyrażeń

Lekarstwem na niemożliwy do bezpośredniego zaimplementowania niedeterminizm jest algorytm Damasa i Milnera [3].

Elaboruj _{}ac wyrażenie przy pomocy tego algorytmu, wywodzi si_{}e typy główne podwyrażeń, konkretyzuj _{}ac w razie potrzeby konteksty, w których odbywa si_{}e elaboracja. Zamiast ”zgadywać” typy, zakłada si_{}e że s _{}a one najbardziej ogólne, czyli że s _{}a świeżymi zmiennymi typowymi. W wypadku reguł, zakładaj _{}acych równość pewnych typów w przesłankach, przeprowadza si_{}e unifikacj_{}e. Aplikacja podstawień wynikłych z unifikacji reprezentuje precyzowanie wiedzy na temat tego, jakie typy powinny były być ”zgadni_{}ete” w poprzednich stadiach elaboracji.

W regule typowania aplikacji (nieco uproszczonej):

\frac{C ⊢ exp ⇒ τ′ → τ, γ  C ⊢ atexp ⇒ τ′, γ′}{C ⊢ exp atexp ⇒ τ, γ · γ′}  (10)

widać wymaganie równości typu τ′ w obu przesłankach. A oto fragment systemu EML Kit odpowiadaj _{}acy tej regule. S1, S2 i S3 s _{}a tu podstawieniami, oo ich złożeniem, a onC i on aplikacj _{}a podstawienia odpowiednio do kontekstu i typu:

fun elab_exp (C : Environments.Context, exp : IG.exp) :
    (Substitution * StatObject.Type * OG.exp) =
    case exp of
    ...
    (* Application expression *)                      (* rule 10 *)
    | IG.APPexp(i, exp, atexp) =>
        let
            val (S1, tau1, out_exp)   = elab_exp(C, exp)
            val (S2, tau2, out_atexp) = elab_atexp(S1 onC C, atexp)
            val new   = freshType()
            val arrow = StatObject.mkTypeArrow(tau2,new)
            val (S3, i') = Unify(arrow, S2 on tau1, i)
        in
            (S3 oo S2 oo S1, S3 on new,
             OG.APPexp(i', out_exp, out_atexp))
        end

Widać, jak zamiast ”niedeterministycznego zgadywania” używa si_{}e tu świeżego typu (freshType). Można zauważyć unifikacj_{}e (Unify) i aplikacje podstawień. Wyraźna jest też rola umowy, że każda elaboracja podwyrażenia daje w wyniku w szczególności wytworzone przez siebie podstawienie.

4.2 Ślady

Ślady służ _{}a akumulowaniu obiektów semantycznych pojawiaj _{}acych si_{}e podczas analizy statycznej. Do informacji przechowywanej w śladach odwołuje si_{}e nast_{}epnie Semantyka Weryfikacyjna EML. Ślady graj _{}a również pewn _{}a aktywn _{}a rol_{}e w Semantyce Statycznej EML, chociaż post_{}epuj _{}ac z wystarczaj _{}ac _{}a ostrożności _{}a można, jak pokazałem w rozdziale 3.3, poprawnie elaborować programy bez ich użycia.

4.2.1 Ślad elaboracji

W rozdziale 2.2.2 ślady zostały przedstawione, na potrzeby rozważań o analizie statycznej, jako drzewa wywodu os _{}adów semantyki statycznej. Jest to o tyle usprawiedliwione, iż ze śladu można zrekonstruować reprezentowany przez niego wywód, choć jak wspominałem w rozdziale 3.2, nie jest to proste.

Od tej pory, przez ślad analizy statycznej programu P w kontekście C, b_{}ed_{}e rozumiał główny ślad, jaki według Semantyki Statycznej EML (patrz rozdział 4.2.2) daje si_{}e wywieść dla P w C. Natomiast przez ślad elaboracji programu P w kontekście C, b_{}ed_{}e rozumiał ślad analizy statycznej P w φ(C), gdzie φ jest podstawieniem wynikłym z elaboracji P w C.

Na przykład, podczas elaboracji programu:

fun f x = (x 5) < 25

wyrażenie P, wyst_{}epuj _{}ace po prawej stronie znaku równości, elaborowane jest w pewnym kontekście C. W tym kontekście zmiennej x przypisany jest typ, b_{}ed _{}acy zmienn _{}a typow _{}a, nazwijmy j _{}a α. Widać, że nie istnieje ślad analizy statycznej P w kontekście C, ponieważ typ przypisany w C zmiennej x nie jest typem funkcyjnym, a wi_{}ec nie da si_{}e wywieść typu dla aplikacji (x 5). Natomiast ślad elaboracji P w kontekście C istnieje, gdyż równy jest on śladowi analizy statycznej P w kontekście φ(C), gdzie podstawienie φ, wynikaj _{}ace z elaboracji P, przypisuje zmiennej α typ int → int.

4.2.2 Ślad jako obiekt semantyczny

Ślady posiadaj _{}a pewn _{}a dodatkow _{}a struktur_{}e, wynikaj _{}ac _{}a z możliwości ich domykania. Operator Clos jest używany w kilku miejscach Semantyki Statycznej J _{}adra EML (reguły 11.1, 11.2, 11.3 i 17), aby domykać ślad wzgl_{}edem kontekstu:

Clos_{C}γ = ∀α^{(k)}.γ

gdzie ∀ to kwantyfikator wi _{}aż _{}acy zmienne typowe, zaś α^{(k)} to zmienne typowe wolne w γ, a nie wyst_{}epuj _{}ace wolno w C. W śladach Semantyki Statycznej Modułów EML można natomiast wi _{}azać nazwy struktur lub nazwy typów.

A oto pełna definicja śladów J _{}adra EML:

Trace = Tree(SimTrace ⊎ TraceScheme)

SimTrace = Type ⊎ Env ⊎ (Context × Type) ⊎ (Context × Env) ⊎

(Context × TyName) ⊎ TyEnv ⊎ (VarEnv × TyRea) TraceScheme = ⊎_{k≥0}TraceScheme^{(k)} TraceScheme^{(k)} = TyVar^{k} × Trace gdzie Tree(A) jest dziedzin _{}a skończonych binarnych drzew elementów z A (st _{}ad też pochodzi spotykany dalej operator składania śladów, pojawiaj _{}acy si_{}e we frazach w rodzaju γ · γ′). Pozostałe nazwy oznaczaj _{}a albo dziedziny obiektów Semantyki Statycznej EML, albo zbiory śladów szczególnej postaci, jak np. TraceScheme, który zawiera ślady b_{}ed _{}ace domkni_{}eciami innych śladów.

Prezentacja śladów Modułów EML w definicji Extended ML [10] nie jest w pełni satysfakcjonuj _{}aca, głównie z punktu widzenia osoby zajmuj _{}acej si_{}e implementacj _{}a. W nowej wersji definicji Extended ML [11] autorzy zdefiniowali ślady zgodnie z moj _{}a propozycj _{}a zawart _{}a w [4]:

Trace = Tree(Trace_{COR} ⊎ SimTrace ⊎ BoundTrace) BoundTrace = NameSet × Trace SimTrace = StrName ⊎ Rea ⊎ VarEnv ⊎ TyEnv ⊎ Env

gdzie Trace_{COR} to ślady J _{}adra EML, opisane powyżej. Zgodnie z t _{}a definicj _{}a przeprowadziłem implementacj_{}e zbierania śladów i ta definicja posłuży mi za podstaw_{}e rozważań o śladach, metodzie uzyskiwania śladów elaboracji programów i poprawności tej metody.

4.3 Zbieranie śladów

4.3.1 Lokalna i globalna główność

Zbieranie śladów prostych jest trywialne. Nieco kłopotów nastr_{}eczaj _{}a natomiast ślady, które uzyskuje si_{}e przez domkni_{}ecie innych śladów. Przykładem może być reguła 17 (tutaj nieco uproszczona):

\frac{C ⊢ valbind ⇒ VE, γ  VE′ = Clos_{C}VE}{C ⊢ val valbind ⇒ VE′ in Env, Clos_{C}γ}  (17)

gdzie śladem jaki należy wywieść dla frazy ”val valbind” jest domkni_{}ecie śladu γ, wywiedzionego dla jedynego podtermu tej frazy — ”valbind”. Twierdzenia podobne do poniższego, choć nieco bardziej skomplikowane, można dowieść również dla innych reguł, w których nast_{}epuje domykanie śladów.

Twierdzenie 4.1. Niech program P ma postać val P′. Niech C b_{}edzie kontekstem, γ śladem elaboracji P′ w kontekście C, zaś φ niech b_{}edzie podstawieniem wynikłym z tej elaboracji.

Wtedy śladem elaboracji P w kontekście C jest Clos_{φ(C)}γ.

Dowód. Wynikiem elaboracji P w kontekście C jest wywiedzenie głównego obiektu semantycznego dla P w kontekście φ(C) według reguły 17, lecz pomijaj _{}ac ślady. Skoro tak, to można zastosować reguł_{}e 17 dla programu P i kontekstu φ(C) i otrzymać tez_{}e.

Jednak najciekawszy jest przypadek śladów złożonych. Reguła 8, dotycz _{}aca typowania elementów rekordu, jest jedn _{}a z reguł, w których ślad programu jest otrzymywany przez złożenie śladów podprogramów:

\frac{C ⊢ exp ⇒ τ, U, γ  ⟨C ⊢ exprow ⇒ ϱ, U′, γ′⟩}{C ⊢ lab = exp ⟨ , exprow⟩ ⇒ \{lab ↦ τ\}⟨+ ϱ⟩, U⟨ ∪ U′⟩, γ⟨·γ′⟩} (8)

Reguła ta jest bardzo skomplikowana. Zamiast niej, za podstaw_{}e naszych rozważań przyjmijmy, nie wyst_{}epuj _{}ac _{}a w definicji EML, reguł_{}e typowania pary wyrażeń, b_{}ed _{}acej uproszczeniem szczególnego przypadku reguły 8:

\frac{C ⊢ exp ⇒ τ, γ C ⊢ exp′ ⇒ τ′, γ′}{C ⊢ (exp, exp′) ⇒ \{1 ↦ τ, 2 ↦ τ′\}, γ · γ′}

Spostrzeżenie 4.2. Niech program T ma postać (P, Q). Niech C b_{}edzie kontekstem. Wtedy elaboracja T w kontekście C ma dwie główne fazy:

• elaborowany jest podprogram P w kontekście C, przy czym otrzymywane jest podstawienie φ_{P} i ślad tej elaboracji γ_{P},

• elaborowany jest podprogram Q w kontekście φ_{P} (C), przy czym otrzymywane jest podstawienie φ_{Q} i ślad tej elaboracji γ_{Q}.

Powstaje pytanie jak uzyskać ślad elaboracji T w kontekście C, zakładaj _{}ac że γ_{P} i γ_{Q} s _{}a poprawnymi śladami elaboracji P i Q? Narzucaj _{}aca si_{}e odpowiedź, że ślad T równy jest γ_{P} · γ_{Q}, niestety nie jest prawdziwa. Ślad γ_{P} uzyskiwany jest w potencjalnie niegłównym dla T kontekście, wi_{}ec mimo iż γ_{P} jest główny dla P, może być zbyt ogólny, by stać si_{}e cz_{}eści _{}a śladu T. Ilustruje to nast_{}epuj _{}acy prosty przykład:

fun g fib = (fib, fib 5)

gdzie P to fib, zaś Q to fib 5. W γ_{P} zmienna fib nie ma przypisanego typu funkcyjnego, mimo że w śladzie T zmienna fib może mieć jedynie typ funkcyjny, gdyż z elaboracji Q wynika, że fib jest funkcj _{}a (w szczególności φ_{Q} przypisuje zmiennej typowej, która jest typem fib, typ funkcyjny).

Twierdzenie 4.3. Przyjmijmy oznaczenia ze Spostrzeżenia 4.2. Wtedy ślad elaboracji T w kontekście C równy jest γ̂ · γ_{Q}, gdzie γ̂ jest śladem elaboracji P w kontekście φ_{Q}(φ_{P} (C)).

Dowód. Ponieważ γ_{Q} jest śladem elaboracji Q w kontekście φ_{P} (C), wi_{}ec z definicji śladu elaboracji, γ_{Q} jest śladem analizy statycznej Q w kontekście φ_{Q}(φ_{P} (C)).

Z drugiej strony wynikiem elaboracji T w kontekście C jest wywiedzenie głównego obiektu semantycznego dla T w kontekście φ_{Q}(φ_{P} (C)), według reguły typowania pary wyrażeń, ale z pomini_{}eciem śladów. Ale w takim razie z reguły typowania pary wyrażeń wynika teza.

Odpowiedniki tego prostego twierdzenia dla innych reguł, w których nast_{}epuje złożenie śladów, s _{}a również dość oczywiste. Co wi_{}ecej podobne twierdzenia można udowodnić również dla j_{}ezyka Modułów EML, z tym że zamiast podstawień b_{}ed _{}a w nich wyst_{}epować realizacje.

Niestety bezpośrednie zastosowanie w algorytmie zbierania śladów procedury jaka wynika z Twierdzenia 4.3, prowadzi do podwójnej elaboracji P. Pierwszy raz w kontekście C, aby uzyskać podstawienie φ_{P} i drugi raz w kontekście φ_{Q}(φ_{P} (C)), aby uzyskać ślad γ̂.

4.3.2 Konkretyzacja śladu

Jednym z najbardziej niepokoj _{}acyh zjawisk, wyst_{}epuj _{}acych podczas budowania śladu programu ze śladów podprogramów, jest to, iż ślady podprogramów czasami powstaj _{}a na skutek domykania niegłównych dla całego programu śladów, wzgl_{}edem również niegłównych kontekstów. Dowód nast_{}epuj _{}acego twierdzenia pokazuje, że zjawisko to nie musi być groźne.

Twierdzenie 4.4. Niech P b_{}edzie programem napisanym w j_{}ezyku J _{}adra Extended ML. Niech D b_{}edzie kontekstem. Niech γ_{P} b_{}edzie śladem elaboracji P w kontekście D. Niech φ b_{}edzie podstawieniem.

Wtedy ślad elaboracji P w kontekście φ(D) równy jest φ(γ_{P}).

Dowód. Indukcja po strukturze γ_{P}. Przypadki bazowe i przypadek składania śladów wynikaj _{}a z podstawowych własności procesu elaboracji. Pozostaje przypadek, gdy γ_{P} ∈ TraceScheme. Wtedy, w ostatnim kroku elaboracji P, musiał wyst_{}epować pewien ślad γ, domykany wzgl_{}edem pewnego kontekstu C, przy czym γ_{P} = Clos_{C}γ.

Niech P′ b_{}edzie podprogramem P odpowiadaj _{}acym γ. Dla uproszczenia załóżmy, że P jest postaci val P′, a wi_{}ec elaboracja P′ jako cz_{}eści P odbyła si_{}e w kontekście D. Niech ta elaboracja daje podstawienie φ_{P′}. W takim razie z Twierdzenia 4.1 wiemy, że C = φ_{P′}(D).

W razie potrzeby można przemianować w γ, P′ i P zmienne typowe wyst_{}epuj _{}ace wolno w γ, a nie wyst_{}epuj _{}ace wolno w C tak, aby znalazły si_{}e one poza zasi_{}egiem φ. Z uzyskanej z dalszego rozumowania tezy, że dla przemianowanego P i γ, ślad elaboracji P w kontekście φ(D) równy jest φ(Clos_{C}γ), łatwo dostać tez_{}e dla oryginalnych P i γ.

Stosuj _{}ac hipotez_{}e indukcyjn _{}a do P′, D, γ i φ dostaj_{}e, że ślad elaboracji P′ w kontekście φ(D) równy jest φ(γ). Niech ta elaboracja daje podstawienie ϕ_{P′}. Z Twierdzenia 4.1 otrzymuj_{}e, że ślad elaboracji P w kontekście φ(D) równy jest Clos_{ϕ_{P′}(φ(D))}φ(γ). Ale można pokazać, że

Clos_{ϕ_{P′}(φ(D))}φ(γ) = Clos_{φ(φ_{P′}(D))}φ(γ) = Clos_{φ(C)}φ(γ)

Pierwsz _{}a z tych równości uzyskuje si_{}e przez żmudn _{}a indukcj_{}e po strukturze P′, korzystaj _{}ac z faktu że odpowiednie zmienne typowe znajduj _{}a si_{}e poza zasi_{}egiem φ (być może na skutek przemianowania zmiennych), druga wynika z tego, że C = φ_{P′}(D).

Pozostaje udowodnić, że

Clos_{φ(C)}φ(γ) = φ(Clos_{C}γ)

Dla uproszczenia założ_{}e do końca dowodu, iż w γ wyst_{}epuje dokładnie jedna typowa zmienna wolna — α. Łatwo to rozumowanie przenieść na przypadki z inn _{}a liczb _{}a zmiennych.

Rozpatrz_{}e nast_{}epuj _{}ace możliwości:

• α wyst_{}epuje wolno w kontekście C. Wtedy Clos_{C}γ = γ, a st _{}ad

φ(Clos_{C}γ) = φ(γ)

Z drugiej zaś strony jedyne zmienne wolne φ(γ) to zmienne wolne wyst_{}epuj _{}ace w φ(α), co wraz z faktem, iż w C wyst_{}epuje wolno α, czyli w φ(C) wyst_{}epuj _{}a wolno zmienne wolne termu φ(α), daje

Clos_{φ(C)}φ(γ) = φ(γ)

• α nie wyst_{}epuje wolno w kontekście C. Wtedy Clos_{C}γ = ∀α.γ a ponieważ ∀α.γ nie posiada zmiennych wolnych, dostaj_{}e

φ(Clos_{C}γ) = ∀α.γ

Z drugiej strony ponieważ α jest poza zasi_{}egiem φ, to φ(γ) = γ oraz φ(C) nie zawiera α, a st _{}ad

Clos_{φ(C)}φ(γ) = ∀α.γ

Teraz wreszcie możemy pokazać, w jaki sposób z poprawnych śladów elaboracji podprogramów można zbudować ślad elaboracji ich pary.

Twierdzenie 4.5. Niech program T ma postać (P, Q). Niech C b_{}edzie kontekstem w którym przeprowadzana jest elaboracja T. Niech φ_{P} b_{}edzie podstawieniem, wynikłym z elaboracji P jako cz_{}eści T, i niech γ_{P} b_{}edzie śladem tej elaboracji. (Zauważmy, że P jest elaborowane w kontekście C.) Niech φ_{Q} b_{}edzie podstawieniem, wynikłym z elaboracji Q jako cz_{}eści T, i niech γ_{Q} b_{}edzie śladem tej elaboracji.

Wtedy φ_{Q}(γ_{P}) · γ_{Q} jest śladem elaboracji T.

Dowód. Z Twierdzenia 4.3 wiemy, iż ślad elaboracji T w kontekście C równy jest γ̂ · γ_{Q}, gdzie γ̂ jest śladem elaboracji P w kontekście φ_{Q}(φ_{P} (C)).

Zastosujmy Twierdzenie 4.4 z φ = φ_{P} i D = C. Dostajemy, że śladem elaboracji P w kontekście φ_{P} (C) jest φ_{P} (γ_{P}). Ale ponieważ φ_{P} zawiera tylko te konkretyzacje typów, które s _{}a niezb_{}edne by udała si_{}e elaboracja P w C (porównaj rozdział 4.1.2), a γ_{P} jest śladem tej właśnie elaboracji, mamy φ_{P} (γ_{P}) = γ_{P}. A wi_{}ec ślad elaboracji P w kontekście φ_{P} (C) równy jest γ_{P}.

Jeśli teraz postawimy φ = φ_{Q} i D = φ_{P} (C) to ponownie spełnione zostan _{}a założenia Twierdzenia 4.4, i uzyskamy γ̂ = φ(γ_{P}) = φ_{Q}(γ_{P}).

Podobne twierdzenia można udowodnić dla wszystich postaci programów J _{}adra EML, w których składane s _{}a ślady i może wyst_{}epować zjawisko domykania niedoprecyzowanego śladu, wzgl_{}edem niegłównego kontekstu. Co wi_{}ecej, twierdzenia podobne do 4.4 i 4.5 można udowodnić również w przypadku j_{}ezyka Modułów, gdy rol_{}e podstawień spełniaj _{}a realizacje.

Wniosek 4.6. Zbierania śladów można dokonywać wraz z elaboracj _{}a, przy pomocy jedoprzebiegowego algorytmu.

Cz_{}eść III

Implementacja

W tej cz_{}eści wielokrotnie odwołuj_{}e si_{}e do kodu źródłowego systemu EML Kit. Staram si_{}e pokazywać przykładowy kod w postaci jak najmniej zmienionej i poci_{}etej. Jednocześnie zdaj_{}e sobie spraw_{}e, że nie jestem w stanie zast _{}apić narracj _{}a przeplatan _{}a przykładami, lektury pełnych źródeł i eksperymentów przy użyciu pracuj _{}acego systemu. Dlatego też w dodatku A podaj_{}e informacje na temat dost_{}epności najnowszego wydania systemu EML Kit, zawieraj _{}acego w szczególności ponad półtora megabajta kodu źródłowego.

5 Aksjomaty w sygnaturach

Elaboracja sygnatur zawieraj _{}acych aksjomaty zbudowana została na podstawie algorytmu naszkicowanego w rozdziale 3.1.5, korzystaj _{}ac z wniosków sformułowanych w rozdziale 3.1.6 i 3.3.4 oraz bazuj _{}ac na elaboracji sygnatur SML zaimplementowanej w systemie ML Kit.

Przypomn_{}e szkic algorytmu z rozdziału 3.1.5:

1. obedrzyj sigexp z aksjomatów dostaj _{}ac sigexp′,

2. dokonaj elaboracji sigexp′ dostaj _{}ac sygnatur_{}e główn _{}a (N′)S′ i ślad γ′,

3. sprawdź, że aksjomaty nie wymuszaj _{}a zrównania typów, ani uznania typu za równościowy w sigexp,

4. dokonaj elaboracji aksjomatów zgodnie z reguł _{}a 74.1, uzyskuj _{}ac ślady γ_{1}, …, γ_{n},

5. jeśli wszystko przebiegło poprawnie, wynikiem jest (N′)S′ i dodatkowo γ′ ze śladami γ_{1}, …, γ_{n} wstawionymi w odpowiednich miejscach.

Widać, że rezultatem kroków 1 i 2 ma być semantyczna sygnatura (N′)S′, główna dla sigexp′ oraz ślad γ′. Ze Spostrzeżenia 3.7 wiadomo, że przydatna byłaby również realizacja φ, b_{}ed _{}aca wynikiem elaboracji wykonanej w kroku 2.

Algorytm elaboracji sygnatur w systemie EML Kit musi być przygotowany na możliwość znalezienia w analizowanej przez siebie sygnaturze aksjomatów. Jeśli nie zaż _{}ada si_{}e inaczej, to napotykane aksjomaty s _{}a elaborowane w bież _{}acej bazie, a ewentualne bł_{}edy ich elaboracji s _{}a zapisywane w drzewie składni abstrakcyjnej i pod innymi wzgl_{}edami ignorowane. Dzi_{}eki temu mog_{}e uzyskać (N′)S′ oraz realizacj_{}e φ elaboruj _{}ac oryginalne sigexp zamiast jej obdartej wersji. Ponieważ ślad takiej elaboracji jest tworem sztucznym i nieprzydatnym, nie zachowam go, a zbieranie γ′ odłoż_{}e na później.

Dokonuje si_{}e to w pierwszym przebiegu algorytmu, którego wywołanie można wyróżnić w kodzie po tym, że dodatkowy parametr elaboracji ma

wartość FIRST_PASS:
fun elab_psigexp (B: Env.Basis, psigexp: IG.psigexp)
    : (Stat.Sig * OG.psigexp) =
  let
    val IG.PRINCIPpsigexp(i, sigexp) = psigexp
    val A = Env.mkAssembly B
    val NofB = Env.N_of_B B
    val (rea, _, S_first, _) =
        (StrId.backup_state();
        elab_sigexp'(B, sigexp, A, FIRST_PASS))
    val (_, rea1) = Stat.equality_principal(NofB, S_first)
    val (_, _, S, out_sigexp) =
        (StrId.restore_state();
        elab_sigexp'(B, sigexp, A, SECOND_PASS(rea1 oo rea)))
  in
    ... Stat.closeStr(NofB, S) ...
  end
   Historia i znaczenie StrId.backup_state oraz StrId.restore_state

pojawiaj _{}acych si_{}e powyżej, opisana jest w rozdziale 8. Znaczenie mkAssembly i wielu rozbudowanych poleceń znajduj _{}acych si_{}e w wykropkowanej cz_{}eści kodu, jest takie samo jak w przypadku elaboracji sygnatur SML, opisanej w dokumentacji systemu ML Kit [2].

Po pierwszym przebiegu tworzona jest realizacja, której aplikacja do sygnatury uczyni j _{}a równościowo główn _{}a (ang.: equality principal). Równościowa główność jest poj_{}eciem, które dla uproszczenia pomin_{}eliśmy w rozważaniach teoretycznych i do którego również tutaj nie b_{}edziemy już wi_{}ecej wracali, gdyż nie przeszkadza ono w poprawnej elaboracji aksjomatów, a jego implementacja przebiega identycznie jak w przypadku SML.

Teraz należy wykonać krok 3, czyli sprawdzić czy aksjomaty czegoś nie wymuszaj _{}a. Na mocy Twierdzenia 3.6 wystarczy w tym celu dokonać elaboracji aksjomatów w odpowiadaj _{}acych im bazach B_{e}. Najłatwiejszym sposobem, aby to osi _{}agn _{}ać jest elaboracja sigexp po raz drugi, z dodatkowym parametrem, którym jest otrzymana w pierwszym przebiegu realizacja φ. Kiedy podczas tej elaboracji napotykany jest aksjomat, jest on elaborowany w bież _{}acej bazie zmodyfikowanej realizacj _{}a φ. Ta baza jest, na mocy Spostrzeżenia 3.7, równa bazie B_{e} aksjomatu:

fun elab_spec (B: Env.Basis, spec: IG.spec, A: Env.Assembly, p : pass):
   (Stat.Realisation * Env.Assembly * Env.Env * OG.spec) =
  case spec of
  ...
   (* Axiom specification *)
  | IG.AXIOMspec(i, axdesc) =>
      let
        val (out_axdesc) =
          case p
            of FIRST_PASS => elab_axdesc(B, axdesc)
             | (SECOND_PASS(rea)) => elab_axdesc(rea onB B, axdesc)
      in
        (Stat.Id, Env.emptyA, Env.emptyE, OG.AXIOMspec(okConv i, out_axdesc))
      end

Podczas drugiego przebiegu elboracji sigexp nast_{}epuje zbieranie śladu, nazwijmy go γ, a w nim zbierane s _{}a również ślady γ_{1}, …, γ_{n} zgodnie z krokiem 4. Co wi_{}ecej, jak łatwo zobaczyć, γ równy jest śladowi γ′, z γ_{1}, …, γ_{n} wstawionymi w odpowiednich miejscach, co oznacza, że elaboracja została zakończona.

6 Ślady j_{}ezyka Modułów

W systemie EML Kit ślady s _{}a gromadzone w drzewie składni abstrakcyjnej programu. Każdy w_{}ezeł takiego drzewa zawiera pole, w którym przechowywane s _{}a dodatkowe informacje. W wypadku programów, które przeszły już proces elaboracji, typ tego pola ma nast_{}epuj _{}ac _{}a definicj_{}e:

datatype PostElabGrammarInfo =
  POST_ELAB_GRAMMAR_INFO of {preElabGrammarInfo: PreElabGrammarInfo,
                             errorInfo: ErrorInfo Option,
                             typeInfo: TypeInfo Option,
                             overloadingInfo: OverloadingInfo Option,
                             trace : Trace Option}

Przy czym pojawiaj _{}acy si_{}e tu i w innych miejscach typ Option, jest zdefiniowany nast_{}epuj _{}aco:

datatype 'a Option = None | Some of 'a

Ściśle mówi _{}ac, w w_{}ezłach nie ma prawdziwych śladów, czyli obiektów budowanych przy pomocy operacji właściwych dziedzinom postaci Tree(A) (patrz rozdział 4.2.2). Zamiast tego i w pewnym sensie równoważnie, w w_{}ezłach znajduj _{}a si_{}e komponenty śladów. W ten sposób ślad podprogramu, maj _{}acego swój korzeń w danym w_{}eźle, reprezentowany jest przez całe poddrzewo składni abstrakcyjnej, zaczynaj _{}ace si_{}e w tym w_{}eźle i zawieraj _{}ace składniki tego śladu.

Ślady j_{}ezyka Modułów EML składaj _{}a si_{}e ze śladów j_{}ezyka J _{}adra EML (tu oznaczonych TraceCOR — ich zbieraniu poświ_{}econy jest rozdział 7) oraz śladów prostych (SimTrace). Ponieważ nigdy nie zdarza si_{}e jednoczesne dodanie komponentu do śladu i zwi _{}azanie w nim nazw, zjawisko zwi _{}azywania nazw w śladach może być reprezentowane jako trzeci rodzaj składnika śladu

(BoundTrace):
datatype Trace =
    TRACE_COR of TraceCOR
  | SIM_TRACE of SimTrace
  | BOUND_TRACE of BoundTrace
and BoundTrace =
    BOUND of NameSet
and SimTrace =
    STRNAME of StrName
  | REA of Rea
  | VARENV of VarEnv
  | TYENV of TyEnv
  | ENV of Env

Dodawania śladów można teraz dokonywać przy pomocy prostych funkcji pomocniczych:

(* Auxiliary functions for trace collection *)
fun addTrace (tr : Trace.Trace) (i : PostElabGrammarInfo) =
    GrammarInfo.addPostElabTrace(i, tr)
fun addCoreTrace (tr : Trace.TraceCOR) (i : PostElabGrammarInfo) =
    addTrace (Trace.TRACE_COR(tr)) i
fun addSimTrace (sim : Trace.SimTrace) (i : PostElabGrammarInfo) =
    addTrace (Trace.SIM_TRACE(sim)) i
fun addBoundTrace (bound : Trace.BoundTrace) (i : PostElabGrammarInfo) =
    addTrace (Trace.BOUND_TRACE(bound)) i

Elaboracja sygnatur odbywa si_{}e w dwóch przebiegach, po to by poprawnie traktować aksjomaty (patrz rozdział 5). Mechanizmy, skonstruowane na potrzeby tej elaboracji, pozwalaj _{}a również bez dodatkowych wysiłków opanować niedeterminizm, przeszkadzaj _{}acy w zbieraniu śladów j_{}ezyka Modułów.

Poprawne musi być jedynie zbieranie śladów podczas drugiego przebiegu elaboracji. Ale wtedy właśnie dost_{}epna jest już wynikowa realizacja całego programu, dzi_{}eki której można ”zgadywać” ostateczn _{}a konkretyzacj_{}e pojawiaj _{}acych si_{}e obiektów semantycznych. Dzi_{}eki temu nie ma potrzeby uściślania zebranych uprzednio śladów, a do każdego komponentu aplikowana jest tylko jedna realizacja i tylko jeden raz.

Ilustruj _{}a to dwie reguły Semantyki Statycznej Modułów EML, które s _{}a źródłami niedetermizmu w wyborze własności podstruktur pojawiaj _{}acyh si_{}e w sygnaturach:

\frac{B ⊢ spec ⇒ E, γ}{B ⊢ sig spec end ⇒ (m, E), m · γ}  (63)

\frac{B(sigid)≥_{φ}S}{B ⊢ sigid ⇒ S, φ}  (64)

oraz implementacja kroku elaboracji odpowiadaj _{}acego tym regułom:

fun elab_sigexp' (B: Env.Basis, sigexp: IG.sigexp, A: Env.Assembly, p : pass):
(Stat.Realisation * Env.Assembly * Stat.Str * OG.sigexp) =
case sigexp of
(* Generative *)
IG.SIGsigexp(i, spec) =>
let
val (rea, A1, E, out_spec) = elab_spec(B, spec, A, p)
val m = Stat.freshStrName()
val S  = Stat.mkStr(m, E)
val A2 = A1 union Env.singleA_Str(S)
in
(rea, A2, S, OG.SIGsigexp(addSimTrace
 (Trace.STRNAME(case p
                  of FIRST_PASS => m
                   | (SECOND_PASS(rea1)) => M.onStrName rea1 m))
 (okConv i), out_spec))
end
(* Signature identifier *)
| IG.SIGIDsigexp(i, sigid) =>
case Env.lookup_sigid(B, sigid)
of Some sigma =>
     let
       val (S, A', rea) = Env.Sig_instance_for_traces sigma
     in
       (Stat.Id, A', S, OG.SIGIDsigexp(addSimTrace
        (Trace.REA(case p
                     of FIRST_PASS => rea
                      | (SECOND_PASS(rea1)) => rea1 oo rea))
        (okConv i), sigid))
     end
 | None => ... ErrorInfo.LOOKUP_SIGID sigid ...

7 Ślady j_{}ezyka J _{}adra

Z Wniosku 4.6 wynika, że zbierania śladów j_{}ezyka J _{}adra EML można dokonywać, dodaj _{}ac do bież _{}acych śladów nowe komponenty i ci _{}agle konkretyzuj _{}ac stare, poprzez aplikowanie podstawień.

Inn _{}a możliwości _{}a jest wstrzymanie si_{}e od poprawiania śladów podczas elaboracji, a zamiast tego zaaplikowanie końcowego podstawienia do śladu otrzymanego na końcu procesu. Aby dowieść, że jest to poprawne, potrzebne jest twierdzenie podobne do Lematu 3.3 z rozdziału 3.1.4. Dowód lematu nast_{}epuje poprzez indukcj_{}e po wszystkich regułach Semantyki Statycznej J _{}adra EML.

Rzecz _{}a, która wymaga ostrożności jest to, iż skoro wstrzymujemy si_{}e od konkretyzacji śladów, nie powinniśmy ich również za wcześnie domykać. W zwi _{}azku z tym implementacja śladów elaboracji J _{}adra EML zawiera dwie formy TraceScheme. Jedna z nich to lista zmiennych, reprezentuj _{}aca zmienne znajduj _{}ace si_{}e pod kwantyfikatorem. Druga to kontekst, jaki wyst_{}epował podczas elaboracji, gdy pojawiła si_{}e potrzeba domkni_{}ecia śladu, ale domkni_{}ecie zostało odłożone na później:

datatype Trace =
    TRACE of SchemeTrace Option * SimTrace Option
and SimTrace =
    TYPE of Type
  | ENV of Env
  | CONTEXTxTYPE of Context * Type
  | CONTEXTxENV of Context * Env
  | TYENV of TyEnv
  | VARENVxTYREA of VarEnv * TyRea
  | CONTEXTxTYNAME of Context * TyName
and SchemeTrace =
    SCHEME_C of Context
  | TYVARS of TyVar list

Zauważmy, że ponieważ czasami jednocześnie dodaje si_{}e komponent do śladu i domyka cały ślad, typ Trace nie może być sum _{}a rozł _{}aczn _{}a możliwych postaci komponentów śladu, jak było to w rozdziale 6.

Podczas zbierania śladów, każda napotkana sytuacja, w której potrzebne by było domkni_{}ecie śladu, powoduje umieszczenie bież _{}acego kontekstu w komponencie SchemeTrace. Natomiast po zebraniu całego śladu elaboracji, wykonywana jest operacja process_core_trace_and_tvs, która aplikuje wynikowe podstawienie elaboracji do każdego atomowego śladu, dokonuj _{}ac jednocześnie właściwego domykania na podstawie zgromadzonych kontekstów:

fun onScheme (S, SCHEME_C(C)) = SCHEME_C(Environments.onC (S, C))
| onScheme (S, TYVARS(_))   = Crash.impossible "CoreTrace.onScheme"
fun onScheme_opt (S, Some(scheme)) = Some(onScheme (S, scheme))
| onScheme_opt (S, None)          = None
fun onSim (S, TYPE(tau)) = TYPE(Environments.on (S, tau))
| onSim (S, ENV(E)) = ENV(Environments.onE (S, E))
| onSim (S, CONTEXTxTYPE(C, tau)) = CONTEXTxTYPE(Environments.onC (S, C),
                                                 Environments.on (S, tau))
| onSim (S, CONTEXTxENV(C, E)) = CONTEXTxENV(Environments.onC (S, C),
                                                 Environments.onE (S, E))
| onSim (S, TYENV(TE)) = TYENV(TE)
| onSim (S, VARENVxTYREA(VE, phi_Ty)) = VARENVxTYREA(VE, phi_Ty)
| onSim (S, CONTEXTxTYNAME(C, t)) = CONTEXTxTYNAME(Environments.onC (S, C), t)
fun onSim_opt (S, Some(sim)) = Some(onSim (S, sim))
| onSim_opt (S, None)      = None
fun onCoreTrace (S, TRACE(scheme_opt, sim_opt)) =
  TRACE(onScheme_opt (S, scheme_opt), onSim_opt (S, sim_opt))
fun tyvars_sim (TYPE(tau)) = Environments.tyvarsTy tau
| tyvars_sim (ENV(E)) = Environments.tyvarsE E
| tyvars_sim (CONTEXTxTYPE(C, tau)) = (Environments.tyvarsC C)
                                      @ (Environments.tyvarsTy tau)
| tyvars_sim (CONTEXTxENV(C, E)) = (Environments.tyvarsC C)
                                   @ (Environments.tyvarsE E)
| tyvars_sim (TYENV(TE)) = []
| tyvars_sim (VARENVxTYREA(VE, phi_Ty)) = []
| tyvars_sim (CONTEXTxTYNAME(C, t)) = Environments.tyvarsC C
fun tyvars_sim_opt (Some(sim)) = tyvars_sim sim
| tyvars_sim_opt None = []
fun process_core_trace_and_tvs (core_trace, tvs) S =
let
  val core_trace' as (TRACE(scheme_opt, sim_opt)) = onCoreTrace (S, core_trace)
  val sim_opt_tvs = tyvars_sim_opt sim_opt
  val free_tvs = sim_opt_tvs @ tvs
in
  case scheme_opt
    of None => (core_trace', free_tvs)
     | Some(SCHEME_C(C)) =>
        let val tvs_to_bind = minus (free_tvs, Environments.tyvarsC C)
        in (TRACE(Some(TYVARS(tvs_to_bind)), sim_opt),
            minus (free_tvs, tvs_to_bind))
        end
     | Some(TYVARS(_)) =>
        Crash.impossible "CoreTrace.process_core_trace_and_tvs"
end

8 Anegdota

Kiedy skończyłem kodowanie algorytmu elaboracji aksjomatów w sygnaturach, przez kilka dni byłem pewien, mogłem dowieść, że jest on poprawny — ale algorytm uparcie produkował dziwne i niewyjaśnialne rezultaty. Byłem nieco zirytowany. Jednak to, co uczyniło mnie naprawd_{}e złym, było odkrycie, że winowajc _{}a s _{}a efekty uboczne. Jestem ich fanatycznym przeciwnikiem i nie przyjmowałem do wiadomości, że autorzy tak eleganckiego systemu, jak ML Kit, mogli zniżyć si_{}e do ich stosowania. Tymczasem okazało si_{}e, że w systemie ML Kit, a co za tym idzie również w systemie EML Kit, efekty uboczne s _{}a używane. Mi_{}edzy innymi po to, aby uzyskiwać świeże nazwy typów i struktur podczas elaboracji sygnatur.

Rozwi _{}azałem problem w raczej brutalny sposób, nie przebieraj _{}ac w środkach, jak można zobaczyć w kodzie funkcji elab_psigexp powyżej oraz w odpowiedzialnym za szkody module poniżej:

functor Timestamp(): TIMESTAMP =
struct
  type stamp = int
  val r = ref 0
  fun new() = (r := !r + 1; !r)
  fun print i = "$" ^Int.string i
(* mikon#1.44 *)
  val backup = ref 0
  fun backup_state() = backup := !r
  fun restore_state() = r := !backup
(* end mikon#1.44 *)
end;

Cz_{}eść IV

Podsumowanie

Formalizm Extended ML został w 1994 roku opisany w swojej definicji [10]. Od tego czasu Extended ML wykorzystywany jest do tworzenia oprogramowania i do celów edukacyjnych. Trwaj _{}a prace nad teori _{}a dowodu EML. Rozwijane s _{}a prototypowe narz_{}edzia wspomagaj _{}ace proces konstrukcji oprogramowania. Ci _{}agle ulepszana jest i poprawiana sama definicja formalizmu, w czym autor tej pracy chlubi si_{}e mieć swój malutki udział.

Od samego pocz _{}atku wyraźne jest znaczenie analizy statycznej EML. Zdefiniowana ona została w cz_{}eści definicji zwanej Semantyk _{}a Statyczn _{}a. Jej wst_{}epne implementacje były jednym z najważniejszych elementów kolejnych wersji systemu EML Kit, stanowi _{}ac o jego użyteczności w praktycznych zastosowaniach. Pobieżny opis ostatecznej implementacji zawartej w systemie EML Kit 1.0, wraz z dokładnym omówieniem niektórych szczegółów, został zamieszczony w raporcie na temat systemu EML Kit [4]. Ponadto Stefan Kahrs poświ_{}ecił prac_{}e [9] opisowi różnic mi_{}edzy analiz _{}a statyczn _{}a Extended ML i analiz _{}a statyczn _{}a Standard ML. A ta z kolei rozpatrywana była w wielu pozycjach, na przykład w [15] czy w [14].

Bież _{}aca aktywność naukowa wokół Extended ML skupiona jest na Semantyce Weryfikacyjnej EML i zagadnieniach, które można by nazwać jej ”implementacj _{}a”. Z kolei Semantyka Weryfikacyjna cz_{}esto odwołuje si_{}e do Semantyki Statycznej, na przykład w celu wyrażenia własności posiadania typu. Co wi_{}ecej, Semantyka Statyczna jest obci _{}ażona odpowiedzialności _{}a za zbieranie różnorakich informacji na potrzeby Semantyki Weryfikacyjnej. Wszystko to sprawia, iż niezb_{}edna jest pełna i godna zaufania implementacja Semantyki Statycznej EML, co stało si_{}e motywacj _{}a do opisanych tu przedsi_{}ewzi_{}eć.

Niniejsz _{}a prac _{}a mam nadziej_{}e zamkn _{}ać temat własności analizy statycznej EML i metod jej przeprowadzania. W pracy tej zdaj_{}e również spraw_{}e z najciekawszych aspektów jej implementacji w ramach systemu EML Kit. Szczególn _{}a uwag _{}a obdarzyłem dwa problemy, powstaj _{}ace podczas sprawdzania poprawności typowej programów napisanych w j_{}ezyku Extended ML. Pierwszy problem to analiza statyczna sygnatur, w których mog _{}a jednocześnie wyst_{}epować aksjomaty i postulaty równości typów. Drugi to zbieranie śladów podczas analizy statycznej. Wskazałem źródła groźnych bł_{}edów, jakie mog _{}a być popełnione jeśli te problemy nie s _{}a potraktowane z wystarczaj _{}ac _{}a ostrożności _{}a. Na tym tle naszkicowałem poprawne rozwi _{}azania, wspominaj _{}ac również o pewnych ich wariantach. Udowodniłem także szereg własności Semantyki Statycznej EML, które potem posłużyły mi do dowodu poprawności podanych algorytmów. Na końcu przedstawiłem rzeczywist _{}a implementacj_{}e opisanych rozwi _{}azań, w tej postaci w jakiej jest ona cz_{}eści _{}a systemu EML Kit.

Podzi_{}ekowania

Szczególnie serdecznie chciałbym podzi_{}ekować Andrzejowi Tarleckiemu, mojemu promotorowi.

Pozostałym autorom Extended ML: Stefanowi Kahrsowi i Donowi Sannelli, jestem wdzi_{}eczny za życzliw _{}a uwag_{}e i czas jaki mi poświ_{}ecili. Z wdzi_{}eczności _{}a pozdrawiam przyjaciół, z którymi wspólnie pracowałem nad systemem EML Kit: Marcina Jurdzińskiego, Sławomira Leszczyńskiego, Roberta Marona i Aleksego Schuberta. Za dobre słowo dzi_{}ekuj_{}e Marcinowi Benke, Sławomirowi Białeckiemu, Sławomirowi Lasocie i Michałowi Grabowskiemu.

Dodatki

A System EML Kit

EML Kit jest dost_{}epny w sieci Internet. Poza wydaniem kodu źródłowego systemu EML Kit wersji 1.0, istnieje również wydanie zawieraj _{}ace binaria dla systemu Solaris na architekturze Sun SPARC, oraz wydanie zawieraj _{}ace binaria dla systemu Linux na architekture i386.

Wszystkie te zestawy s _{}a dost_{}epne przez anonimowe ftp z:

ftp://zls.mimuw.edu.pl/pub/mikon/EMLKit

Można je również znaleźć na stronie domowej WWW systemu EML Kit:

http://zls.mimuw.edu.pl/~mikon/ftp/EMLKit/README.html

EML Kit ma nast_{}epuj _{}acy copyright:

Copyright (C) 1993 Edinburgh and Copenhagen Universities: for the ML Kit Copyright (C) 1996, 1997 Marcin Jurdziński, Mikołaj Konarski, Sławomir Leszczyński i Aleksy Schubert

EML Kit został wydany na warunkach opisanych w licencji GNU GPL, co wyjaśniaj _{}a i przypiecz_{}etowuj _{}a nast_{}epuj _{}ace informacje w j_{}ezyku angielskim zał _{}aczane do każdego wydania systemu:

The EML Kit is free software; you can redistribute it and/or modify it under the terms of the GNU General Public License as published by the Free Software Foundation; either version 2 of the License, or (at your option) any later version.

The EML Kit is distributed in the hope that it will be useful, but WITHOUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR A PAR-TICULAR PURPOSE. See the GNU General Public License for more details.

Autorzy systemu EML Kit s _{}a wdzi_{}eczni za wszelk _{}a pomoc. Prace nad systemem EML Kit były cz_{}eściowo wspierane przez nast_{}epuj _{}ace granty KBN (Komitetu Badań Naukowych):

• ”Formal Methods of Software Development”

     http://wwwat.mimuw.edu.pl/~tarlecki/kbn93grant/index.html

• ”Logical Aspects of Software Specification and Development Methods”

     http://wwwat.mimuw.edu.pl/~tarlecki/kbn96grant/index.html

B Obiekty semantyczne

Dziedziny prostych obiektów semantycznych Semantyki Statycznej J _{}adra Extended ML, przestawione s _{}a w Tabeli 1. Dziedziny te: TyVar, TyName i StrName, to dowolne nieskończone zbiory. Ponadto każdy t ∈ TyName posiada arność k ≥ 0, a klasa nazw typów o arności k znaczana jest TyName^{(k)}.

α lub tyvar ∈ TyVar zmienne typowe
t ∈ TyName  nazwy typów
m ∈ StrName nazwy struktur

Tabela 1: Proste obiekty semantyczne

Dziedziny złożonych obiektów semantycznych Semantyki Statycznej J _{}adra EML, przestawione s _{}a w Tabeli 2.

Gdy A i B s _{}a zbiorami, Fin A oznacza zbiór skończonych podzbiorów A, zaś A →^{fin} B oznacza zbiór skończonych odwzorowań (cz_{}eściowych funkcji o skończonej dziedzinie) z A do B.

Dla dowolnej dziedziny obiektów semantycznych A definiujemy Tree(A) jako zbiór skończonych binarnych drzew o elementach z A. Innymi słowy Tree(A) jest najmniejszym rozwi _{}azaniem równania dziedzinowego

Tree(A) = {ϵ} ⊎ A ⊎ {x · y | x, y ∈ Tree(A)}

Operacja ⊎ oznacza sum_{}e rozł _{}aczn _{}a dziedzin. Zakładamy, że wszystkie definiowane dziedziny s _{}a rozł _{}aczne.

τ ∈ Type = TyVar ⊎ RecType ⊎ FunType ⊎ ConsType
(τ_{1}, ···, τ_{k}) lub τ^{(k)} ∈ Type^{k}
(α_{1}, ···, α_{k}) lub α^{(k)} ∈ TyVar^{k}
ϱ ∈ RecType = Lab →^{fin} Type
τ → τ′ ∈ FunType = Type × Type

ConsType = ⊎_{k≥0}ConsType^{(k)}

τ^{(k)}t ∈ ConsType^{(k)} = Type^{k} × TyName^{(k)}
θ lub Λα^{(k)}.τ ∈ TypeFcn = ⊎_{k≥0}TyVar^{k} × Type
σ lub ∀α^{(k)}.τ ∈ TypeScheme = ⊎_{k≥0}TyVar^{k} × Type
S lub (m, E) ∈ Str = StrName × Env
(θ, CE) ∈ TyStr = TypeFcn × ConEnv
SE ∈ StrEnv = StrId →^{fin} Str
TE ∈ TyEnv = TyCon →^{fin} TyStr
CE ∈ ConEnv = Id →^{fin} TypeScheme
VE ∈ VarEnv = Id →^{fin} TypeScheme
E lub (SE, TE, VE) ∈ Env = StrEnv × TyEnv × VarEnv
T ∈ TyNameSet = Fin(TyName)
U ∈ TyVarSet = Fin(TyVar)
C lub T, U, E ∈ Context = TyNameSet × TyVarSet × Env
φ_{Ty} ∈ TyRea = TyName → TypeFcn
γ ∈ Trace = Tree(SimTrace ⊎ TraceScheme)

SimTrace = Type ⊎ Env ⊎ (Context × Type) ⊎ (Context × Env) ⊎ (Context × TyName) ⊎ TyEnv ⊎ (VarEnv × TyRea)

TraceScheme = ⊎_{k≥0}TraceScheme^{(k)}

∀α^{(k)}.γ ∈ TraceScheme^{(k)} = TyVar^{k} × Trace

Tabela 2: Złożone obiekty semantyczne

Obiekty semantyczne Semantyki Statycznej Modułów EML to obiekty semantyczne Semantyki Statycznej J _{}adra EML, oraz dodatkowe obiekty semantyczne przestawione w Tabeli 3.

M ∈ StrNameSet = Fin(StrName)
N lub (M, T) ∈ NameSet = StrNameSet × TyNameSet
Σ lub (N)S ∈ Sig = NameSet × Str
Φ lub (N)(S, (N′)S′) ∈ FunSig = NameSet × (Str × Sig)
G ∈ SigEnv = SigId →^{fin} Sig
F ∈ FunEnv = FunId →^{fin} FunSig
B lub N, F, G, E ∈ Basis = NameSet × FunEnv × SigEnv × Env
φ_{Str} ∈ StrRea = StrName → StrName
φ lub (φ_{Ty}, φ_{Str}) ∈ Rea = TyRea × StrRea
γ ∈ Trace = Tree(Trace_{COR} ⊎ SimTrace ⊎ BoundTrace)
(N)γ ∈ BoundTrace = NameSet × Trace

SimTrace = StrName ⊎ Rea ⊎ VarEnv ⊎ TyEnv ⊎ Env

Tabela 3: Dalsze złożone obiekty semantyczne

Bibliografia

[1] H. P. Barendregt. The Lambda Calculus, its Syntax and Semantics. 2nd edition, North Holland (1984).

[2] L. Birkedal, N. Rothwell, M. Tofte and D. N. Turner. The ML Kit, Version 1. (1993).

[3] L. Damas and R. Milner. Principal type schemes for functional programs. Proc. 9th ACM Symposium on Principles of Programming Languages, pp. 207–212. ACM, New York (1982).

[4] M. Jurdziński, M. Konarski, A. Schubert. The EML Kit, Version 1. Technical Report TR 96-04 (225), Institute of Informatics, Warsaw University (1996).

[5] J. Hannan. Extended natural semantics. Journal of Functional Programming, 3(2), 123–152 (1993).

[6] R. Harper. Introduction to Standard ML. Report ECS-LFCS-86-14, Univ. of Edinburgh (1986).

[7] S. Kahrs. Mistakes and ambiguities in the definition of Standard ML. Report ECS-LFCS-93-257, Univ. of Edinburgh (1993).

[8] S. Kahrs. Mistakes and ambiguities in the definition of Standard ML – Addenda. Univ. of Edinburgh (1995).

[9] S. Kahrs. On the Static Analysis of Extended ML. Univ. of Edinburgh (1994).

[10] S. Kahrs, D. Sannella and A. Tarlecki. The Definition of Extended ML. Report ECS-LFCS-94-300, Univ. of Edinburgh (1994).

[11] S. Kahrs, D. Sannella and A. Tarlecki. The Definition of Extended ML, Version 1.15 + 0.2i.

[12] S. Kahrs and D. Sannella and A. Tarlecki. The semantics of Extended ML: a gentle introduction. Proc. Workshop on Semantics of Specification Languages, Utrecht, 1993. Springer Workshops in Computing, 186–215 (1994).

[13] X. Leroy. Manifest types, modules and separate compilation. In: Proc. 21st ACM Symposium on Principles of Programming Languages, Portland. ACM (1994).

[14] X. Leroy. Polymorphic typing of an algorithmic language. Research report 1778, INRIA (1992).

[15] R. Milner and M. Tofte. Commentary on Standard ML. MIT Press (1991).

[16] R. Milner, M. Tofte and R. Harper. The Definition of Standard ML. MIT Press (1990).

[17] C. Reade. Elements of functional programming. Addison-Wesley (1989).

[18] D. Sannella and A. Tarlecki. Essential concepts of algebraic specification and program development. Fundamental Aspects of Computing, to appear.

[19] D. Sannella and A. Tarlecki. Extended ML: past, present and future. Proc. 7th Workshop on Specification of Abstract Data Types, Wusterhausen. Springer LNCS 534, 297–322 (1991).

[20] D. Sannella and M. Wirsing. Specification Languages. In: Algebraic Foundations of Systems Specifications (E. Astesiano, H.-J. Kreowski and B. Krieg-Brückner, editors). Chapman and Hall, to appear.

[21] M. Wirsing. Algebraic specification. In: Handbook of Theoretical Computer Science, Vol. B (J. van Leeuwen, ed.), 675-788. Elsevier and MIT Press (1990).