Specifying and Verifying Parametric Processes

Wiesław Pawłowski^{∗} Paweł Pa̧czkowski^{†} Stefan Sokołowski^{∗}

December 1994

Abstract

A framework in which processes parametrized with other processes can be specified, defined and verified is introduced. Higher order processparameters are allowed. The formalism resembles typed lambda calculus built on top of a process algebra, where specifications play the role of types. A proof system for deriving judgements “parametric process meets a specification” is given.

1 Introduction

A typical approach to software development is that of decomposition of large tasks into smaller subtasks. The decomposition principle, when formalized in terms of a specification system, by which, following [Sokołowski 94], we mean a triple

(Constr, Spec, sat)

consisting of a set of constructions Constr (programs, processes, etc.), a set of specifications Spec, and satisfaction relation sat relating constructions to specifications, amounts to the requirement that a task of providing a construction c that satisfies a given specification S (denoted c sat S) can be decomposed as follows:

1. provide sub-constructions c_{1}, …, c_{n} that satisfy some sub-specifications S_{1}, …, S_{n} into which the original specification S is decomposed, and

2. provide a method of combining c_{1}, …, c_{n} so as to obtain such c that c sat S.

In [Sokołowski 94], a point of view was taken, that the method mentioned in point 2 should be a construction itself, i.e. belong to Constr. Adopting this point of view we can rephrase 2 as 2′. provide a parametric construction f such that

∗Institute of Computer Science, Polish Academy of Sciences, ul. Abrahama 18, 81-825 Sopot, Poland, e-mail: {W.Pawlowski, S.Sokolowski}@IPIPAN.Gda.PL; supported by ICS PAN, KBN grant PB-1312/P3/92/02 and CRIT IC 1010/II.

†Department of Computing Science, Chalmers University of Technology, 412-96 Göteborg, Sweden, and Institute of Mathematics, University of Gdańsk, ul. Wita Stwosza 57, 80-952 Gdańsk, Poland, e-mail: pawel@cs.chalmers.se, matpmp@halina.univ.gda.pl; supported by KBN grant PB-1312/P3/92/02, CRIT IC 1010/II and ESPRIT BRA CONCUR2.

f sat S_{1} → S_{2} → ⋯ → S_{n} → S

The “functional” specification S_{1} → S_{2} → ⋯ → S_{n} → S, which is assumed to belong to Spec, is intended to specify precisely those parametric constructions which yield objects satisfying S when applied to sub-constructions satisfying S_{1}, …, S_{n}. Thus, if the decomposition steps 1 and 2′ are realized then fc_{1} … c_{n} defines c we were looking for.

When the sub-constructions are again decomposed into smaller bits the parameters become parametric themselves and we have to deal with higher order parameters. In [Sokołowski 94] a more elaborate decomposition schema than the one presented above is considered: dependent products rather than functional specifications are allowed, but here we will confine ourselves to a simple setup.

The purpose of this work is to apply the methodology sketched above in the context of concurrent process specification and verification. As a starting point we adopt a process algebra and logic for specifying processes proposed in [Olderog 91]. Olderog extends a process algebra by introducing mixed terms, where a specification can become a part of a process term. This enables transformation based development of processes [Olderog 91, Olderog 91a]. We consider a different option and introduce parametric processes that contain process variables. We allow higher order parametricity: process variables can represent also parametric processes. Technically speaking, Olderogs’s process algebra is extended with abstraction and application primitives. This leads to a formalism resembling a typed lambda calculus built on top of a process algebra, where specifications play the role of types. Mixed terms can be viewed as a special case of parametric processes.

We provide a proof system for deriving judgements “a (parametric) process meets a specification”. To this end, we needed to reformulate the proof system for nonparametric processes that was given in [Olderog 91]. Derivations in that proof system use mixed terms. We provide a direct proof system for nonparametric processes, which does not appeal to mixed terms and which is shown to be equivalent to that of [Olderog 91]. The direct proof system is extended to the parametric case.

The concept of parametric processes (but only first order ones) has already appeared in [Milner 89]. However, this method of constructing CCS processes is not reflected in their verification because the bisimulation proof technique used in this reference requires a considerable effort in decomposing large verification tasks into smaller ones (see e.g. [Larsen and Milner 86]).

The formalism we develop allows decomposition steps of the form 1 and 2′ that involve higher-order processes as parameters and helps one to do a systematic book-keeping of process dependencies, which is useful in higher-order constructions. We view our approach as an alternative to process development methods using transformation [Olderog 91] or refinement [Holmström 89] techniques.

The paper is organized as follows. In Section 2 we present a process algebra of nonparametric processes and a logic for specifying them that appear in [Olderog 91]. A new, direct proof system for nonparametric processes is given in Section 3. In Section 4 we define parametric processes and extend the proof system to the parametric case. Section 5 contains an example.

2 Nonparametric processes and specifications

The class of processes that we consider and a logic for specifying their properties are taken from [Olderog 91]. We briefly present the main notions, referring to [Olderog 91] for a comprehensive exposition.

2.1 Processes

Let Comm be an infinite set of communications. Together with a special symbol τ representing a hidden or internal activity of a process it will constitute the set of actions.

In order to define a syntactic representation of processes we start with a description of the set of recursive terms Rec. Let X be a (countable) set of (process) identifiers. We assume that X is partitioned into sets X_{A} of identifiers with alphabet A, where A ⊆ Comm is finite. In the definition below P and Q range over recursive terms, X ranges over identifiers, and A over finite sets of communications. The set Rec is defined as follows:

P ::=  stop_{A} (deadlock)
| a.P  (prefix)
| P + Q (choice)
| P ∥ Q (parallel composition)
| P [b/a] (renaming)
| P \a (hiding)
| X  (identifier)
| μX.P (recursion)

Iterated applications of renaming and hiding will be abbreviated as follows:

• P [b̄/ā] will stand for P [b_{1}/a_{1}] … [b_{n}/a_{n}], where b̄ = b_{1}, …, b_{n}, ā = a_{1}, …, a_{n}

• P \A will denote P \a_{1} … \a_{n}, where A = {a_{1}, … a_{n}}.

Definition 1 A recursive term P is communication guarded if there exists a set of communications A such that for every recursive subterm μX.Q of P, for every free occurrence of X in Q

(1) X lies within a subterm of Q of the form a.R

(2) X does not lie within a subterm of Q of the form R[b/a] or R\a, where a ∈ A and b ∉ A.

If the condition (2) above is dropped, we say that P is action guarded (this notion is usually given a separate, slightly simpler definition).

To define process terms one more notion is needed — a notion of a (communication) alphabet. An alphabet of a recursive term P (denoted by α(P)) is a set of communications defined inductively as follows:

\begin{aligned}α(stop_{A}) & = & A \\ α(a.P) & = & \{a\} ∪ α(P) \\ α(P + Q) & = & α(P) ∪ α(Q) \\ α(P ∥ Q) & = & α(P) ∪ α(Q) \\ α(P [b/a]) & = & (α(P) − \{a\}) ∪ \{b\} \\ α(P \a) & = & (α(P) − \{a\}) \\ α(X) & = & A if X ∈ X_{A} \\ α(μX.P) & = & α(X) ∪ α(P) \end{aligned}

Definition 2 We say that a recursive term P is a process term (or simply, a process) if it satisfies the following conditions:

• P is action guarded

• every subterm a.Q of P satisfies a ∈ α(Q)

• every subterm Q + R of P satisfies α(Q) = α(R)

• every subterm μX.Q of P satisfies α(X) = α(Q)

The set of all process terms will be denoted by Proc. A process term is closed if it does not contain free process identifiers. The set of all closed process terms will be denoted by CProc.

The intuitive meaning of process terms is as follows:

• stop_{A} denotes a process which neither engages in any communication nor in any internal action.

• a.P denotes a process which first communicates a and then behaves like P.

• P + Q denotes a process which behaves like P or like Q depending on whether its first action was an action of P or of Q. If the first action could be performed by P as well as by Q the choice made is nondeterministic.

• P ∥ Q denotes a parallel composition of P and Q which behaves as P and Q working independently except for synchronization on actions belonging to the intersection of their communication alphabets.

• P [b/a] denotes a process which behaves like P, but with all actions a changed to b.

• P \a denotes a process which behaves like P, but with all actions a hidden, i.e. changed to τ.

• μX.P behaves like P, but with every occurrence of X inside P denoting a “recursive call” to μX.P.

The above intuition can be made precise in several different ways. One possible choice is so called readiness semantics. It describes process behaviour in terms of pairs (tr, F) where tr is finite sequence of communications called trace, and F, called ready set, is a set of actions in which a process is ready to engage after “performing” the trace tr. Besides the ready pairs the semantic domain contains a distinguished element τ representing initial unstability of a process, and “divergent” ready pairs of the form (tr, ↑) which represent behaviours where a process after performing trace tr enters an infinite loop.

Thus, the set of process information over A is defined as:

Info_{R,A} = {τ} ∪ A^{∗} × P(A) ∪ A^{∗} × {↑}

and the semantic domain of the readiness semantics is defined as follows:

DOM_{R} = ⋃_{A⊆Comm} DOM_{R,A}

where A is a finite subset of Comm and

DOM_{R,A} = {(A, Γ)|Γ ⊆ Info_{R,A}}.

The readiness semantics for closed process terms is a function:

R^{∗}[[·]] : CProc → DOM_{R}

which can be given an elegant denotational definition.

There is a natural partial ordering on the semantic domain DOM_{R}:

(A_{1}, R_{1}) ⊑ (A_{2}, R_{2}) if A_{1} = A_{2} and R_{1} ⊇ R_{2}

Intuitively, if R^{∗}[[P]] ⊑ R^{∗}[[Q]] then the process denoted by Q is more controllable than the one denoted by P, i.e. it is more deterministic, less divergent and more stable.

2.2 Readiness specifications

Processes are specified by formulas of many-sorted predicate logic, called readiness logic, which has sorts of communications, traces (finite sequences of communications), ready sets (finite subsets of communications), natural numbers and logical values. In this report we give just a minimal necessary information on readiness logic. For our purposes it is sufficient to remark that readiness logic allows one to define sets of ready pairs in a direct manner and is fairly expressive, for example, regular sets over Comm can be expressed in it.

A readiness specification is a formula of readiness logic, in which at most the distinguished trace variable h and the distinguished set variable F are free, and which satisfies some natural syntactic restrictions that guarantee a monotonicity property explained below. Since a specification has just two free variables h and F, the notion of truth of a specification with respect to the evaluation (tr, F) of h and F can be defined and will be denoted

(tr, F) ⊧ S  (1)

If (1) holds we say that S is satisfied by a ready pair (tr, F). Thus, a specification S determines a set of ready pairs which satisfy it.

Moreover, with every specification S its alphabet, denoted by α(S), can be associated. This is a consequence of yet another syntactic restriction on readiness formulas that every occurrence of the free variable h lies in the scope of projection ↓_{A} onto some finite set of communications A. What it means semantically is that S defines a set of ready pairs (tr, F), where only the projection of tr onto α(S) is defined and the actions outside α(S) do not affect satisfiability of S by (tr, F).

The monotonicity property of readiness specifications that was mentioned above is defined as follows: for an arbitrary readiness specification S and for all traces tr and ready sets F and G

(tr, F) ⊧ S and F ⊆ G imply (tr, G) ⊧ S

The set of specifications will be denoted by Spec. The readiness semantics of readiness specifications is defined as follows:

R^{∗}[[S]] = (α(S), {(tr, F)|tr ∈ α(S)^{∗} ∧ F ⊆ α(S) ∧ (tr, F) ⊧ S}).

2.3 Satisfaction relation

Since processes as well as specifications are interpreted semantically over readiness domain, the satisfaction relation has a simple semantic definition:

P sat S iff R^{∗}[[P]] ⊒ R^{∗}[[S]]

Intuitively, it means that

• The process P and the specification S have the same alphabets i.e. α(P) = α(S).

• Safety condition. If P may engage in a trace tr then there must exist a ready set F such that (tr, F) ⊧ S.

• Liveness condition. After performing a trace tr the process P must engage in one of the ready sets F such that (tr, F) ⊧ S.

• Stability condition. The process P is stable immediately.

2.4 Proof system for sat via mixed terms

The inference system for sat defined in [Olderog 91] makes use of a notion of mixed terms. Mixed terms are, as the name suggests, a mixture of readiness specifications and process terms and are formally defined by allowing specifications in recursive terms

P ::= S | stop_{A} | a.P | …

and generalizing the definitions of alphabets and processes in a straightforward way.

Since processes and specifications are interpreted in the same semantic domain, there is no difficulty in extending readiness semantics to mixed terms. The satisfaction relation on mixed terms, denoted by ≡>, is defined as

M_{1} ≡> M_{2} iff R^{∗}[[M_{1}]] ⊒ R^{∗}[[M_{2}]],

where M_{1}, M_{2} are mixed terms. The relation sat can be viewed as a special case of ≡> restricted to the pairs P ≡> S where P is a process and S is a specification.

In [Olderog 91] a proof system for ≡> is given, which obviously allows us to derive assertions of the form P sat S, but mixed terms will be used in the derivations. The inference rules of the proof system for ≡> are presented in Table 1. In these rules, P, Q, R range over closed mixed terms, S and T — over specifications. Curly braces are used to denote syntactic substitutions.

3 Proof system for sat

The first step towards introducing parametricity into the formalism proposed by Olderog is to provide a proof system for sat, which does not appeal to mixed terms. In Table 2 we propose such a proof system, whose rules bear a clear resemblance to Olderog’s proof system for ≡>. (From now on, the symbol ≡> will refer to the syntactic notion of derivability in the proof system of Table 1.)

The judgements of the proof system for sat have the form

Γ ⊢ P sat S,  (2)

where P ∈ Proc, S ∈ Spec and Γ is a set of assumptions,

Γ = {X_{1} sat S_{1} , …, X_{n} sat S_{n}}.

The sets of assumptions will be needed to handle recursion. The special case of (2), with Γ = ∅ will be shown to coincide with Olderog’s notion of P ≡> S.

The theorems below show the relative soundness and completeness of the proposed proof system for sat with respect to the proof system for ≡>.

To state the theorems we need the following auxiliary notation: for a process term P and Γ = {X_{1} sat S_{1} , …, X_{n} sat S_{n}}, by P {Γ} we shall denote a mixed term P {S_{1}/X_{1}, …, S_{n}/X_{n}}, obtained from P by replacing free occurrences of variables X_{1}, …, X_{n} by specifications S_{1}, …, S_{n}.

To distinguish the rules of the proof systems for ≡> and for sat, we add index _{≡>} to the names of the respective rules of the proof system for ≡>.

Theorem 3 (Relative soundness of proof system for sat) If Γ ⊢ P sat S then P {Γ} ≡> S.

Proof. Follows by by induction on the length of the derivation of Γ ⊢ X sat S. Note, that some of the assumptions of proof rules in Table 1 are replaced by different but equivalent versions in Table 2. Such equivalent pairs of assumptions are collected in Lemma 4 below. □

(Reflexivity)  P ≡> P

(Transitivity)  \frac{P ≡> Q  Q ≡> R}{P ≡> R}

(Context)  \frac{Q ≡> R}{M\{Q/X\} ≡> M\{R/X\}}

where M is a mixed term, M{Q/X} and M{R/X} are closed mixed terms

(Consequence) \frac{⊧ S ⇒ T}{P ≡> T} , where α(S) = α(T)

(Deadlock)  stop_{A} ≡> h↓_{A} ≤ ε

(Prefix) \frac{(ε, \{a\}) ⊧ S}{a.S\{a.h/h\} ≡> S} , where a ∈ α(S)

(Choice)  S + T ≡> φ_{+}(S, T)

where φ_{+}(S, T) ≡ (h↓_{A} = ε ⇒ S ∧ T) ∧ (h↓_{A} ≠ ε ⇒ S ∨ T) and α(S) = α(T)

(Parallel)  S ∥ T ≡> φ_{∥}(S, T)

where φ_{∥}(S, T) ≡ ∃G ∃H (S{G/F } ∧ T {H/F }∧

G ∩ H ⊆ F ∧ (G ∪ H) − A ⊆ F)

and A = α(S) = α(T)

(Renaming)  S[b̄/ā] ≡> φ_{[ ]}(S, b̄, ā)

where φ_{[ ]}(S, b̄, ā) ≡ ∃t ∃G (S{t/h, G/F } ∧ t[b̄/ā] = h↓_{A}∧

G[b̄/ā] ⊆ F)

and A = α(S){b̄/ā}

(Hiding)  \begin{matrix}⊧ S\{F − B/F \} ⇒ T \\ ∀b ∈ B b ⊧ ¬∃F S \\ ∀tr ∈ α(S)^{∗} ∃n ≥ 0 ∀b_{1}, …, b_{n} ∈ B tr b_{1} … b_{n} ⊧ ¬∃F S \\ S \ B ≡> T \end{matrix}

where α(T) = α(S) − B and α(S) = A

(Recursion) \frac{P \{S/X\} ≡> S}{μX.P ≡> S} ,

where μX.P is a communication guarded closed mixed term and α(S) = α(X)

Table 1.

(Consequence)

⊧ S ⇒ T
Γ ⊢ P sat S
Γ ⊢ P sat T

, where α(S) = α(T)
(Deadlock)  Γ ⊢ stop_{A} sat h↓_{A} ≤ ε

(Prefix)

⊧ S{ε/h, {a}/F }
Γ ⊢ P sat S{ah/h}
Γ ⊢ a.P sat S

, where a ∈ α(S)

(Choice)

Γ ⊢ P sat S
Γ ⊢ Q sat T
Γ ⊢ P + Q sat φ_{+}(S, T)

, where α(S) = α(T)

(Parallel)

Γ ⊢ P sat S
Γ ⊢ Q sat T
Γ ⊢ P ∥ Q sat φ_{∥}(S, T)
(Renaming)  Γ ⊢ P sat S ; Γ ⊢ P [b̄/ā] sat φ_{[ ]}(S, b̄, ā)

(Hiding)

⊧ S{F − B/F } ⇒ T
⊧ S ⇒ ∀b ∈ B h↓_{A} ≠ b
⊧ S ⇒ ∃n∀b_{1} … b_{n} ∈ B^{∗} ¬∃F S{h b_{1} … b_{n}/h}
Γ ⊢ P sat S
Γ ⊢ P \B sat T ,

where α(T) = α(S) − B and α(S) = A

(Recursion)  Γ, X sat S ⊢ P sat S Γ ⊢ μX.P sat S ,

where μX.P is communication guarded and α(S) = α(X)

(Assumption) Γ, X sat S ⊢ X sat S , where α(S) = α(X) Table 2.

Lemma 4

(a) ⊧ S{ε/h, {a}/F } if and only if (ε, {a}) ⊧ S

(b) ⊧ S ⇒ ∀b ∈ B h↓_{A} ≠ b if and only if ∀b ∈ B b ⊧ ¬∃F S

(c) ⊧ ∃n∀b_{1} … b_{n} ∈ B^{∗} ¬∃F S{hb_{1} … b_{n}/h}

if and only if ∀tr ∈ α(S)^{∗} ∃n ≥ 0 ∀b_{1}, …, b_{n} ∈ B tr b_{1} … b_{n} ⊧ ¬∃F S

Corollary 5 Proof system for sat is sound, that is,

if ⊢ P sat S then R^{∗}[[S]] ⊑ R^{∗}[[P]]

Proof. Follows from Theorem 3 and soundness of proof system for ≡>. □ The converse of Theorem 3 also holds.

Theorem 6 (Relative Completeness) Let P be a process and Γ a set of assumptions such that P {Γ} is a closed term. If P {Γ} ≡> S for a specification S then Γ ⊢ P sat S.

Proof. The proof is long and is omitted due to space limitations. □ We end this section with the following useful observation

Proposition 7 If for a recursive term P a judgement Γ ⊢ P sat S can be derived for some S and Γ, then P ∈ Proc, that is, P satisfies the restrictions of Definition 2.

Proof. Follows by induction on the derivation of Γ ⊢ P sat S. □

4 Parametric Processes and Specifications

The triple (CProc, Spec, sat)

can be viewed as a specification system, in the sense of [Sokołowski 94]. We lift it to the parametric case by extending the process algebra with abstraction and application primitives, in a manner resembling the typed lambda calculus, where types are replaced with specifications.

First we introduce a syntactic class PSpec of parametric specifications ranged over by σ and defined by the following abstract syntax:

σ ::= S | σ → σ

Intuitively, specification σ_{1} → σ_{2} describes a set of parametric processes, each of which when given a process satisfying (possibly parametric) specification σ_{1} as an argument yields a process that satisfies specification σ_{2}.

The syntax of recursive terms is extended by adding two new clauses

P ::= … | λX : σ . P | P P

We consider the recursive terms up to α conversion, where λ as well as μ are variable binding operators.

The set of parametric processes will be defined as a subset of so extended recursive terms. In the case of nonparametric processes, syntactic restrictions enumerated in Definition 2 were used to distinguish the set Proc of processes in the set of (nonparametric) recursive terms. However, as it has been noted in Proposition 7, these restrictions are encoded also in proof system for sat. In the parametric case, it is more convenient to adopt a counterpart of Proposition 7 as a definition rather than separately formulate syntactic restrictions that define the desired set of parametric processes. This is the approach we are going to take, but first we need to refine some notions.

The notions of alphabet of a process and alphabet of a specification have to be extended to the parametric case. So far the alphabets were just finite subsets of Comm, the set of communications. Alphabets of parametric processes (and specifications), we shall call them hyper-alphabets in the sequel, have to be more complex objects, indicating the alphabets of possible arguments of a process. We define the set H of all hyper-alphabets as follows:

H_{0}  = set of finite subsets of Comm
H_{n+1} = {(A, B) | A, B ∈ H_{n}} ∪ H_{n}
H  = ⋃_{n=0}^{∞} H_{n}

Now, the hyper-alphabet α^{∗}(σ) of a specification σ is defined recursively by the following clauses:

\begin{matrix}α^{∗}(σ) = α(S), & if σ = S \\ α^{∗}(σ) = (α^{∗}(σ_{1}), α^{∗}(σ_{2})), & if σ = σ_{1} → σ_{2} \end{matrix}

The hyper-alphabet α^{∗}(P) of a recursive term P is defined by the clauses given below. If it is not possible to associate an alphabet with a term using these defining clauses, α^{∗}(P) is considered to be undefined. Just as in the nonparametric case we assume that every process variable X has an associated hyper-alphabet α^{∗}(X).

α^{∗}(X)  = the hyper-alphabet associated with X
α^{∗}(stop : A) = A
α^{∗}(a . P)  = α^{∗}(P) ∪ {a}  if α^{∗}(P) ∈ H_{0}
α^{∗}(P + Q)  = α^{∗}(P) ∪ α^{∗}(Q)  if α^{∗}(P), α^{∗}(Q) ∈ H_{0}
α^{∗}(P ∥Q)  = α^{∗}(P) ∪ α^{∗}(Q)  if α^{∗}(P), α^{∗}(Q) ∈ H_{0}
α^{∗}(P [b/a])  = (α^{∗}(P) − {a}) ∪ {b} if α^{∗}(P) ∈ H_{0}
α^{∗}(P \a)  = (α^{∗}(P) − {a})  if α^{∗}(P) ∈ H_{0}
α^{∗}(μX . P)  = α^{∗}(P) ∪ α^{∗}(X)  if α^{∗}(P) ∈ H_{0}
α^{∗}(λX : σ . P) = (α^{∗}(X), α^{∗}(P))  if α^{∗}(X) = α^{∗}(σ)
α^{∗}(P Q)  = B  if \begin{matrix}α^{∗}(P) = (A, B) \\ and α^{∗}(Q) = A \end{matrix}

Note that α^{∗}(P) = α(P) for P ∈ Proc and that alphabets of terms such as (λX : σ.P) + Q, where a process algebra operator + s applied to a higher order term, are not defined.

In the sequel we will consider only those recursive terms, whose hyperalphabets are defined, and the notion of recursive terms will refer to such terms from now on. The set of so understood recursive terms can be stratified into two subsets: the subset of terms whose alphabet is in H_{0} and to which process constructors +, a., ∥, \, [ ] and μ can be applied, and the subset of higher order terms, on which only abstractions and applications can be performed. Note however, that an application P Q, where P is a higher order term, can belong to the former subset and process algebra operators can be applied to it.

The syntactic notion of communication guardedness also needs to be redefined. Apart from conditions (1) and (2), we add the following point to Definition 1:

(3) X does not lie within a subterm of Q of the form RQ

Now we can formulate the proof system for the satisfaction relation sat extended to the parametric case. The judgements will have the form

Γ ⊢ P sat σ

where P is a (parametric) recursive term and the set of assumptions Γ is extended in the obvious way to contain assumptions of the form X sat σ.

The proof system contains all the rules collected in Table 2, which were used for nonparametric processes, but this time we assume that S and T range over nonparametric specifications, P and Q range over parametric recursive terms, Γ is extended as explained above, and the side conditions concerning alphabets refer to hyper-alphabets, i.e. α is replaced with α^{∗}. The side condition of communication guardedness in Recursion rule refers now to the modified version of this notion.

Moreover, the proof system of Table 2 is extended with the following rules, which are essentially λ-introduction and λ-elimination rules of the proof system for Church typed λ calculus (see for example [Barendregt 92]), plus a modified Assumption rule, which replaces the Assumption rule from Table 2.

(Assumption) Γ, X sat σ ⊢ X sat σ , where α^{∗}(X) = α^{∗}(σ)

(Abstraction)  \frac{Γ, X sat σ ⊢ P sat ρ}{Γ ⊢ λX : σ . P sat σ → ρ} , where α^{∗}(X) = α^{∗}(σ)

(Application)  \frac{Γ ⊢ P sat σ → ρ  Γ ⊢ Q sat σ}{Γ ⊢ P Q sat ρ}

Definition 8 The set of parametric processes PProc consists of those recursive terms P, for which Γ ⊢ P sat σ can be derived for some Γ and σ. CPProc, the set of closed parametric processes, is defined as the set of those parametric processes that have no free variables.

Note that the above definitions and Proposition 7 imply that Proc ⊆ PProc and CProc ⊆ CPProc.

We have just defined all components of a parametric specification system

(CPProc, PSpec, sat)

In this report we do not provide semantical account of parametric processes. This can be done by extending the readiness denotational semantics so that parametric processes are interpreted as process-valued functions on processes. Such a construction, which is an adaptation of a general procedure described in [Sokołowski 94], will be reported separately together with soundness proof of the proof system for sat . Here, we just show that the proof system respects β reductions.

Since parametric processes can be seen as lambda terms built on top of nonparametric processes, the notion of β-reduction can be defined in a standard manner:

(λX : σ . P) Q⟶^{β}P {Q/X}

We will use the same arrow ⟶^{β} to denote β-reducibility in possibly many steps. The next proposition ensures that sat is preserved by β reductions.

Proposition 9 If Γ ⊢ P sat σ and P ⟶^{β}P′ then Γ ⊢ P′ sat σ.

Proof. By induction on the derivation of Γ ⊢ P sat σ. □

Corollary 10 If P ∈ PProc and P ⟶^{β}P′ then P′ ∈ PProc.

In [Sokołowski 94] a special case of shallow parametricity is distinguished. A shallow n-parameter process has the form

λX_{1} : S_{1} … λX_{n} : S_{n} . P  (3)

This class of parametric processes corresponds to mixed terms of [Olderog 91]. The process term shown above can be syntactically translated into a mixed term

P {S_{1}/X_{1} , …, S_{n}/X_{n}}

Conversely, a mixed term P can be translated into a process having the form (3) by replacing every occurrence of any specification S_{i} appearing in P with a fresh variable X_{i}.

The following proposition shows that there is an exact match between the proof systems for ≡> on mixed terms and the proof system for sat on the restricted class of shallowly parametric processes.

Proposition 11 ⊢ λX_{1} : S_{1} … λX_{n} : S_{n} . P sat S_{1} → ⋯ → S_{n} → S if and only if P {S_{1}/X_{1} , …, S_{n}/X_{n}} ≡> S.

Proof. It can be show by induction that

⊢ λX_{1} : S_{1} … λX_{n} : S_{n} . P sat S_{1} → ⋯ → S_{n} → S

if and only if

S_{1} sat X_{1} , …, S_{n} sat X_{n} ⊢ P sat S.

By Theorems 3 and 6 this is equivalent to P {S_{1}/X_{1} , …, S_{n}/X_{n}} ≡> S. □

5 Example

We present here small example to illustrate the use of the proposed formalism: a task of constructing a counter of capacity 2. CNT2 below is a readiness specification of such a counter. Upon communication up (dn) the value stored in the counter is increased (decreased) by 1. The symbol up#h denotes the number of up communications in trace h.

CNT2 ≡ (0 ≤ up#h − dn#h ≤ 2) ∧ (up#h − dn#h < 2 ⇒ up ∈ F)∧
(up#h − dn#h > 0 ⇒ dn ∈ F)

The construction of process cnt2 such that

⊢ cnt2 sat CNT2

can be decomposed into constructing a counter of capacity 1, cnt1, and a parametric process mk-cnt2 that constructs a counter of capacity 2 given a counter of capacity 1:

⊢ mk-cnt2 sat CNT1 → CNT2

⊢ cnt1 sat CNT1

CNT1 is a specification of a counter of capacity 1:

CNT1 ≡ (0 ≤ up#h − dn#h ≤ 1) ∧ (up#h − dn#h = 0 ⇒ up ∈ F)∧
(up#h − dn#h = 1 ⇒ dn ∈ F)

Finally, the processes that realize the specifications can be defined as follows:

mk-cnt2 ≡ λX : CNT1 . (X[lk/up]∥X[lk/dn])\lk
cnt1  ≡ μX . up.dn.X
cnt2  ≡ mk-cnt2 cnt1

Using the proof system for parametric processes we can derive

⊢ cnt2 sat CNT2

as well as the remaining satisfaction assertions above.

Acknowledgement

We would like to thank Thorsten Altenkirch, Kārlis Černās and Uno Holmer for helpful comments on this work.

References

[Barendregt 92] H.P. Barendregt, Lambda Calculi with Types, in: Handbook of Logic in Computer Science, vol. 2 (S. Abramsky, Dov M. Gabbay, T. S. E. Maibaum, Eds.) pp. 117–309, Calderon Press, Oxford 1992.

[Holmström 89] S. Holmström, A refinement calculus for specification in Hennessy-Milner logic with recursion, Formal Aspects of Computing, vol. 1 (3). pp. 242–272, 1989.

[Larsen and Milner 86] K. Larsen and R. Milner, A Complete Protocol Verification using Relativised Bisimulations, R 86-12, Institute of Electrical Systems, Aalborg University Centre, 1986.

[Milner 89] R. Milner, Communication and Concurency, Prentice Hall, 1989.

[Olderog 91] E.-R. Olderog, Nets, Terms and Formulas, Cambridge University Press, Cambridge 1991.

[Olderog 91a] E.-R. Olderog, Towards a design calculus for communicating programs, in: Proc. CONCUR ’91, LNCS, Springer, 1991.

[Sokołowski 94] S. Sokołowski, The GDM approach to specifications and their realizations. Part I: Specification systems. Technical Report, Gdańsk, 1994.