Add datatypes to arithm server example

thesis.tex

@@ -786,7 +786,7 @@ session type της μιας στο session type της άλλης θα οδηγ
         \hline
         Action Tag& First Argument & Second Argument &Explanation\\
         \hline
-        ?f\_rec\_tag(T, E)   & $T$: fix reference στην αναδρομική συν/ση & $E$: session type της συν/σης& Περιγράφει τον 
+        ?f\_rec\_tag(T, E)   & $T$: fix reference στην αναδρομική συν/ση & $E$: session type της συν/σης& Περιγράφει τον
         τύπο συνεδρίας μιας αναδρομικής συνάρτησης\\
 
         ?sa\_recv\_tag(DT1, DT2) & $DT1$: τύπος δεδομένων του σώματος του receive clause & $DT2$: τύπος δεδομένων που
@@ -806,25 +806,6 @@ session type της μιας στο session type της άλλης θα οδηγ
     \end{tabular}
 \end{center}
 
-
-%%\begin{center}
-%%    \begin{tabular}{||c c c c||}
-%%        \hline
-%%        Col1 & Col2 & Col2 & Col3 \\ [0.5ex]
-%%        \hline\hline
-%%        1 & 6 & 87837 & 787 \\
-%%        \hline
-%%        2 & 7 & 78 & 5415 \\
-%%        \hline
-%%        3 & 545 & 778 & 7507 \\
-%%        \hline
-%%        4 & 545 & 18744 & 7560 \\
-%%        \hline
-%%        5 & 88 & 788 & 6344 \\ [1ex]
-%%        \hline
-%%    \end{tabular}
-%%\end{center}
-
 \begin{lstlisting}[language=Erlang, caption=-sestype() annotation, basicstyle=\tiny]
 -sestype({{server, 0},
          ?f_rec_tag(1, [?sa_offer_tag([{?dt_any_tag, [?sa_recv_tag(?dt_any_tag,
@@ -879,9 +860,6 @@ annotations θα οδηγούσε σε απόρριψη αρκετών σωστ
 
 ο έλεγχος θα είχε αποτύχει, καθώς το $any$ αποτελεί τον υπερτύπο όλων των τύπων δεδομένων της Erlang.
 
-% TODO
-Το type lattice δίνεται στο σχήμα 5.Χ.
-
 \subsection{Έλεγχος peers}
 Πέραν του $-sestype()$, εισάγουμε και άλλο ένα annotation: $-peers()$. Χρησιμοποιώντας αυτό, ο προγραμματιστής μπορεί να
 υποδείξει στο σύστημά μας πως πρέπει να ελέγξει ότι δύο συναρτήσεις αποτελούν τα δύο άκρα ενός πρωτοκόλλου επικοινωνίας.
@@ -1199,30 +1177,49 @@ sqrt_client(Server, N) ->
 
 \begin{lstlisting}[language=Erlang, caption=Arithmetic Server Implementation, basicstyle=\tiny]
 -sestype({{server, 0},
-         ?f_rec_tag(1, [?sa_offer_tag([{?dt_atom_tag, [?sa_recv_tag(?dt_atom_tag, ?dt_tuple_tag([])),
-                                                       ?sa_recv_tag(?dt_integer_tag, ?dt_tuple_tag([])),
-                                                       ?sa_recv_tag(?dt_integer_tag, ?dt_tuple_tag([])),
-                                                       ?sa_send_tag(1, ?dt_tuple_tag([])), ?sa_rec_tag(1)]},
-                                       {?dt_atom_tag, [?sa_recv_tag(?dt_atom_tag, ?dt_tuple_tag([])),
-                                                       ?sa_recv_tag(?dt_integer_tag, ?dt_tuple_tag([])),
-                                                       ?sa_send_tag(1, ?dt_tuple_tag([])), ?sa_rec_tag(1)]},
-                                       {?dt_atom_tag, [?sa_recv_tag(?dt_atom_tag, ?dt_tuple_tag([])),
-                                                       ?sa_recv_tag(?dt_integer_tag, ?dt_tuple_tag([])),
-                                                       ?sa_send_tag(1, ?dt_tuple_tag([])), ?sa_rec_tag(1)]},
+         ?f_rec_tag(1, [?sa_offer_tag([{?dt_atom_tag, [?sa_recv_tag(?dt_atom_tag,
+                                                                   ?dt_tuple_tag([?dt_atom_tag, ?dt_pid_tag])),
+                                                       ?sa_recv_tag(?dt_atom_tag,
+                                                                    ?dt_tuple_tag([?dt_atom_tag, ?dt_pid_tag, ?dt_integer_tag])),
+                                                       ?sa_recv_tag(?dt_atom_tag,
+                                                                    ?dt_tuple_tag([?dt_atom_tag, ?dt_pid_tag, ?dt_integer_tag])),
+                                                       ?sa_send_tag(1,
+                                                                    ?dt_tuple_tag([?dt_atom_tag, ?dt_pid_tag, ?dt_integer_tag])),
+                                                                    ?sa_rec_tag(1)]},
+                                       {?dt_atom_tag, [?sa_recv_tag(?dt_atom_tag,
+                                                                    ?dt_tuple_tag([?dt_atom_tag, ?dt_pid_tag])),
+                                                       ?sa_recv_tag(?dt_atom_tag,
+                                                                    ?dt_tuple_tag([?dt_atom_tag, ?dt_pid_tag, ?dt_integer_tag])),
+                                                       ?sa_send_tag(1,
+                                                                    ?dt_tuple_tag([?dt_atom_tag, ?dt_pid_tag, ?dt_integer_tag])),
+                                                                    ?sa_rec_tag(1)]},
+                                       {?dt_atom_tag, [?sa_recv_tag(?dt_atom_tag,
+                                                                    ?dt_tuple_tag([?dt_atom_tag, ?dt_pid_tag])),
+                                                       ?sa_recv_tag(?dt_atom_tag,
+                                                                    ?dt_tuple_tag([?dt_atom_tag, ?dt_pid_tag, ?dt_integer_tag])),
+                                                       ?sa_send_tag(1,
+                                                                    ?dt_tuple_tag([?dt_atom_tag, ?dt_pid_tag, ?dt_number_tag])),
+                                                                    ?sa_rec_tag(1)]},
                                        {?dt_atom_tag, [?sa_recv_tag(?dt_atom_tag, ?dt_tuple_tag([]))]}])])}).
 
 -sestype({{sum_client, 2},
-         ?f_rec_tag(1, [?sa_send_tag(1, ?dt_tuple_tag([])), ?sa_send_tag(1, ?dt_tuple_tag([])),
-                        ?sa_send_tag(1, ?dt_tuple_tag([])), ?sa_recv_tag(?dt_atom_tag, ?dt_tuple_tag([])),
+         ?f_rec_tag(1, [?sa_send_tag(1, ?dt_tuple_tag([?dt_atom_tag, ?dt_pid_tag])),
+                        ?sa_send_tag(1, ?dt_tuple_tag([?dt_atom_tag, ?dt_pid_tag, ?dt_integer_tag])),
+                        ?sa_send_tag(1, ?dt_tuple_tag([?dt_atom_tag, ?dt_pid_tag, ?dt_integer_tag])),
+                        ?sa_recv_tag(?dt_atom_tag, ?dt_tuple_tag([?dt_atom_tag, ?dt_pid_tag, ?dt_integer_tag])),
                         ?sa_rec_tag(1)])}).
 
 -sestype({{neg_client, 2},
-         ?f_rec_tag(1, [?sa_send_tag(1, ?dt_tuple_tag([])), ?sa_send_tag(1, ?dt_tuple_tag([])),
-                        ?sa_recv_tag(?dt_atom_tag, ?dt_tuple_tag([])), ?sa_rec_tag(1)])}).
+         ?f_rec_tag(1, [?sa_send_tag(1, ?dt_tuple_tag([?dt_atom_tag, ?dt_pid_tag])),
+         `              ?sa_send_tag(1, ?dt_tuple_tag([?dt_atom_tag, ?dt_pid_tag, ?dt_integer_tag])),
+                        ?sa_recv_tag(?dt_atom_tag, ?dt_tuple_tag([?dt_atom_tag, ?dt_pid_tag, ?dt_integer_tag])),
+                        ?sa_rec_tag(1)])}).
 
 -sestype({{sqrt_client, 2},
-         ?f_rec_tag(1, [?sa_send_tag(1, ?dt_tuple_tag([])), ?sa_send_tag(1, ?dt_tuple_tag([])),
-                        ?sa_recv_tag(?dt_atom_tag, ?dt_tuple_tag([])), ?sa_rec_tag(1)])}).
+         ?f_rec_tag(1, [?sa_send_tag(1, ?dt_tuple_tag([?dt_atom_tag, ?dt_pid_tag])),
+                        ?sa_send_tag(1, ?dt_tuple_tag([?dt_atom_tag, ?dt_pid_tag, ?dt_integer_tag])),
+                        ?sa_recv_tag(?dt_atom_tag, ?dt_tuple_tag([?dt_atom_tag, ?dt_pid_tag, ?dt_number_tag])),
+                        ?sa_rec_tag(1)])}).
 \end{lstlisting}
 
 Τα contracts αυτά μας λένε το εξής: