代数规约是一种独立于软件实现的描述软件系统的形式化方法，本文介绍一种面向服务的代数规约语言Sofia，设计并实现了Sofia代数规约语言解析工具，通过解析工具检查代数规约的语法错误。

毕业论文关键词：代数规约，解析工具，JavaCC，Sofia 60981

The design and implementation of algebraic specification language parsing tool

Algebraic specification is a formal specification technique for specifying software systems in an implementation-independent style. 

In this paper, we introduce an algebraic specification language named Sofia and focus on the design and implementation of algebraic specification language parser. By the parser, we can check whether there is in the algebraic specification language syntax errors.

Keywords: Algebraic specification,  Parser tools, Sofia, JavaCC

目录

一、引言5

1.1 代数规约语言.5

1.2 解析器.5

1.3 论文主要工作.5

1.4 论文组织安排.5

二、代数规约语言Sofia文法6

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

2.2 Sofia规约的总体结构.6

2.3 signature的语法和语义7

2.4 公理的语法和语义10

2.5总结.11

三、面向Sofia的解析工具设计和实现.12

3.1 JavaCC12

3.2 数据结构设计.13

3.3 Token18

3.4 代码功能详细20

3.5界面截图.32

四、结论.34

五、结束语.34

六、致谢及参考书目35

1.1 代数规约语言

代数规约方法早在上个世纪七十年代提出，是以一种独立于软件实现的风格定义抽象数据的形式化方法。在过去三十年，代数规约方法在理论基础、语言、工具方面取得重大进展，逐渐演化成一种成熟的形式化方法。

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

在理论方面，代数规约引入隐代数、行为理论、范畴、共轭代数、规范机制等概念与理论。在语言方面，已提出OBJ3/CafeObj、CASL等代数规约语言以满足抽象数据类型、组件、不确定的并发系统与Web服务的需要。

基于代数规约的测试方法的最有吸引力的特点是它支持自动化测试软件系统，能够自动生成测试用例并成功解决驱动和测试结果检查等问题。因此，基于代数规约的测试理论、技术与方法得到不断发展。

代数规约除了用于测试领域外，它还支持规约形式化求精、需求定义、程序证明、程序的正确性求精、形式推理、逆向工程和软件测试等形式化的软件开发活动。代数方法提供一个严格的方法的重要基础并支持大型系统的软件工程的机械支持。

1.2 解析器

一般来说，解析器就是判断输入的字符串是否满足给定的语法规则，在需要时还可以提取出相应的语法单位实例的工具。本文中所用到的解析器使用JavaCC编写的。

解析器的输入包括若干行序列，每行都包含一个表达式，一般是一些抽象的表示。

解析器的输出并不是由JavaCC 规定的，并非程序员想让它输出什么它就什么样，只能用Java 表示出来。

编译器中，解析器的输出可能是机器码或汇编码的形式。大多数编译器的解析器会生成输入程序的某种中间代码，这些中间代码表示日后会被编译器的其他部分用到。不同的应用会有不同的输出形式。

1.3 论文主要工作

此次毕业设计主要设计和实现代数规约语言解析工具，在理解代数规约语言的基础上，基于JavaCC，实现代数规约语法检查动能和类型检查功能。