repos / bachelor-thesis.git

Syntax.lagda

  1\chapter{Syntax}
  2
  3\if{False}
  4\begin{code}
  5-- Imports
  6
  7open import Prelude
  8\end{code}
  9\fi
 10
 11Formal syntax and semantic of Jolie are based on SOCK process calculi~\cite{Gui07,Guidi}.  
 12SOCK was created for designing service-oriented systems and was inspired by notable $\pi$-calculus \cite{Milner1999} and WS-BPEL~\cite{BPEL}.  
 13Primitives in SOCK are able to express one-way and request-response communication,  parallel and sequential behaviour of processes and control primitives. 
 14
 15SOCK (so a formalization of Jolie program) comprises of three layers: 
 16
 17\begin{itemize}
 18\item \textit{Behavioural layer}: specifies with internal actions of a process and communication
 19performs as seen from the process’ point of view.
 20\item \textit{Service layer}: it deals with underlying
 21architectural instructions, states, service instances and correlation sets.
 22\item \textit{Network layer}: is in charge of connecting and interacting of communicating services.
 23\end{itemize}
 24
 25This chapter has three sections about the syntax of layers of Jolie. They contain the definition of abstract syntax tree in Agda and their description.
 26
 27
 28\section{Behaviour layer}
 29
 30The most important type of statements in behavioural level regards performing communications and handling data. Statements in this layer are called behaviours. Also, there are variables and expressions.
 31
 32\subsubsection{Handling data}
 33Communication messages in Jolie are represented by trees. Variables are paths in data trees and the type of the a data tree is a tree too. Communications are type checked at run-time when a message is received, and such type checking is formally defined at ~\cite{nielsen2013type}. For example:
 34
 35\begin{center}
 36  amount = 12\\
 37  amount.fruit.apple = 2\\
 38  amount.fruit.description = "Apple"\\
 39\end{center}
 40
 41The \textit{amount} variable represents the following tree:
 42
 43\Tree [ .{amount = 12} [ .fruit [ .{apple = 2} ]
 44                            [ .{description = "Apple"} ] ] ]
 45
 46\vspace{0.5cm}
 47
 48To simplify further operations with variables, we propose their enumeration. Let $ J $ be a Jolie program,
 49$ V = vars(J) $ -- variables in $ J $, then $ V_i = i$ where $i \in \mathbb{N} $.
 50Then the example above will look like:
 51
 52\Tree [ .$V_0$ [ .$V_1$ ]
 53               [ .$V_2$ ]]
 54
 55\begin{center}
 56  $V_0 =$ amount = 12 \Rightarrow\ 0\\
 57  $V_1 =$ amount.fruit.apple = 2 \Rightarrow\ 1\\
 58  $V_2 =$ amount.fruit.description = "Apple" \Rightarrow\ 2\\
 59\end{center}
 60
 61After this simplification, the type of variables can be defined. The type of natural numbers \AgdaDatatype{ℕ} is located in the standard library of Agda~\cite{agdastdlib}.
 62
 63\begin{code}
 64Variable : Set
 65Variable = ℕ
 66\end{code}
 67
 68Next, I define the possible values in Jolie. They are usual as in almost every programming language: strings, ints, booleans, doubles, longs and void. \AgdaDatatype{String}, \AgdaDatatype{Bool} and \AgdaDatatype{ℤ} are datatypes from the standard library.
 69
 70\begin{code}
 71data Value : Set where
 72  string : String → Value
 73  int : ℤ → Value
 74  bool : Bool → Value
 75  double : ℤ → ℤ → Value
 76  long : ℤ → Value
 77  void : Value
 78\end{code}
 79
 80Usually, there are binary and unary operations. Binary operations may be arithmetical (plus, minus, multiplication, division and power) and logical (equality, and, or). I define only one unary operation: $not$.
 81
 82\begin{code}
 83data BinaryOp : Set where
 84  -- Arithmetical
 85  plus minus mult div power : BinaryOp
 86  -- Logical operations
 87  equal and or : BinaryOp
 88
 89data UnaryOp : Set where
 90  not : UnaryOp
 91\end{code}
 92
 93Next, I define the type of expressions. Expressions may contain variables, binary operations, unary operations and constants.
 94
 95\begin{code}
 96data Expr : Set where
 97  var : Variable → Expr
 98  binary : BinaryOp → Expr → Expr → Expr
 99  unary : UnaryOp → Expr → Expr
100  constant : Value → Expr
101\end{code}
102
103Here are some examples of expressions which are possible to construct:
104
105\begin{itemize}
106
107\item $ 2 + 2 $
108
109\begin{code}
1102+2 : Expr
1112+2 = binary plus (constant (int (+ 2))) (constant (int (+ 2)))
112\end{code}
113
114\item $x + 1$
115\begin{code}
116x : Variable
117x = 0
118
119x+1 : Expr
120x+1 = binary plus (var x) (constant (int (+ 1)))
121\end{code}
122
123\item $ A \land B $
124
125\begin{code}
126A B : Variable
127A = 0
128B = 1
129
130A∧B : Expr
131A∧B = binary and (var A) (var B)
132\end{code}
133
134\end{itemize}
135
136\subsubsection{Communications}
137
138There are two types of communication statements in Jolie: input and output statements, both can be uni-directional (one-way operations) and bi-directional (request-response operations). In the case of output statements, we use the notion of an output port name (location) which is necessary for binding the communicated data to it. The data is made use by communication statements as variable paths and expressions described above.
139
140Operation names, channel names and locations (usually are URLs) are represented by strings.
141
142\begin{code}
143Operation Location Channel : Set
144Operation = String
145Location = String
146Channel = String
147\end{code}
148
149
150The following two types are called communication ports. They define how communications with other services are performed. There are two kinds of ports:
151
152\if{False}
153\begin{code}
154data Behaviour : Set
155\end{code}
156\fi
157
158\begin{itemize}
159\item \textit{Input ports}: they deal with exposing input operations to other services.
160
161\begin{code}
162data η : Set where
163  -- o(x) -- One-way
164  _[_] : Operation → Variable → η
165
166  -- o(x)(x'){B} -- Request-response
167  _[_][_]_ : Operation → Variable → Variable → Behaviour → η
168\end{code}
169
170\item \textit{Output ports}: they define how to invoke a set of operations of other services.
171
172\begin{code}
173data η^ : Set where
174  -- o@l(e) -- Notification
175  _at_[_] : Operation → Location → Expr → η^
176
177  -- o@l(e)(x) -- Solicit-response
178  _at_[_][_] : Operation → Location → Expr → Variable → η^
179\end{code}
180
181\end{itemize}
182
183\subsubsection{Behaviour}
184
185The behavioural layer has both ordinary control--flow statements ('if-then-else', 'while', 'assign')
186and special statements to control parallelism and communication ('inputchoice', 'parallel', 'input', 'output', etc).
187
188\begin{code}
189data Behaviour where
190  if_then_else_ : Expr → Behaviour → Behaviour → Behaviour
191  while[_]_ : Expr → Behaviour → Behaviour
192  -- Sequence
193  _∶_ : Behaviour → Behaviour → Behaviour
194  -- Parallel
195  _∥_ : Behaviour → Behaviour → Behaviour
196  -- Assign
197  _≃_ : Variable → Expr → Behaviour
198  nil : Behaviour
199  -- [η₁]{B₁}⋯[ηₐ]{Bₐ}
200  inputchoice : List (η × Behaviour) → Behaviour
201  wait : Channel → Operation → Location → Variable → Behaviour
202  exec : Channel → Operation → Variable → Behaviour → Behaviour
203  input : η → Behaviour
204  output : η^  → Behaviour
205\end{code}
206
207The \textit{input choices} behaviour is a list of options where each element represents the tuple of guard $\eta$ and the behaviour $b$, which is executed if $\eta$ allows. \textit{wait} and \textit{exec} are runtime behaviours. They are required for the preservation property of the type system.
208
209Here are some examples of behaviours which are possible to construct:
210
211\begin{itemize}
212
213\item The first example is a \AgdaDatatype{nothing} function. It takes any behaviour and does nothing.
214
215\begin{code}
216nothing : Behaviour → Behaviour
217nothing _ = nil
218\end{code}
219
220\item
221
222Notice, that \AgdaDatatype{Behaviour} has only \AgdaInductiveConstructor{if\_then\_else} constructor, but not \AgdaDatatype{if\_then} without `else` branch. This can be solved by defining a function \AgdaDatatype{if-then} which takes an expression and a behaviour for the branch, which is called when the expression is true.
223
224\begin{code}
225if-then : Expr → Behaviour → Behaviour
226if-then condition behaviour = if condition then behaviour else nil
227\end{code}
228
229\item The last example is the \AgdaDatatype{always} function. It's an infinite while loop which executes a given behaviour.
230
231\begin{code}
232always : Behaviour → Behaviour
233always behaviour = while[ constant (bool true) ] behaviour
234\end{code}
235
236\end{itemize}
237
238\input{NetworkAndService}