形式化方法是目前兴起的一种很重要的软件开发方法。代数规格说明可以应用于形式化方法。它用一组代数公理来刻画对类操作行为的需求,它提供了一种形式化的手段,使人们能够把类的实体的需求说明较严谨地描述出来。在基于代数规格说明的面向对象类级的软件测试研究中,代数规格说明作为一个基本的已知条件必须首先构造出来。公理系统是一个代数规格说明的最主要部分,它描述需求的语义,它必须具有独立性、一致性和完整性。本课题基于代数规格说明的独立性、一致性和完整性来完成代数规格说明中公理的辅助构造工具的设计和实现,包括对原有方案CLA作了某些局部性修改;较详细地分析和阐述了方案CLA所枚举的公理左边的所有可能的模式的理由;在代数规格说明公理系统一致性和独立性原有的形式化定义和命题的基础上,提出了判断这种公理系统一致性和独立性的一个半自动化近似算法;对这两者作了实现和实验。以期提高构造代数规格说明的效率,节约形式化软件开发的成本,舒缓产业界人士对构造公理的困难。