1.2 代数规约简介

代数规约出现在20世纪70年代,作为一个正式的规范技术，用于指定数据结构在实现独立的风格。这种方法已经引起提供技术数据抽象，理论制定的一些规范的方法，规范属性分析，模块化发展，多层次组合。规范是建立在代数等式逻辑和底层语义是来自于代数，其中不同的数学结构，如基团，环和领域进行了研究。

形式化方法是以形式规约为基础,具有比较严谨的形式化理论基础，并支持保证程序正确性的系统开发方法.这种方法在理想情况下可以应用验证过的求精步骤从初始的形式规约推导出最终的可执行程序。

在过去的三十年代数规约方法在理论基础、语言、工具方面取得重大进展逐渐演化成为一种成熟的形式化方法。

1.3 论文主要工作

此次毕业设计主要研究开放云计算接口的代数规约描述技术，并用代数规约方法形式化描述软件系统。具体为：应用代数规约形式化方法描述开放云计算接口，从而发现自然语言描述中存在的不精确、模糊、不完整和不一致等错误。最终理解代数规约形式化方法和代数规约语言，描述云计算OCCI各类接口，并列出接口的代数规约描述。

1.4 论文组织安排文献综述

本论文分为四章节，第一章是引言，主要介绍论文课题的来源、研究内容、方向、研究内容的基本状况及论文安排；第二章介绍代数规约语言，包括代数规约理论及代数规约语言；第三章是代数规约在云计算接口OCCI（包括OCCI Core Model、Infrastructure和OCCI HTTP Rendering）上的运用，是本次论文的重点。第四章是结束语。

二  代数规约语言

2.1 代数规约理论

代数规约方法最早应用于定义抽象数据类型，一个抽象数据类型即一个代数表示，该代数由载体集合和建立在这些载体上的函数集构成。每个载体对应一个类型（type）,称为一个分类（sort）。

分类（sort）是分析阶段的概念，当基本类型作用于代数表达式时，称之为类子；类型是设计与实现阶段的概念。因此，一个软件实体的代数规约典型形式包括语法和语义两个主要部分。前者定义操作名和各操作的操作数和结果值的分类，即基调；后者通过一组以等式形式表示的公理集合定义操作必须满足的属性，即公理。

一个代数规约AS可以由一个二元组<∑,E>表示。∑=<sort，ops>被称为这个代数规约的特征（signature）。Sort是由分类组成的有限集合，ops是定义在分类之上的操作的有限集合。E是一组有限等式集合，称这些等式为公理。∑声明了代数规约的语法部分，指出了代数规约中使用的分类，并且定义了这些分类之上的操作。公理集合E是代数规约的语义部分，说明了∑中定义在分类之上的操作应满足的性质。

代数规约包含：分类名、可观察性、基调和公理。其中，分类名在指定的范围具有唯一性。如果一个分类定义了类似于比较两个同类型变量是否相等的操作，则该分类是可观察的，否则是不可观察的。基调包括操作集合定义，每个操作均由操作名、输入类型和返回值的类型构成，如果输入类型列表为空，则表明操作是常数。公理主要由变量及等式或者附带条件的等式构成，而且应用于等式中。

2.2 代数规约语言

常见的代数规约语言有OBJ3、CafeOBJ、CASL以及由CASL扩展的子语言，如CACOCC等。

CASL，由CoFI开发，是现在最常用的代数规范语言。它是一种偏向于解的语言，主要用于传统的软件设计。CASL汲取了许以前的规范语言精华，也开发了一些新的功能，从而让代数规约更简洁、更高效。它可能最终取代大多数以前的语言，并为未来的研究和发展提供一个共同的基础。