================================================================================
P9317   S.F.M. van Vlijmen & J.J. van Wamel
        "A semantic approach to Protocold using process algebra"


We study of the operational behaviour of the specification language
Protocold. We examine whether BPAb (Basic Process Algebra with backtracking)
forms a useful basis for a clear representation of the execution of certain
language constructs from Protocold.
Our primary focus is on those constructs that contain some form of
backtracking. Backtracking in Protocold contains the undoing of bindings
of object names (logical variables).

We first provide a short introduction to both formalisms, and then make a
rough comparison of them both. Some elementary Protocold features, such as
object names and the binding of object names, are then defined relative to
a special data environment for BPAb.
Finally, a small language PCl is defined for the description of the
operational behaviour of Protocold-like expressions, as well as a mapping
from Sig(PCl) expressions to Sig(BPAb) terms.
Some operational equivalences that hold in Protocold are defined as rules
in PCl, such that algebraic manipulation of Sig(PCl) expressions is possible.
Normal forms over Sig(PCl) are defined, and it turns out that a mapping of
these normal forms to Sig(BPAb) terms preserves some typical properties
of backtracking in PCl.
A canonical mapping does not exist, however, because backtracking in a
Protocold (and Sig(PCl)) expression is `global': it is not limited to the
scope of certain operators.

We think that, although the language Protocold is too rich to be fully
expressed in terms of BPAb (particularly where the specification of
abstract data types is at stake), the operational behaviour of Protocold
specifications can be specified adequately in BPAb.