Evgenii Akentev
·
2019-01-18
Semantics.lagda
1\chapter{Semantics of behavioural layer}
2
3\if{False}
4\begin{code}
5open import Prelude
6open import Typesystem
7open import Syntax
8\end{code}
9\fi
10
11This chapter describes the semantics of behaviour layer of Jolie, which is described with a labelled transition system. The labels with semantics rules are required for the type preservation property.
12
13\section{Labels}
14
15Before the description of the labels, I have to define the type of state. Since actions between behaviours are performed in processes, there is a need to keep the state of them. However, since this project is not an interpreter of Jolie, I don't care what the type of state is, so I chose it to be a natural number.
16
17\begin{code}
18State : Set
19State = ℕ
20\end{code}
21
22The semantics of Jolie are described with a labelled transition system. A transition between behaviours can have one of the following labels:
23
24\begin{code}
25data Label : Set where
26\end{code}
27
28The first label \AgdaInductiveConstructor{lb-nil} denotes the lack of action.
29
30\begin{code}
31 lb-nil : Label
32\end{code}
33
34Label \AgdaInductiveConstructor{lb-assign} denotes the action of evaluating expression $e$ and the assignment the result to the variable $x$.
35
36\begin{code}
37 ---- x = e
38 lb-assign : Variable → Expr → Label
39\end{code}
40
41Label \AgdaInductiveConstructor{lb-read} denotes reading the state $t$ of the underlying process.
42
43\begin{code}
44 ---- read t
45 lb-read : State → Label
46\end{code}
47
48The two following labels are dual. Their purpose is unidirectional communication and in the first part of bidirectional communication. Label \AgdaInductiveConstructor{lb-send} denotes sending an expression $e$ through an operation $o$ to a location $l$ over a fresh channel $r$.
49
50\begin{code}
51 ---- νr o@l(e)
52 lb-send : Channel → Operation → Location → Expr → Label
53\end{code}
54
55Label \AgdaInductiveConstructor{lb-store} denotes storing storing in a variable $x$ a message received through an operation $o$ over a channel $r$.
56
57\begin{code}
58 ---- r : o(x)
59 lb-store : Channel → Operation → Variable → Label
60\end{code}
61
62The next two labels are dual too. They are intended for the second of part of bidirectional communication. Label \AgdaInductiveConstructor{lb-write} denotes writing a variable $x$ at channel $r$ as part of an operation $o$.
63
64\begin{code}
65 ---- (r, o)!x
66 lb-write : Channel → Operation → Variable → Label
67\end{code}
68
69And the last one label \AgdaInductiveConstructor{lb-read-write} denotes reading a message from channel $r$ as part of an operation $o$ and storing it in a variable $x$.
70
71\begin{code}
72 ---- (r, o@l)?x
73 lb-read-write : Channel → Operation → Location → Variable → Label
74\end{code}
75
76There are also five more labels, but they are used in the service layer.
77
78\section{Semantic rules}
79
80There were created 17 semantic rules for the behavioural layer, but I present only the subset of them.
81
82Since semantic rules use the current state of processes, there is a need in such function which allows getting the value of expression at the current state. I express such function as a type:
83
84\begin{code}
85data _⟨_⟩≔_ : Expr → State → Expr → Set where
86 stub : ∀ {e₁ s e₂} → e₁ ⟨ s ⟩≔ e₂
87\end{code}
88
89The \AgdaInductiveConstructor{stub} constructor is very simple and should be replaced with a normal mechanism for working with states in the future. It's needed to make the type inhabited.
90
91The following type expresses the semantic rules (transitions). It consists of two behaviours and a label.
92
93\begin{code}
94data _↝_∶_ : Behaviour → Behaviour → Label → Set where
95\end{code}
96
97The first constructor is intended for the \AgdaInductiveConstructor{nil} behaviour. It constructs the type with two \AgdaInductiveConstructor{nil}s and one \AgdaInductiveConstructor{lb-nil} label.
98
99\begin{code}
100 b-nil : nil ↝ nil ∶ lb-nil
101\end{code}
102
103The \AgdaInductiveConstructor{b-assign} rule takes a variable $x$ and an expression $e$ and constructs the type with the variable $x$, the expression $e$, the behaviour \AgdaInductiveConstructor{nil} and the label \AgdaInductiveConstructor{lb-assign}. It means that the assignment action is performed in the transition to the \AgdaInductiveConstructor{nil} behaviour.
104
105\begin{code}
106 b-assign : {x : Variable} {e : Expr}
107 → (x ≃ e) ↝ nil ∶ lb-assign x e
108\end{code}
109
110The constructor is pretty simple. It checks if the value of an expression $e$ is true, then it takes a transition from the \AgdaInductiveConstructor{if\_then\_else} behaviour to the $b_1$ behaviour. Its label is \AgdaInductiveConstructor{lb-read} because it needs to get the value of the expression from the state.
111
112\begin{code}
113 b-if-then : {e : Expr} {t : State} {b₁ b₂ : Behaviour}
114 → e ⟨ t ⟩≔ (constant (bool true))
115 → (if e then b₁ else b₂) ↝ b₁ ∶ lb-read t
116\end{code}
117
118This rule is similar to the previous one. The difference is that it's indended for the case when the value of the expression $e$ is false. The result of a transition is the $b_2$ behaviour.
119
120\begin{code}
121 b-if-else : {e : Expr} {t : State} {b₁ b₂ : Behaviour}
122 → e ⟨ t ⟩≔ (constant (bool false))
123 → (if e then b₁ else b₂) ↝ b₂ ∶ lb-read t
124\end{code}
125
126The two following rules are standard. They describe the behaviour of the \AgdaInductiveConstructor{while[\_]\_} statement. They are under the \AgdaInductiveConstructor{lb-read} label too. \AgdaInductiveConstructor{b-iteration} iterates if the value of the expression is true and \AgdaInductiveConstructor{b-no-iteration} does nothing if the value is false.
127
128\begin{code}
129 b-iteration : {e : Expr} {t : State} {b : Behaviour}
130 → e ⟨ t ⟩≔ (constant (bool true))
131 → (while[ e ] b) ↝ (b ∶ (while[ e ] b)) ∶ lb-read t
132
133 b-no-iteration : {e : Expr} {t : State} {b : Behaviour}
134 → e ⟨ t ⟩≔ (constant (bool false))
135 → (while[ e ] b) ↝ nil ∶ lb-read t
136\end{code}
137
138The semantic rules for the parallel and sequence behaviours are standard too. If there is a transition $ B_1 \xrightarrow{\eta} B_1' $, then the resulting transition is possible for both semantic rules.
139
140\begin{code}
141 b-seq : {b₁ b₂ b₁′ : Behaviour} {η : Label}
142 → b₁ ↝ b₁′ ∶ η
143 → (b₁ ∶ b₂) ↝ (b₁′ ∶ b₂) ∶ η
144
145 b-par : {b₁ b₂ b₁′ : Behaviour} {η : Label}
146 → b₁ ↝ b₁′ ∶ η
147 → (b₁ ∥ b₂) ↝ (b₁′ ∥ b₂) ∶ η
148\end{code}
149
150The last semantic rule is called \AgdaInductiveConstructor{b-struct}. It means that if there are two equal behaviours $b_1$ and $b_2$, a transition $ b_2 \xrightarrow{\eta} b_2' $ and $b_1'$ is equal to $b_2'$, then there is a transition $ b_1 \xrightarrow{\eta} b_1' $. This rule states that behaviours that are structurally congruent have the same transitions.
151
152\begin{code}
153 b-struct : {b₁ b₂ b₁′ b₂′ : Behaviour} {η : Label}
154 → b₁ ≡ b₂
155 → b₂ ↝ b₂′ ∶ η
156 → b₁′ ≡ b₂′
157 → b₁ ↝ b₁′ ∶ η
158\end{code}
159
160The definition of structural congruence for behaviours is given in the next chapter with the lemma and its proof.