近年来，为了保证各种软件的正确性和提高软件的可维护性、可重用性，人们对软件形式方法的研究越来越广泛和深入，形式方法的研究之所以能够迅速，除了因为其本身固有的优点，如精确、可以进行推理验证等，对形式方法的支持工具越来越多也是一个重要的原因。 本课题研究的是形式规格说明语言Object-Z的支持工具的集成的一部分——一个证明责任产生器。证明责任产生器的工作就是对规格说明进行动态检查，完成静态语法分析不能完成的工作，从而使规格说明的验证工作更加完善。而整个支持工具集成系统的完成，可以大大推广Object-Z，使其得到更广泛的应用，充分发挥它的优点。 本文从Obiect-Z的基本结构出发，提出了对规格说明产生证明责任的策略，从初始状态、前置条件、不变式、定义域检查这四个角度出发，验证规格说明初始状态的存在性、操作是否满足前置条件、操作结果是否满足不变式以及某些运算的操作数是否处于定义域中，从而实现对规格说明一致性的验证。同时，实现的工具提供了一个图形用户接口，用户可以通过该接口来输入自己想证明的性质，更进一步实施对规格说明一致性的验证。 本课题研究开发的证明责任产生器，以LATEX风格的Object-Z规格说明为输入，经过转换后产生证明责任，最终保存在”.tex”文件中，从定理证明器Z/EVES中导入即可证明。 由于采用了纯Java技术、Unicode码和字符流的输入输出方式，因此本软件是一个跨平台、跨语种的编辑器。只要通过Internet下载本软件，只要用户机器上有相应的Java虚拟机，就能够很容易地使用本软件。