论文部分内容阅读
在写出规格说明后,需要对规格说明的严密性进行证明,定理证明则可以消除规格说明中的模糊性和不一致性,从而验证规格说明是否满足用户需求.证明责任是从规格说明中产生待证的性质,该文描述了一个Z的证明责任产生器的工作过程.完成证明责任产生器的工作难点就在于如何生成证明责任,本文对这一工作进行了详细的介绍.