摘要
在写出规格说明后,需要对规格说明的严密性进行证明,定理证明则可以消除规格说明中的模糊性和不一致性,从而验证规格说明是否满足用户需求.证明责任是从规格说明中产生待证的性质,该文描述了一个Z的证明责任产生器的工作过程.完成证明责任产生器的工作难点就在于如何生成证明责任,本文对这一工作进行了详细的介绍.
A specifier must prove the rigor of a specification after he has written it. Theorem proving can eliminate inconsistency of a specification so that the specification can be verified with respect to the user requirements. Proof obligations are properties generated from the specification to be proven. The paper describes how a proof obligation generator works. The difficulty in developing a proof obligation generator lies in the generation of the proof obligations, which is discussed in this paper.
出处
《上海大学学报（自然科学版）》
CAS
CSCD
北大核心
2005年第5期495-499,共5页
Journal of Shanghai University:Natural Science Edition
基金
国家自然科学基金资助项目(60373072)
上海第四期重点学科建设资助项目
关键词
形式规格说明
验证
Z
证明责任
前置条件
不变式
formal specification
verification
Z
proof obligation
pre-condition
invariant
