VarDeclarations表示变量声明，通常是全局变量，由一对变量名和它的类型组成，下面是它的语法：

<SortName>为变量类型，<VarID>为变量标识符，下面是一条公理的例子：

即定义StackService类型的变量S，ReplaceRequest类型的变量X，对于所有的S，X，当S。length>0，符合：S;replace(X)。top = X。value。

在SOFIA语义中有一个重要概念term，它是基于代数规约的Web服务测试技术的基础，每一个条件等式由一对term组成，term的语法如下：

每个term由操作子构成，SOFIA语言的操作子有三类：

常操作子（由Const声明，如上例中的nil，表示生成一个空栈），表示规约单元的构造操作； 

可观察操作子（也被称为属性操作子，由Attribute声明，如上例中的isEmpty、top和length操作，分别表示当前堆栈是否为空、栈顶元素和长度），表示规约单元使用到的数据类型；

转换操作子（由Operation声明，如上例中的push和pop操作，分别表示在堆栈中压入和弹出元素），表示会改变规约单元状态的操作。 

下面是一个term的例子。

pop(push(pop(push(s,n)),m))为一个term，其中，push(pop(push(s,n)),m)也为一个term，它又包含pop(push(s,n))这个子term，同样，这个子term又包含自己的子term。

Term是生成测试序列的基础。

2。3  主流Web服务

2。3。1  什么是Web Service

Web Service是对软件开发中面向对象设计的发展和升华，它具有高度可复用性，作为软件模块参与到分布式计算中。Web Service是松散耦合的，其开放的标准以及一些服务提供者达成的共识，使得其成为应用集成的平台。开发者可以通过整合不同来源的Web Service来构造自己的应用，而不用知道这些Web Service位于何处以及如何实现。从另外一个角度讲，也可以说Web Service就是服务提供者通过某些协议提供的远程调用接口。

2。3。2  基于SOAP的Web Service

目前主流的Web Service是基于SOAP+WSDL的。下面分别介绍相关协议、技术。

2。3。2。1 SOAP协议

W3C组织提出并倡导了一系列协议，以规范Web开发方式。简单对象访问协议（Simple Object Access Protocol）就是其中一部分。SOAP是一个轻量级协议，提供了在 分布式的环境中如何 的解决办法。SOAP完全基于XML的特点，使它可以实现异构通信，包括不同的语言、不同的计算机体系结构、甚至不同的操作系统。

SOAP消息含有三个部分：来*自~优|尔^论:文+网www.youerw.com +QQ752018766*

封装(Envelop元素)：由于Envelop元素是最上层元素，所以一个SOAP消息必须有Envelop元素。它说明了一个框架，描述消 容、由谁发送、谁应 它以及如何处理它们；

报头（Header元素）：一个SOAP消息可以没有报头。它的作用是为SOAP消息附加额外属性。即使没有得到通信双方事先同意，报头元素也可以附加额外属性。开发者可以用这种方式按照自己需要扩充SOAP消息。

报体（Body元素）：SOAP消息必须有报体元素，它记录了目标节点信息。