Pages: 495-499
Year: 2005 Issue:  5
Journal: JOURNAL OF SHANGHAI UNIVERSITY (NATURAL SCIENCE EDITION)
Keyword:  形式规格说明; 验证; Z; 证明责任; 前置条件; 不变式;
Abstract: 在写出规格说明后,需要对规格说明的严密性进行证明,定理证明则可以消除规格说明中的模糊性和不一致性,从而验证规格说明是否满足用户需求.证明责任是从规格说明中产生待证的性质,该文描述了一个Z的证明责任产生器的工作过程.完成证明责任产生器的工作难点就在于如何生成证明责任,本文对这一工作进行了详细的介绍.