基于代数规约的Web服务测试执行技术研究(4)
2）基于逻辑的方法：主要思想是用逻辑的方法描述系统预期的性能（系统性能包括时序、底层规约和可能的行为）。主要形式是使用公理系统（与所选逻辑相关）证明系统是否达到预期的性能。
3）代数方法：主要思想为将未定义状态下不同的操作行为联系起来，主要做法是给出操作的显式定义。与基于模型的方法类似，代数方法并不能显式表示并发状态。
4）过程代数方法：主要思想为限制所有容许的可观察的过程，并用它们之间的通信表示系统行为。过程代数方法支持显式表示并发过程。
5）基于网络的方法：主要思想是使用具有形式语义的图形语言描述系统。因为图形化表示法易于理解，而且非专业人员能够使用，因此使系统确定表示法被广泛应用于开发过程中。
2。2 代数规约语言
20世纪70年代，代数规约技术开始出现，它采用独立于实现的方式定义抽象数据类型，用公理集的方式描述抽象数据类型的约束。基于代数规约的测试方法，由于其设计与实现独立于软件系统，且在自动生成测试用例、提供测试驱动和判断测试输出等方面有独到之处，已经被研究人员应用于测试工作。可以测试的对象有：抽象数据类型、类、过程、Web服务和组件等[8]。
代数规约由数个软件实体集构成（抽象数据类型、类、服务，甚至现实世界中的物理对象、数据、过程等，都可以视为软件实体），软件实体由规约单元描述。这样的话，一个描述Web Service的代数规约就可分解为数个规约单元。规约单元用Sort描述，Sort也被称为类子，是规约单元的唯一的标识。类子包括基调（Signature）、公理集（Axiom）两部分。基调为定义在类子上的操作集（Operators），公理集为操作的语义约束。此外，新的规约单元可以通过扩展（extends）和使用（uses）两种方式重用已有的规约单元。
本文所构建的测试执行框架所使用的代数规约语言为SOFIA语言。
SOFIA语言拥有之前提到的代数规约语言的共有特点，整体结构为一组规约单元，而规约单元分为两个部分：基调单元（Signature）和公理单元（Axiom）。此外，SOFIA的规约单元还有定义（Definition）部分，用户可以在此部分定义规约的辅助函数和概念。下面以Stack服务为例介绍SOFIA语言。
Stack服务提供简单的堆栈服务，操作有PUSH、POP、REPLACE。
Spec StackService;
uses PushRequest, PopRequest,ReplaceRequest,
PushResponse, PopResponse,ReplaceResponse,
Integer,Bool;
Const:nil;
Attr
isEmpty:Bool;
length: Integer;
top: Integer;
Operation
push(PushRequest): PushResponse;
pop(PopRequest):PopResponse;
replace(ReplaceRequest): ReplaceResponse;
Axiom
nil。isEmpty = True;
nil。length = 0;
For all S : StackService ,X : PopRequest that
S。isEmpty = True, if S。length = 0;
S;pop(X)。length = S。length-1, if S。length>0;
End
For all S : StackService, X: PushRequest that
S;push(X)。isEmpty = False;
S;push(X)。top = X。value;
S;push(X)。length = S。length+1;
End
For all S : StackService, X : ReplaceRequest that
S;replace(X)。top = X。value, if S。length>0;
EndEnd
Spec为SOFIA语言的基本语句段，相对于代数规约的规约单元。Uses部分描述本规约单元用到的数据类型，可以为基本数据类型，如integer、bool，也可以为复杂数据类型，如PushRequest（PUSH操作的请求信息）。Const部分描述本规约单元使用的固定部分，nil表示栈的初始状态（空栈）。Attr可以简单的理解为局部变量。Operation描述规约单元的操作集，在此规约单元中包括PUSH、POP、REPLACE操作。push(PushRequest): PushResponse表示push操作以PushRequest为输入，PushResponse为返回。Axiom描述操作的语义约束。Axiom的BNF（Backus-Naur Form）表示为：文献综述