一个Z的证明责任产生器  

A Proof Obligation Generator for Z

作　　者：沈毅[1] 缪淮扣[1] 文志诚[1] 陈怡海[1] 

机构地区：[1]上海大学计算机工程与科学学院,上海200072

出　　处：《上海大学学报（自然科学版）》2005年第5期495-499,共5页Journal of Shanghai University:Natural Science Edition

基　　金：国家自然科学基金资助项目(60373072);上海第四期重点学科建设资助项目

摘　　要：在写出规格说明后,需要对规格说明的严密性进行证明,定理证明则可以消除规格说明中的模糊性和不一致性,从而验证规格说明是否满足用户需求.证明责任是从规格说明中产生待证的性质,该文描述了一个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.

关 键 词：形式规格说明 验证 Z 证明责任 前置条件 不变式 

分 类 号：TP311[自动化与计算机技术—计算机软件与理论]