Object-Z编辑器的分析、设计和实现

摘要

该文介绍了一个用JDK1.2.2编写的Object-Z编辑器的核心部分,通过Object-Z编辑器的帮助,用户可以很容易地以图形化的方式输入Box风格的Object-Z规格说明.通过转换引擎的帮助,用户可以立刻得到和Box风格相对应的Latex风格的Object-Z规格说明.由于Box风格具有直观、易于被使用者接受的特点,所以特别适合作为规格说明编写者与用户间交流的媒介;由于Latex风格是纯文本的,所以特别适合进行词法和语法分析,通过该编辑器,这两个优点体现在该编辑器中,因此用户可以在一个界面下完成规格说明编写、修改和检测查错这三个步骤.该Object-Z规格说明编辑器是基于Object-Z的软件规格说明的构造环境,也是该课题组正在开发的基于Object-Z规格说明的软件测试工具的前端部分,它可提供原始的Latex风格的Object-Z规格说明.该规格说明编辑器还提供了对生成测试用例程序的调用,这样用户可以容易地通过编辑的Object-Z规格说明得到他所需要的测试用例.

目录

文摘

英文文摘

致谢

第一章引言

1.1.形式方法

1.1.1.形式方法简介

1.1.2.形式方法的分类

1.1.3.形式方法的主要优点

1.1.4.软件规格说明的分类

1.2.规格说明语言Object-Z

1.2.1. Z及其扩展

1.2.2. Object-Z

1.3.基于规格说明的软件测试

1.3.1.基于规格说明的测试构成

1.3.2.驱动测试

第二章需求分析与需求定型

2.1.整体分析与需求定义

2.1.1.用户需求分析与确定

2.1.2.Object-Z编辑器的系统需求分析与确定

2.2.需求定型

第三章核心设计

3.1.核心框架的问题分析

3.2.Java的JFC类库及可能的解决方案

3.2.1.Java的Swing类库介绍

3.2.2.Swing组件的体系结构：

3.2.3.利用Swing类库进行核心设计的两种可行方案及其比较

3.3.最终核心方案

3.3.1.需求细化与总体设计思路

3.3.2.布局管理器的深入设计以及布局算法

3.3.3.基于多态的动作序列与核心框架设计

第四章Object-Z特殊符号输入的解决

4.1.有关Uni code码

4.2.Unicode码与Object-Z特殊字符的映射

4.3.Object-Z特殊字符与Latex的映射

第五章Object-Z编辑器的功能介绍

第六章结论与展望

参考文献