![](https://csdnimg.cn/release/download_crawler_static/88746748/bg4.jpg)
M.A.
巴博萨
Barbosa/Electronic Notes in Theoretical Computer Science 175
(
2007
)
39
相关的问题是,应该使用什么样的形式主义来具体
说明使用模式
?转换系统
[19
,
29]
,正则表达式
[25
,
26
,
31]
或进程代数
[18
,
3]
是通常用于表示行为的形式
结构的巨大多样性的一部分,这也在
Web
服务的形式化中进行了探索。进程代数,
特别是,提供了一个表现性的设置表示行为模式,并建立
/
验证其属性的组合方式。
然而,对于底层的交互规则,需要一定的灵活性。实际上,必须同时使用不同的此
类规程来捕获Web服务编排的不同方面。例如,管理它们之间的
软件连接器
的组成
(以构建整体
粘合代码
)的规则与用于捕获后者和相关Web服务接口之间的交互的
规则不同。在任何情况下,我们都需要一种方法来指定相关的交互规则,同时保证
所使用的行为组合子是
参数化的
,满足这个目标需要一种
通用的
方法来
设计
过程代
数。我们以前在经典过程演算的共代数重构方面的工作,在[7,8]中有记录,提供
了必要的成分。在下面的小节中简要回顾了这项工作,这为讨论其在Web服务编排
上下文中的应用铺平了道路
2.2
通用进程代数
参考文献
[7
,
8]
介绍了一种设计进程代数的指称方法,其中进程被标识为最终余代
数
[17]
的居民,并且它们的组合子由(
“
一步
”
行为生成器函数的)共归纳扩展定义这
种构造的
普遍性
需要定义和证明原则,整个微积分的发展都是基于
这些
原则。
从技术上讲,这相当于系统地使用了共归纳扩张的普适性质。 也就是说, 对于
每个任意余代数
<$U
,
p
:
U
−→
P(
Act
×
U
)
<$
,存在唯一的到最终余代数
ω
:
ν
−→
P(
Act
×
ν
)的态射
[
(
p
)
]
,满足
k= [(p)] ⇔ ω ·k=P(id
×
k)·p
(
1
)
其 中 P是 有 限 幂 集 函 子
5
。 因 此 , 由 于 过 程 是 最 终 余 代 数 的 居 住 者 , 表 达 式 P
(Act
×
v)代表一组对,每一对代 表一个转移和 一 个 相 应的延续过程 。 这 样 的
[(p)]表示由p产生的行为,并配备了一系列在计算中有用的定律。
[
4
]
与范畴论所要求的
无点
在函数式编程的
双重
T. Hagino [15].
[5
]
这个定义当然可以推广到任意的余代数。