274
R. Hamers and S.-S. Jongmans
1 ↓
[S↓-One]
S i∈{1,2} ↓
S1 + S2 ↓
[S↓-Alt]
S1 ↓ and S2 ↓
S1 · S2 ↓
[S↓-Seq]
S1 ↓ and S2 ↓
S1 S2 ↓
[S↓-Par]
Fig. 9. Operational semantics of the specification calculus (termination)
(f v, ∅, ∅)
τ
− →
∗ (true, ∅, ∅)
p[n] q[m] : f
p[n]q[m]!v
− −−−−−− → p[n]q[m]?v
p[n]q[m]?v
− −−−−−− → 1
[S-Com]
S = p[n] q[m]
S
p[n]q[m]#
−−−−−−→ 1
[S-Cls]
S i∈{1,2}
β
− → S
S1 + S2
β
− → S
[S-Alt]
S1
β
− → S
1
S1 · S2
β
− → S
1 · S2
[S-Seq1]
S1 ↓ and S2
β
− → S
2
S1 · S2
β
− → S
2
[S-Seq2]
S[fix X S/X]
β
− → S
fix X S
β
− → S
[S-Rec]
S1
β
− → S
1
S1 S2
β
− → S
1 S2
[S-Par1]
S2
β
− → S
2
S1 S2
β
− → S1 S
2
[S-Par2]
S[n/x] ⊗ (... ⊗ (S[n
−1/x] ⊗ S[n
/x]))
β
− → S
⊗
n≤x≤n S
β
− → S
[S-Rep]
Fig. 10. Operational semantics of the specification calculus (reduction)
and ⊗ over {+, ·, }. The calculus is generated by the following grammar:
S ::= 1
p[n] q[m] : f
p[n]q[m]?v
p[n] q[m]
S 1 + S 2
S 1 · S 2
S 1 S 2
fix X S
X
⊗
n≤x≤n S
Calculus notation corresponds with Discourje notation (Sect. 2): p[n] q[m] : f
specifies communication of a value that satisfies f from p[n] to p[m]; p[n] q[m]
specifies closing of the channel from p[n] to q[m]; S 1 ⊗ S 2 specifies the alternative, sequential, and parallel composition of S 1 and S 2 ; fixX S and X specify
recursion; and
⊗
n≤x≤n S specifies repetition of S for every value x between n
and n
, where iterations are composed using ⊗. “Boxed” specifications (1 and
p[n]q[m]?v; the box is not part of the syntax) are auxiliary in the sense they
are used in defining the operational semantics (below), but they are not written
directly in specifications by programmers: 1 specifies a skip; p[n]q[m]?v specifies
a receive of v by q[m], previously sent by p[n].
The operational semantics of the calculus is defined in terms of termination
predicate ↓ and labeled reduction relation →. Labels, ranged over by β, are of the
form p[n]q[m]!v (send), p[n]q[m]?v (receive), and p[n]q[m]# (close). The termination and reduction rules are shown in Figs. 9–10. (This operational semantics
coincides with Basic Process Algebra [22], plus free merge, recursion, and repetition.) Rule [S-Com] induces two reductions (first a send, then a receive), via
auxiliary specification p[n]q[m]?v. We note that the specification calculus has no
τ -reductions (which are not monitored; we verify only channel actions). We also
note that it can express some, but not all, context-free languages: it can count
(using
), but it cannot encode a stack.
R. Hamers and S.-S. Jongmans
1 ↓
[S↓-One]
S i∈{1,2} ↓
S1 + S2 ↓
[S↓-Alt]
S1 ↓ and S2 ↓
S1 · S2 ↓
[S↓-Seq]
S1 ↓ and S2 ↓
S1 S2 ↓
[S↓-Par]
Fig. 9. Operational semantics of the specification calculus (termination)
(f v, ∅, ∅)
τ
− →
∗ (true, ∅, ∅)
p[n] q[m] : f
p[n]q[m]!v
− −−−−−− → p[n]q[m]?v
p[n]q[m]?v
− −−−−−− → 1
[S-Com]
S = p[n] q[m]
S
p[n]q[m]#
−−−−−−→ 1
[S-Cls]
S i∈{1,2}
β
− → S
S1 + S2
β
− → S
[S-Alt]
S1
β
− → S
1
S1 · S2
β
− → S
1 · S2
[S-Seq1]
S1 ↓ and S2
β
− → S
2
S1 · S2
β
− → S
2
[S-Seq2]
S[fix X S/X]
β
− → S
fix X S
β
− → S
[S-Rec]
S1
β
− → S
1
S1 S2
β
− → S
1 S2
[S-Par1]
S2
β
− → S
2
S1 S2
β
− → S1 S
2
[S-Par2]
S[n/x] ⊗ (... ⊗ (S[n
−1/x] ⊗ S[n
/x]))
β
− → S
⊗
n≤x≤n S
β
− → S
[S-Rep]
Fig. 10. Operational semantics of the specification calculus (reduction)
and ⊗ over {+, ·, }. The calculus is generated by the following grammar:
S ::= 1
p[n] q[m] : f
p[n]q[m]?v
p[n] q[m]
S 1 + S 2
S 1 · S 2
S 1 S 2
fix X S
X
⊗
n≤x≤n S
Calculus notation corresponds with Discourje notation (Sect. 2): p[n] q[m] : f
specifies communication of a value that satisfies f from p[n] to p[m]; p[n] q[m]
specifies closing of the channel from p[n] to q[m]; S 1 ⊗ S 2 specifies the alternative, sequential, and parallel composition of S 1 and S 2 ; fixX S and X specify
recursion; and
⊗
n≤x≤n S specifies repetition of S for every value x between n
and n
, where iterations are composed using ⊗. “Boxed” specifications (1 and
p[n]q[m]?v; the box is not part of the syntax) are auxiliary in the sense they
are used in defining the operational semantics (below), but they are not written
directly in specifications by programmers: 1 specifies a skip; p[n]q[m]?v specifies
a receive of v by q[m], previously sent by p[n].
The operational semantics of the calculus is defined in terms of termination
predicate ↓ and labeled reduction relation →. Labels, ranged over by β, are of the
form p[n]q[m]!v (send), p[n]q[m]?v (receive), and p[n]q[m]# (close). The termination and reduction rules are shown in Figs. 9–10. (This operational semantics
coincides with Basic Process Algebra [22], plus free merge, recursion, and repetition.) Rule [S-Com] induces two reductions (first a send, then a receive), via
auxiliary specification p[n]q[m]?v. We note that the specification calculus has no
τ -reductions (which are not monitored; we verify only channel actions). We also
note that it can express some, but not all, context-free languages: it can count
(using
), but it cannot encode a stack.