论文部分内容阅读
本文主要研究了软件需求规格说明的一种验证方法——定理证明技术，研究开发PVS-Z定理证明原型系统。该系统能够对Z规格说明的定理进行证明，从而实现对规格说明的验证。首先，在PVS系统中定义Z的类型和运算操作符，并且形式地推导了Z的基本定律，用户可以在以后的证明过程中使用这些Z定律而无需知道它的语义，从而建立了Z的工具库。其次，在应用研究部分，我们根据Z规格说明语言的语法语义，制定了一系列由Z规格说明到PVS规格说明的转换规则。通过转换，可将Z的规格说明以PVS的理论形式表示出来，为定理证明做准备工作。最后利用PVS-Z定理证明原型系统，对规格说明的定理进行证明。通过具体实例验证本系统能够有效地证明Z规格说明的相关定理，实现了对规格说明的性质的验证。