Skip to content

S
softlab-thesis
Commit 18439d4d authored by Achilles Benetopoulos's avatar Achilles Benetopoulos
Browse files
Options

Update theoretical chapter

parent 220d6177
Show whitespace changes
Inline Side-by-side
Showing with 203 additions and 43 deletions
thesis.bib
View file @ 18439d4d
...@@ -101,3 +101,105 @@ ...@@ -101,3 +101,105 @@
isbn = {0262162288}, isbn = {0262162288},
publisher = {The MIT Press} publisher = {The MIT Press}
} }
@inproceedings{fowler-erlang,
author = {Simon Fowler},
title = {An Erlang Implementation of Multiparty Session Actors},
booktitle = {Proceedings 9th Interaction and Concurrency Experience, {ICE} 2016,
Heraklion, Greece, 8-9 June 2016.},
pages = {36--50},
year = {2016},
crossref = {DBLP:journals/corr/BartolettiHKV16},
url = {https://doi.org/10.4204/EPTCS.223.3},
doi = {10.4204/EPTCS.223.3},
timestamp = {Fri, 30 Nov 2018 13:24:58 +0100},
biburl = {https://dblp.org/rec/bib/journals/corr/Fowler16},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{spy,
author = {Neykova, Rumyana and Yoshida, Nobuko and Hu, Raymond},
year = {2013},
month = {09},
pages = {358-363},
title = {SPY: Local Verification of Global Protocols},
doi = {10.1007/978-3-642-40787-1_25}
}
@inproceedings{nielson-tes,
title={Type and Effect Systems},
author={Flemming Nielson and Hanne Riis Nielson},
booktitle={Correct System Design},
year={1999}
}
@inproceedings{polymorphic-binding,
author = {Henglein, Fritz and Mossin, Christian},
title = {Polymorphic Binding-Time Analysis},
booktitle = {Proceedings of the 5th European Symposium on Programming: Programming Languages and Systems},
series = {ESOP '94},
year = {1994},
isbn = {3-540-57880-3},
pages = {287--301},
numpages = {15},
url = {http://dl.acm.org/citation.cfm?id=645390.651420},
acmid = {651420},
publisher = {Springer-Verlag},
address = {Berlin, Heidelberg},
}
@article{Solberg_1995,
title={Annotated Type Systems for Program Analysis},
volume={24},
url={https://tidsskrift.dk/daimipb/article/view/7026},
DOI={10.7146/dpb.v24i498.7026},
number={498},
journal={DAIMI Report Series},
author={Solberg, Kirsten},
year={1995},
month={Nov.}
}
@inproceedings{Takeuchi94aninteraction-based,
author = {Kaku Takeuchi and Kohei Honda and Makoto Kubo},
title = {An Interaction-based Language and its Typing System},
booktitle = {In PARLE’94, volume 817 of LNCS},
year = {1994},
pages = {398--413},
publisher = {Springer-Verlag}
}
@inproceedings{language-primitives-honda,
author = {Honda, Kohei and Vasconcelos, Vasco Thudichum and Kubo, Makoto},
title = {Language Primitives and Type Discipline for Structured Communication-Based Programming},
booktitle = {Proceedings of the 7th European Symposium on Programming: Programming Languages and Systems},
series = {ESOP '98},
year = {1998},
isbn = {3-540-64302-8},
pages = {122--138},
numpages = {17},
url = {http://dl.acm.org/citation.cfm?id=645392.651876},
acmid = {651876},
publisher = {Springer-Verlag},
address = {London, UK, UK},
}
@article{multiparty-async,
author = {Honda, Kohei and Yoshida, Nobuko and Carbone, Marco},
title = {Multiparty Asynchronous Session Types},
journal = {J. ACM},
issue_date = {March 2016},
volume = {63},
number = {1},
month = mar,
year = {2016},
issn = {0004-5411},
pages = {9:1--9:67},
articleno = {9},
numpages = {67},
url = {http://doi.acm.org/10.1145/2827695},
doi = {10.1145/2827695},
acmid = {2827695},
publisher = {ACM},
address = {New York, NY, USA},
}
thesis.tex
View file @ 18439d4d
...@@ -134,7 +134,7 @@ Programming languages, Session Types, Type systems, Effect Systems, Concurrency. ...@@ -134,7 +134,7 @@ Programming languages, Session Types, Type systems, Effect Systems, Concurrency.
%%% Various tables %%% Various tables
\tableofcontents \tableofcontents
\listoftables %%\listoftables
\listoffigures \listoffigures
%%% Main part of the book %%% Main part of the book
...@@ -174,7 +174,7 @@ Programming languages, Session Types, Type systems, Effect Systems, Concurrency. ...@@ -174,7 +174,7 @@ Programming languages, Session Types, Type systems, Effect Systems, Concurrency.
η οποία παρέχει ισχυρούς μηχανισμούς ταυτοχρονισμού. η οποία παρέχει ισχυρούς μηχανισμούς ταυτοχρονισμού.
Στη βιβλιογραφία υπάρχει ένας αριθμός από υλοποιήσεις μηχανισμών χρόνου εκτέλεσης για την παρακολούθηση της επικοινωνίας μεταξύ διεργασιών Στη βιβλιογραφία υπάρχει ένας αριθμός από υλοποιήσεις μηχανισμών χρόνου εκτέλεσης για την παρακολούθηση της επικοινωνίας μεταξύ διεργασιών
σε γλώσσες με δυναμικό σύστημα τύπων όπως η Erlang [reference to Python's SPY, reference to Fowler's implementation]. Στη βάση τους, όλες χτίζουν σε γλώσσες με δυναμικό σύστημα τύπων όπως η Erlang \cite{spy, fowler-erlang}. Στη βάση τους, όλες χτίζουν
πάνω στη γλώσσα Scribble, η οποία είναι μια DSL για την περιγραφή πρωτοκόλλων πάνω στη γλώσσα Scribble, η οποία είναι μια DSL για την περιγραφή πρωτοκόλλων
επικοινωνίας. Στη δική μας δουλειά, επιχειρούμε να κατασκευάσουμε ένα σύστημα στατικής ανάλυσης, το οποίο μπορεί να: επικοινωνίας. Στη δική μας δουλειά, επιχειρούμε να κατασκευάσουμε ένα σύστημα στατικής ανάλυσης, το οποίο μπορεί να:
\begin{itemize} \begin{itemize}
...@@ -201,7 +201,7 @@ Programming languages, Session Types, Type systems, Effect Systems, Concurrency. ...@@ -201,7 +201,7 @@ Programming languages, Session Types, Type systems, Effect Systems, Concurrency.
σχετικά απλουστευμένα προγράμματα, τα οποία είναι τυποποιημένα στη σχετική βιβλιογραφία, αλλά και παραδείγματα σχετικά απλουστευμένα προγράμματα, τα οποία είναι τυποποιημένα στη σχετική βιβλιογραφία, αλλά και παραδείγματα
προσαρμοσμένα στο να αναδείξουν τα προτερήματα της υλοποίησής μας. προσαρμοσμένα στο να αναδείξουν τα προτερήματα της υλοποίησής μας.
Τέλος, στο κεφάλαιο 7 προσφέρουμε μερικά συμπεράσματα που προέκυψαν από την υλοποίηση του συστήματος αυτού, αλλά και τα Τέλος, στο κεφάλαιο 6 προσφέρουμε μερικά συμπεράσματα που προέκυψαν από την υλοποίηση του συστήματος αυτού, αλλά και τα
πειράματά μας. Επιπλέον, εκθέτουμε μερικές ιδέες για μελλοντική δουλειά πάνω στο συγκεκριμένο αντικείμενο. πειράματά μας. Επιπλέον, εκθέτουμε μερικές ιδέες για μελλοντική δουλειά πάνω στο συγκεκριμένο αντικείμενο.
\setlength{\parskip}{0em} \setlength{\parskip}{0em}
...@@ -343,7 +343,7 @@ $otp/lib/compiler/src/core\_parse.hrl$. ...@@ -343,7 +343,7 @@ $otp/lib/compiler/src/core\_parse.hrl$.
\chapter{Συστήματα τύπων και επιδράσεων} \chapter{Συστήματα τύπων και επιδράσεων}
Πολλές γλώσσες προγραμματισμού υλοποιούν ένα στατικό σύστημα τύπων, προκειμένου να εγγυηθούν ότι τελεστές εφαρμόζονται μόνο σε Πολλές γλώσσες προγραμματισμού υλοποιούν ένα στατικό σύστημα τύπων, προκειμένου να εγγυηθούν ότι τελεστές εφαρμόζονται μόνο σε
τελεσταίους της κατάλληλης μορφής, δηλαδή του κατάλληλου είδους. Για παράδειγμα, ένα κλασσικό σύστημα τύπων θα απέρριπτε τελεσταίους της κατάλληλης μορφής, δηλαδή του κατάλληλου είδους \cite{types-and-prog-langs, advanced-types-and-prog-langs}. Για παράδειγμα, ένα κλασσικό σύστημα τύπων θα απέρριπτε
το πρόγραμμα 3.1 (γραμμένο σε μια υποθετική γλώσσα), καθώς η πράξη της αφαίρεσης ($-$), δεν έχει νόημα όταν εφαρμόζεται το πρόγραμμα 3.1 (γραμμένο σε μια υποθετική γλώσσα), καθώς η πράξη της αφαίρεσης ($-$), δεν έχει νόημα όταν εφαρμόζεται
σε μια συμβολοσειρά και έναν αριθμό (υποθέτουμε ότι η γλώσσα δεν παρέχει τη δυνατότητα υπερφόρτωσης τελεστών). σε μια συμβολοσειρά και έναν αριθμό (υποθέτουμε ότι η γλώσσα δεν παρέχει τη δυνατότητα υπερφόρτωσης τελεστών).
...@@ -386,7 +386,7 @@ $otp/lib/compiler/src/core\_parse.hrl$. ...@@ -386,7 +386,7 @@ $otp/lib/compiler/src/core\_parse.hrl$.
%FIXME annotations <-> ετικετών %FIXME annotations <-> ετικετών
\section{Συστήματα τύπων με ετικέτες} \section{Συστήματα τύπων με ετικέτες}
Μια προσέγγιση για την επέκταση της εκφραστικότητας ενός συστήματος τύπων είναι η προσθήκη ετικετών στους τύπους με Μια προσέγγιση για την επέκταση της εκφραστικότητας ενός συστήματος τύπων είναι η προσθήκη ετικετών στους τύπους με
αποτέλεσμα την παραμετροποίησή τους. Στόχος αυτής της επέκτασης είναι το να καταστεί εφικτό ένα σύνολο στατικών αναλύσεων, αποτέλεσμα την παραμετροποίησή τους \cite{Solberg_1995}. Στόχος αυτής της επέκτασης είναι το να καταστεί εφικτό ένα σύνολο στατικών αναλύσεων,
όπως: όπως:
\begin{itemize} \begin{itemize}
% FIXME bind-time <-> χρονος δεσίματος % FIXME bind-time <-> χρονος δεσίματος
...@@ -407,7 +407,7 @@ $otp/lib/compiler/src/core\_parse.hrl$. ...@@ -407,7 +407,7 @@ $otp/lib/compiler/src/core\_parse.hrl$.
\section{Συστήματα τύπων και επιδράσεων} \section{Συστήματα τύπων και επιδράσεων}
Ο στόχος της προσθήκης πληροφορίας επιδράσεων στα κλασσικά συστήματα τύπων είναι η επέκτασή τους ώστε να εκφράζουν Ο στόχος της προσθήκης πληροφορίας επιδράσεων στα κλασσικά συστήματα τύπων είναι η επέκτασή τους ώστε να εκφράζουν
επιπλέον ιδιότητες που προκύπτουν από τους σημασιολογικούς κανόνες ενός προγράμματος. επιπλέον ιδιότητες που προκύπτουν από τους σημασιολογικούς κανόνες ενός προγράμματος \cite{nielson-tes, polymorphic-binding}.
Τα συστήματα τύπων και επιδράσεων αποτελούν ουσιαστικά μια παραλλαγή των συστημάτων τύπων με ετικέτες στα οποία Τα συστήματα τύπων και επιδράσεων αποτελούν ουσιαστικά μια παραλλαγή των συστημάτων τύπων με ετικέτες στα οποία
αναφερθήκαμε παραπάνω, αλλά με μια διαφορά: οι ετικέτες σε αυτά τα συστήματα τύπων περιέχουν πληροφορία σχετικά με την αναφερθήκαμε παραπάνω, αλλά με μια διαφορά: οι ετικέτες σε αυτά τα συστήματα τύπων περιέχουν πληροφορία σχετικά με την
...@@ -425,9 +425,22 @@ $otp/lib/compiler/src/core\_parse.hrl$. ...@@ -425,9 +425,22 @@ $otp/lib/compiler/src/core\_parse.hrl$.
σκοπός μιας συνεδρίας είναι το να εγκαθιδρύσει το θέμα της επικοινωνίας, αλλα και το περιεχόμενο και την κατεύθυνση των σκοπός μιας συνεδρίας είναι το να εγκαθιδρύσει το θέμα της επικοινωνίας, αλλα και το περιεχόμενο και την κατεύθυνση των
μηνυμάτων που ανταλλάσουν οι πράκτορες της επικοινωνίας. μηνυμάτων που ανταλλάσουν οι πράκτορες της επικοινωνίας.
Στα [] έχουμε τους πρώτους φορμαλισμούς της επικοινωνίας παράλληλων διεργασιών σε όρους ενός κλασσικού συστήματος τύπων. Οι τύποι συνεδρίας είναι περιγραφές πρωτοκόλλων επικοινωνίας, που διαγράφουν τις επιτρεπόμενες ακολουθίες μηνυμάτων,
μαζί με τους τύπους των μηνυμάτων που ανταλλάσσονται ανάμεσα στους συμμετέχοντες. Μας παρέχουν εγγυήσεις σχετικά με
χαρακτηριστικά της επικοινωνίας, όπως την ποιότητα και την ασφάλειά τους. Ένα καλώς ορισμένο ως προς τους τύπους
πρόγραμμα αποκλείεται να στείλει ή να λάβει μήνυμα του λάθος τύπου.
Στο [] έχουμε μια πρώτη απόπειρα φορμαλισμού της επικοινωνίας παράλληλων διεργασιών, με την εισαγωγή των θεμελιωδών Οι τύποι συνεδρίας μοντελοποιούν την επικοινωνία μεταξύ δύο ή περισσότερων οντοτήτων. Ορίζονται ως μια σειρά από
λειτουργίες εισόδου/εξόδου, οι οποίες περιγράφουν τους τύπους των μηνυμάτων που ανταλλάσσονται. Στη συγκεκριμένη
εργασία, απασχολούμαστε μόνο με συνεδριές μεταξύ δύο συμμετεχόντων.
% Οι τύποι συνεδρίας βασίζονται στην π-άλγεβρα, την οποία εισήγαγε ο Robert Milner βασιζόμενος στη δουλειά των
% Οι τύποι συνεδρίας βασίζονται στην π-άλγεβρα, την οποία εισήγαγε ο Robert Milner to 1992. H π-αλγεβρα είναι μια άλγεβρα
% διεργασιών, δηλαδή ένας αυστηρός τρόπος περιγραφής/μοντελοποίησης ενός ταυτόχρονου συστήματος. Η σημαντική ιδιότητα της
% π-αλγεβρας του Milner είναι ότι επιτρέπει τη μεταφορά ονομάτων καναλιών μέσα από τα ίδια τα κανάλια, το οποίο την
% καθιστά ικανή να περιγράφει συστήματα των οποίων η διαμόρφωση αλλάζει σε βάθος χρόνου.
Στο \cite{Takeuchi94aninteraction-based} έχουμε μια πρώτη απόπειρα φορμαλισμού της επικοινωνίας παράλληλων διεργασιών, με την εισαγωγή των θεμελιωδών
λειτουργιών επικοινωνίας: λειτουργιών επικοινωνίας:
\begin{itemize} \begin{itemize}
\item $k!x$, δηλαδή αποστολή μιας τιμής $x$ μέσω του καναλιού $k$. \item $k!x$, δηλαδή αποστολή μιας τιμής $x$ μέσω του καναλιού $k$.
...@@ -466,12 +479,26 @@ To κανάλι επικοινωνίας $k$ δημιουργείται ρητά ...@@ -466,12 +479,26 @@ To κανάλι επικοινωνίας $k$ δημιουργείται ρητά
μόνο ως προς το είδος της πράξης (μια διεργασία να στέλνει, ενώ η άλλη περιμένει να λάβει μια τιμή από το κανάλι). μόνο ως προς το είδος της πράξης (μια διεργασία να στέλνει, ενώ η άλλη περιμένει να λάβει μια τιμή από το κανάλι).
%% TODO maybe talk about other aspects of session type research? %% TODO maybe talk about other aspects of session type research?
Ακολούθως στο \cite{language-primitives-honda} έχουμε μια επέκταση της δουλειάς του
\cite{Takeuchi94aninteraction-based}, στην οποία πλέον επιτρέπεται η περιγραφή αναδρομικών τύπων συνεδρίας, πράγμα που
επεκτείνει την πρακτική εφαρμογή της θεωρίας των τύπων συνεδριών.
Μέχρι πρόσφατα, η έρευνα επικεντρωνόταν σε τύπους συνεδριών δύο συμμετεχόντων. Αυτές ήταν σε θέση να περιγράφουν
επικοινωνία με πολλαπλούς συμμετέχοντες, όμως τα επιμέρους πρωτόκολλα έπρεπε να αφορούν δύο συγκεκριμένους συμμετέχοντες
και να είναι ανεξάρτητα μεταξύ τους. Συνέπεια αυτού είναι ότι τα συστήματα αυτά δε μπορούν να "περιορίσουν" ή να
διασφαλίσουν τη σειρά με την οποία ανταλλάσονται μηνύματα σε δύο διαφορετικά πρωτόκολλα.
%% FIXME I mean, really
Ο πιο πρόσφατος φορμαλισμός των τύπων συνεδριών κάνει διαχωρισμό ανάμεσα σε μια καθολική και μια τοπική περιγραφή της Στο \cite{multiparty-async}, οι Honda et al αναπτύσσουν ένα σύστημα για να κάνουν reason για συνεδρίες πολλαπλών
επικοινωνίας. Στο [] αναλύονται δύο άλγεβρες βασισμένες σε μια επέκταση της π-άλγεβρας και των τύπων συνεδριών: συμμετεχόντων.
% Αυτό γίνεται με το να καθορίζεται ένας "καθολικός" τύπος που περιγράφει την επικοινωνία που
% διαδραματίζεται στο σύστημα. Ακολούθως, αυτός ο τύπος \it{προβάλλεται} στους επιμέρους συμμετέχοντες σαν ένας κλασσικός
% τύπος συνεδρίας "από τη δική τους σκοπιά".
Σε αυτήν τη δημοσίευση αναλύονται δύο άλγεβρες βασισμένες σε μια επέκταση της π-άλγεβρας και των τύπων συνεδριών:
\begin{itemize} \begin{itemize}
\item Η πρώτη είναι η άλγεβρα που αποτελεί το φορμαλισμό της καθολικής περιγραφής. Σε αυτήν μπορεί να περιγραφεί η \item Η πρώτη είναι η άλγεβρα που αποτελεί το φορμαλισμό της καθολικής περιγραφής της επικοινωνίας.
Σε αυτήν μπορεί να περιγραφεί η
αλληλεπίδραση των πρακτόρων της επικοινωνίας σε ένα αφηρημένο επίπεδο, μόνο σαν μια αλληλουχία από ενέργειες αλληλεπίδραση των πρακτόρων της επικοινωνίας σε ένα αφηρημένο επίπεδο, μόνο σαν μια αλληλουχία από ενέργειες
μεταξύ συμμετεχόντων μεταξύ συμμετεχόντων
\item Η δεύτερη είναι ο φορμαλισμός της τοπικής περιγραφής. Σε αυτήν περιγράφεται η επικοινωνία από τη σκοπιά ενός \item Η δεύτερη είναι ο φορμαλισμός της τοπικής περιγραφής. Σε αυτήν περιγράφεται η επικοινωνία από τη σκοπιά ενός
...@@ -481,10 +508,41 @@ To κανάλι επικοινωνίας $k$ δημιουργείται ρητά ...@@ -481,10 +508,41 @@ To κανάλι επικοινωνίας $k$ δημιουργείται ρητά
Οι δύο άλγεβρες συνδέονται μεταξύ τους με μια σχέση προβολής, η οποία με βάση την καθολική περιγραφή της επικοινωνίας Οι δύο άλγεβρες συνδέονται μεταξύ τους με μια σχέση προβολής, η οποία με βάση την καθολική περιγραφή της επικοινωνίας
(τη χορεογραφία), παράγει την περιγραφή που αντιστοιχεί στα διάφορα endpoints αυτής. (τη χορεογραφία), παράγει την περιγραφή που αντιστοιχεί στα διάφορα endpoints αυτής.
\section{Τύποι Συνεδρίας και Γλώσσες Προγραμματισμού}
Σε πρακτικό επίπεδο, έχει υπάρξει μια πληθώρα εφαρμογών της θεωρίας των τύπων συνεδριών, και με διαφορετικές φιλοσοφίες.
Αρχικά, υπάρχει ο διαχωρισμός ανάμεσα σε στατικά, δυναμικά, και υβριδικά συστήματα τύπων συνεδριών.
\begin{itemize}
\item Ένα στατικό σύστημα τύπων συνεδριών πραγματοποιεί όλους τους ελέγχους του κατα το χρόνο μεταγλώττισης ενός
προγράμματος. Οποιαδήποτε παράβαση του πρωτοκόλλου θα αναφερθεί πριν την εκτέλεση του προγράμματος.
\item Ένα δυναμικό σύστημα τύπων συνεδριών παρακολουθεί την επικοινωνία ανάμεσα στα επιμέρους τμήματα ενός
προγράμματος. Οι τύποι συνεδρίας μετασχηματίζονται σε μηχανές πεπερασμένων καταστάσεων, και τα μηνύματα που
ανταλλάσονται επαληθεύονται με βάση αυτές.
\item Ένα υβριδικό σύστημα τύπων συνεδριών επαληθεύει ορισμένες ιδιότητες της επικοινωνίας (όπως τη σειρά ανταλλαγής
μηνυμάτων) στατικά, κατά τη μεταγλώττιση, και άλλες (όπως τη γραμμικότητα της επικοινωνίας, ή τους τύπους των
ανταλλασσόμενων μηνυμάτων) κατά το χρόνο εκτέλεσης του προγράμματος.
\end{itemize}
Επιπλέον, παρατηρούμε και διαφορές ως προς τον τρόπο με τον οποίο τα συστήματα τύπων συνεδριών παρέχονται στους
προγραμματιστές.
\begin{itemize}
\item Υπάρχουν γλώσσες, όπως η MOOL \cite{} και η SePi \cite{}, που παρέχουν τους τύπους συνεδριών ως built-in
primitives.
\item Σε άλλες υλοποιήσεις, όπως στην Multiparty Session C \cite{} ή στη Session Java \cite{} έχουμε την υλοποίηση
του συστήματος συνεδριών
μέσω μιας βιβλιοθήκης χρόνου εκτέλεσης, με την οποία μπορεί ο προγραμματιστής να συνδέσει το πρόγραμμά του.
\item Τέλος, υπάρχουν εξωτερικά εργαλεία τα οποία αναλύουν τον πηγαίο κώδικα ενός προγράμματος προκειμένουν να
πραγματοποιήσουν την ανάλυση σε επίπεδο τύπων συνεδρίας. Ένα παράδειγμα ενός τέτοιου εργαλείου περιγράφεται στο
επόμενο κεφάλαιο της παρούσας εργασίας.
\end{itemize}
% Implementation work % Implementation work
\chapter{Ένα στατικό σύστημα τύπων συνεδρίας σε Erlang} \chapter{Ένα στατικό σύστημα τύπων συνεδρίας σε Erlang}
Οι τύποι συνεδρίας είναι ένας από τους φορμαλισμούς που έχουν προταθεί για την δόμηση και την ανάλυση της αλληλεπίδρασης μεταξύ Οι τύποι συνεδρίας είναι ένας από τους φορμαλισμούς που έχουν προταθεί για την δόμηση και την ανάλυση της αλληλεπίδρασης μεταξύ
διεργασιών. διεργασιών. Παρουσιάζουμε ένα σύστημα τύπων συνεδρίας εκφρασμένο σαν ένα σύστημα τύπων κι επιδράσεων, εμπνευσμένο από
σχετική δουλειά στον τομέα \cite{effects-as-sessions-as-effects}.
\section{Το σύστημα τύπων} \section{Το σύστημα τύπων}
...@@ -720,7 +778,7 @@ biz() -> ...@@ -720,7 +778,7 @@ biz() ->
\end{itemize} \end{itemize}
Για μια ανάλυση του τρόπου με τον οποίο δουλεύει ο Dialyzer, ο αναγνώστης παραπέμπεται στα \cite{dialyzer-reference-manual} Για μια ανάλυση του τρόπου με τον οποίο δουλεύει ο Dialyzer, ο αναγνώστης παραπέμπεται στα \cite{dialyzer-reference-manual}
και \cite{practical-success-typings} \cite{lsp-scala}. και \cite{practical-success-typings}.
Χρησιμοποιούμε μια έκδοση του Dialyzer βασισμένη σε αυτήν που περιέχεται στην έκδοση 19.0 του Erlang/OTP, ελαφρώς Χρησιμοποιούμε μια έκδοση του Dialyzer βασισμένη σε αυτήν που περιέχεται στην έκδοση 19.0 του Erlang/OTP, ελαφρώς
τροποποιημένη για τους σκοπούς μας, ώστε να διατηρεί την πληροφορία που σχετίζεται με τους τύπους δεδομένων των τροποποιημένη για τους σκοπούς μας, ώστε να διατηρεί την πληροφορία που σχετίζεται με τους τύπους δεδομένων των
...@@ -743,7 +801,7 @@ $Function$ το όνομα της καλούμενης συνάρτησης, κ ...@@ -743,7 +801,7 @@ $Function$ το όνομα της καλούμενης συνάρτησης, κ
Στο τέλος της ανάλυσης των modules του προγράμματος, πραγματοποιούμε ένα iteration πάνω σε όλες τις ορισμένες Στο τέλος της ανάλυσης των modules του προγράμματος, πραγματοποιούμε ένα iteration πάνω σε όλες τις ορισμένες
συναρτήσεις, και κάνουμε resolve όλες τις επιδράσεις που δεν ήταν διαθέσιμες κατά τη διάρκεια αυτής. Εδώ, resolution συναρτήσεις, και κάνουμε resolve όλες τις επιδράσεις που δεν ήταν διαθέσιμες κατά τη διάρκεια αυτής. Εδώ, resolution
σημαίνει η αντικατάσταση των placeholders $\{unavailable, \{Module, Function, Arity\}\}$ με το πλήρες session type της σημαίνει η αντικατάσταση των placeholders \[\{unavailable, \{Module, Function, Arity\}\}\] με το πλήρες session type της
καλούμενης συνάρτησης στο session type της καλούσας. καλούμενης συνάρτησης στο session type της καλούσας.
Αυτός είναι και ο λόγος που δε μπορούμε να διαχειριστούμε αμοιβαίως αναδρομικές συναρτήσεις. Η πλήρης ανάπτυξη του Αυτός είναι και ο λόγος που δε μπορούμε να διαχειριστούμε αμοιβαίως αναδρομικές συναρτήσεις. Η πλήρης ανάπτυξη του
...@@ -786,21 +844,21 @@ session type της μιας στο session type της άλλης θα οδηγ ...@@ -786,21 +844,21 @@ session type της μιας στο session type της άλλης θα οδηγ
\hline \hline
Action Tag& First Argument & Second Argument &Explanation\\ Action Tag& First Argument & Second Argument &Explanation\\
\hline \hline
?f\_rec\_tag(T, E) & $T$: fix reference στην αναδρομική συν/ση & $E$: session type της συν/σης& Περιγράφει τον \textit{?f\_rec\_tag(T, E)} & $T$: fix reference στην αναδρομική συν/ση & $E$: session type της συν/σης& Περιγράφει τον
τύπο συνεδρίας μιας αναδρομικής συνάρτησης\\ τύπο συνεδρίας μιας αναδρομικής συνάρτησης\\
?sa\_recv\_tag(DT1, DT2) & $DT1$: τύπος δεδομένων του σώματος του receive clause & $DT2$: τύπος δεδομένων που \textit{?sa\_recv\_tag(DT1, DT2)} & $DT1$: τύπος δεδομένων του σώματος του receive clause & $DT2$: τύπος δεδομένων που
θα κάνει match με το receive clause & Session Type ενός receive clause \\ θα κάνει match με το receive clause & Session Type ενός receive clause \\
?sa\_send\_tag(P, DT) & $P$: pid reference του παραλήπτη & $DT$: τύπος δεδομένων του μηνύματος που αποστέλεται \textit{?sa\_send\_tag(P, DT)} & $P$: pid reference του παραλήπτη & $DT$: τύπος δεδομένων του μηνύματος που αποστέλεται
& Session Type ενός send clause \\ & Session Type ενός send clause \\
?sa\_offer\_tag(L) & $L$: λίστα με session types των receive clauses & - & Session Type ενός multi-branch receive statement \\ \textit{?sa\_offer\_tag(L)} & $L$: λίστα με session types των receive clauses & - & Session Type ενός multi-branch receive statement \\
?sa\_choice\_tag(L) & $L$: λίστα με session types των send clauses & - & Session Type ενός branching execution όπου \textit{?sa\_choice\_tag(L)} & $L$: λίστα με session types των send clauses & - & Session Type ενός branching execution όπου
το πρώτο session action κάθε branch είναι ένα send clause \\ το πρώτο session action κάθε branch είναι ένα send clause \\
?sa\_rec\_tag(T) & $T$: reference σε μια αναδρομική συν/ση & - & Session Type αναδρομικής κλήσης συν/σης \\ \textit{?sa\_rec\_tag(T)} & $T$: reference σε μια αναδρομική συν/ση & - & Session Type αναδρομικής κλήσης συν/σης \\
\hline \hline
\end{tabular} \end{tabular}
...@@ -1255,27 +1313,27 @@ sqrt_client(Server, N) -> ...@@ -1255,27 +1313,27 @@ sqrt_client(Server, N) ->
ότι αποστέλει ένα $atom sqrt$ αντί για $neg$ στο πρώτο της μήνυμα. ότι αποστέλει ένα $atom sqrt$ αντί για $neg$ στο πρώτο της μήνυμα.
\end{itemize} \end{itemize}
Στα σχήματα 6.1 έως 6.4 φαίνονται οι τύποι συνεδρίας των παραπάνω συναρτήσεων, σε μορφή γραφήματος. Στα σχήματα 5.4 έως 5.7 φαίνονται οι τύποι συνεδρίας των παραπάνω συναρτήσεων, σε μορφή γραφήματος.
\begin{figure}[ht] \begin{figure}[h]
\caption{server/0} \caption{server/0}
\centering \centering
\includegraphics[scale=0.4]{arithmetic/server_0.png} \includegraphics[scale=0.4]{arithmetic/server_0.png}
\end{figure} \end{figure}
\begin{figure}[ht] \begin{figure}[h]
\caption{sum\_client/2} \caption{sum\_client/2}
\centering \centering
\includegraphics[scale=0.5]{arithmetic/sum_client_2.png} \includegraphics[scale=0.5]{arithmetic/sum_client_2.png}
\end{figure} \end{figure}
\begin{figure}[ht] \begin{figure}[h]
\caption{neg\_client/2} \caption{neg\_client/2}
\centering \centering
\includegraphics[scale=0.5]{arithmetic/neg_client_2.png} \includegraphics[scale=0.5]{arithmetic/neg_client_2.png}
\end{figure} \end{figure}
\begin{figure}[ht] \begin{figure}[h]
\caption{sqrt\_client/2} \caption{sqrt\_client/2}
\centering \centering
\includegraphics[scale=0.5]{arithmetic/sqrt_client_2.png} \includegraphics[scale=0.5]{arithmetic/sqrt_client_2.png}
...@@ -1289,14 +1347,14 @@ sqrt_client(Server, N) -> ...@@ -1289,14 +1347,14 @@ sqrt_client(Server, N) ->
{server,0} : "u (4). Of<any; ?(atom x {atom, pid, (atom x atom)}). {server,0} : "u (4). Of<any; ?(atom x {atom, pid, (atom x atom)}).
?(atom x {atom, pid, (atom x atom)} x number). ?(atom x {atom, pid, (atom x atom)} x number).
?(atom x {atom, pid, (atom x atom)} x number). ?(atom x {atom, pid, (atom x atom)} x number).
pid(1) !(atom x pid x number).rec(4).,any; pid(1) !(atom x pid x number).rec(4).,
?(atom x {atom, pid, (atom x atom)}). any; ?(atom x {atom, pid, (atom x atom)}).
?(atom x {atom, pid, (atom x atom)} x number). ?(atom x {atom, pid, (atom x atom)} x number).
pid(1) !(atom x pid x number).rec(4).,any; pid(1) !(atom x pid x number).rec(4).,
?(atom x {atom, pid, (atom x atom)}). any; ?(atom x {atom, pid, (atom x atom)}).
?(atom x {atom, pid, (atom x atom)} x number). ?(atom x {atom, pid, (atom x atom)} x number).
pid(1) !(atom x pid x float).rec(4).,any; pid(1) !(atom x pid x float).rec(4).,
?(atom x any).>." any; ?(atom x any).>."
{sum_client,2} : "u (3). pid(1) !(atom x pid). {sum_client,2} : "u (3). pid(1) !(atom x pid).
pid(1) !(atom x pid x integer). pid(1) !(atom x pid x integer).
...@@ -1427,17 +1485,17 @@ The matching sequences are: ...@@ -1427,17 +1485,17 @@ The matching sequences are:
\appendix \appendix
\chapter{Ευρετήριο συμβολισμών} % \chapter{Ευρετήριο συμβολισμών}
%
$A \rightarrow B$ : συνάρτηση από το πεδίο $A$ στο πεδίο $B$. % $A \rightarrow B$ : συνάρτηση από το πεδίο $A$ στο πεδίο $B$.
%
\chapter{Ευρετήριο γλωσσών} % \chapter{Ευρετήριο γλωσσών}
%
\textbf{Haskell} : η γλώσσα της ζωής μου. % \textbf{Haskell} : η γλώσσα της ζωής μου.
%
\chapter{Ευρετήριο αριθμών} % \chapter{Ευρετήριο αριθμών}
%
42 : life, the universe and everything. % 42 : life, the universe and everything.
%%% End of document %%% End of document
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment