1.4 论文组织安排

本论文分为四章，第一章引言，简要介绍代数规约、解析工具以及论文主要工作；第二章详细介绍代数规约语言Sofia的文法；第三章给出Sofia解析工具的设计和实现。第四章是感悟。第五章是结束语。最后是参考书目。

二、代数规约语言Sofia文法

2.1 面向服务的代数规约语言

在面向服务的计算中，发现和动态组合服务必须建立在准确的机器理解的语义服务之上。Sofia语言就是因此而被设计出来。它基于代数规约的理论，代数规约包括行为和代数上的处理。本章首先介绍Sofia中规约的整体结构和各种不同类型的规约单元，然后介绍signatures的语法和语义，接着描述公理的语法和语义，最后给出Sofia总结。

2.2 Sofia规约的总体结构

2.2.1规约单元的类型

    一个Sofia的规约包括一系列的规约单元，一共定义四种单元如下：

<Specification> ::= <Unit>*

<Unit> ::= <Spec Unit>

         | <Signature Unit>

         | <Axiom Unit>

         | <Definition Unit>

一个<Spec Unit>是一个完整的规约，用来指定一种类型的软件实体和系统。每一个实体就是一个type的实例，它可以是一个数据类型，一个类，一种构件或一种Web服务等。每一个规约单元包括两个主要部分：一个signature和一套公理，其BNF表示如下：

<Spec unit> ::=

  Spec <Sort Name> [<Observability>];

      [extends <Sort Names>]

      [uses <Sort Names>]

      <Signature>;

      [<Axioms>]

  End

<Sort Name>的位置是用来命名单元的标识符。它与被标明的软件实体一致。它被称作单元的主sort。

规约单元可以被分解为两个部分。一个Signature单元和一个公理单元。这两个有同一sort名称的单元组合在一起相当于一个带有一致性signature和公理的完整规约。

<Signature unit> ::=

  Signature <Sort Name> [<Observability>];

      [extends <Sort Names>]

      [uses <Sort Names>]

      <Signature>

  End

<Axiom Unit> ::=

  Axioms <Sort Name>;

     <Axioms>

  End

除规约单元之外，Definition单元定义了一系列的用在规约中的辅助性功能和概念。

<Definition unit> ::=

   Definition [uses <Sort Names>]

        <Signature>;

        [<Axioms>]

   End

Signature部分定义了语法方面的功能和关系，同时公理定义了语义。本文只介绍Signature部分。

2.2.2 Units之间的关系

规约单元之间存在两种关系：uses关系和extension关系。他们分别在<extends>和<uses>语句中被清楚地罗列出来。在关键字uses后面的一系列sort名称给出了当前正在用的sorts。这些sorts在规约中被用作操作的参数或者结果。指定的单元也含有被用过的sorts的成分。在语法上，<Sort Name>是sort名称分隔罗列构成的列表。

<Sort Names>::= <Sort Name>[, <Sort Names>]

<Sort Name>::= <Identifier>

Extention关系和类之间的继承关系相同。换句话说，如果sort A的规范扩展 sort B，那么sort B里面的常量、变量、操作、公理等同样包含在sort A里面。同时，sort A里还有明确标明的附加内容。