Discourje: Runtime Verification of Communication Protocols in Clojure
273
(I, E, H)
α
− → (I
, E
, H
)
(C[I], E, H)
α
− → (C[I ], E , H )
[I-Ctxt]
I[v/x]
α
− → I
((fn x I) v, E, H)
α
− → (I , E, H)
[I-App]
E(x) = v
(x, E, H)
τ
− → (v, E, H)
[I-Var]
(def x v, E, H)
τ
− → (nil, E[x → v], H)
[I-Def]
I[v/x]
α
− → I
(let x v I, E, H)
α
− → (I , E, H)
[I-Let]
I[v/x][(fn xr (loop x xr I))/recur ]
α
− → I
(loop x v I, E, H)
α
− → (I , E, H)
[I-Loop]
v ∈ {true, false}
(Iv, E, H)
α
− → (I
v , E, H)
(if v Itrue I false , E, H)
α
− → (I
v , E, H)
[I-If]
(I, E, H)
α
− → (I
, E, H)
(v · I, E, H)
α
− → (I , E, H)
[I-Seq]
H() = (w, n) and |w| < n
(send v, E, H)
!v
− − →
(nil, E, H[ → (v·w, n)])
[I-Send]
H() = (w·v, n)
(recv , E, H)
?v
− − →
(v, E, H[ → (w, n)])
[I-Recv]
H() = (w, n) and n > 0
(close , E, H)
#
− − →
(nil, E, H[ → (w, 0)])
[I-Close]
H() = ⊥ and v > 0
(chan v, E, H)
τ
− →
(, E, H[ → (, v)])
[I-Chan]
Fig. 8. Operational semantics of the implementation calculus
Contexts are generated by the following grammar:
C ::= | C I | (fn x I) C | def x C | let x C I | loop x C I | if C I t I f | C · I |
send C I | send C | recv C | close C | chan C | C C I | I C
Rule [I-App] executes the first step of a function: it first substitutes value v for
variable x in body I (notation: I[v/x]), and then executes the first step. Rule [IVar] executes a read in the global environment. Rule [I-Def] executes a write to
the global environment (notation: E[x → v]). Rule [I-Let] executes the first step
of a let binder, similar to rule [I-App]. Rule [I-Loop] executes the first step of a
loop: it first substitutes value v for variable x (the loop parameter) in body I,
then substitutes the loop itself (wrapped in a function to rebind x in the loop’s
next iteration) for recur, and then executes the first step. Rule [I-If] executes
the first step of a branch of a conditional, if the condition is boolean. Rule [ISeq] executes the first step of the suffix of a sequence, after the prefix has been
executed using rule [I-Ctxt]. Rule [I-Send] executes the send through a channel,
if that channel exists and is not full. Rule [I-Recv] executes the receive through a
channel, if that channel exists and is not empty. Rule [I-Close] executes the close
of a channel, if that channel exists and is not yet closed. Rule [I-Chan] executes
the creation of a new channel.
Specification calculus. Next, we define a calculus to model Discourje specifications. Let p, q range over roles, f over boolean functions (from the implementation calculus), n, m over number expressions (from the implementation calculus),
273
(I, E, H)
α
− → (I
, E
, H
)
(C[I], E, H)
α
− → (C[I ], E , H )
[I-Ctxt]
I[v/x]
α
− → I
((fn x I) v, E, H)
α
− → (I , E, H)
[I-App]
E(x) = v
(x, E, H)
τ
− → (v, E, H)
[I-Var]
(def x v, E, H)
τ
− → (nil, E[x → v], H)
[I-Def]
I[v/x]
α
− → I
(let x v I, E, H)
α
− → (I , E, H)
[I-Let]
I[v/x][(fn xr (loop x xr I))/recur ]
α
− → I
(loop x v I, E, H)
α
− → (I , E, H)
[I-Loop]
v ∈ {true, false}
(Iv, E, H)
α
− → (I
v , E, H)
(if v Itrue I false , E, H)
α
− → (I
v , E, H)
[I-If]
(I, E, H)
α
− → (I
, E, H)
(v · I, E, H)
α
− → (I , E, H)
[I-Seq]
H() = (w, n) and |w| < n
(send v, E, H)
!v
− − →
(nil, E, H[ → (v·w, n)])
[I-Send]
H() = (w·v, n)
(recv , E, H)
?v
− − →
(v, E, H[ → (w, n)])
[I-Recv]
H() = (w, n) and n > 0
(close , E, H)
#
− − →
(nil, E, H[ → (w, 0)])
[I-Close]
H() = ⊥ and v > 0
(chan v, E, H)
τ
− →
(, E, H[ → (, v)])
[I-Chan]
Fig. 8. Operational semantics of the implementation calculus
Contexts are generated by the following grammar:
C ::= | C I | (fn x I) C | def x C | let x C I | loop x C I | if C I t I f | C · I |
send C I | send C | recv C | close C | chan C | C C I | I C
Rule [I-App] executes the first step of a function: it first substitutes value v for
variable x in body I (notation: I[v/x]), and then executes the first step. Rule [IVar] executes a read in the global environment. Rule [I-Def] executes a write to
the global environment (notation: E[x → v]). Rule [I-Let] executes the first step
of a let binder, similar to rule [I-App]. Rule [I-Loop] executes the first step of a
loop: it first substitutes value v for variable x (the loop parameter) in body I,
then substitutes the loop itself (wrapped in a function to rebind x in the loop’s
next iteration) for recur, and then executes the first step. Rule [I-If] executes
the first step of a branch of a conditional, if the condition is boolean. Rule [ISeq] executes the first step of the suffix of a sequence, after the prefix has been
executed using rule [I-Ctxt]. Rule [I-Send] executes the send through a channel,
if that channel exists and is not full. Rule [I-Recv] executes the receive through a
channel, if that channel exists and is not empty. Rule [I-Close] executes the close
of a channel, if that channel exists and is not yet closed. Rule [I-Chan] executes
the creation of a new channel.
Specification calculus. Next, we define a calculus to model Discourje specifications. Let p, q range over roles, f over boolean functions (from the implementation calculus), n, m over number expressions (from the implementation calculus),