逻辑程序综合的一种方法

木文给出逻辑程序综合的一种方法,按规范说明则p(X)Formula(X)中一阶公式Formula(X)的结构,反复运用变换规则,得到一个正确定义谓词p(X)Prolog程序。对于递归说明,也给出了相应的方法。     

OOZS：一种面向对象的Z语言扩展

在软件开发过程中，面向对象方法和形式方法的综合使用有助于充分利用这两种方法的优点并克服它们的不足。在Ｚ规格说明语言的基础上，作者设计了一种结构化的面向对象形式规格说明语言ＯＯＺＳ，以提高形式规格说明的层次性及模块化能力。本文简要介绍了ＯＯＺＳ语言的设计思想及其面向对象特征。     

抽象数据类型的PROLOG实现

抽象数据类型(abstract data type,以下简称ADT)和PROLOG都可作为数据类型的描述语言,本文旨在揭示二者间的关系。 本文给出ADT的形式定义及语义(执行策略),定义了一个证明系统用以表述执行策略,最后引入一个有效的从ADT到PROLOG的变换规则。     

面向对象的形式规格说明语言OOZS

ＯＯＺＳ语言是一种面向对象的形式规格说明语言,用于书写软件的形式规格说明。它是Ｚ语言的一种扩展,用以支持面向对象的软件分析方法,提供了类封装机制、类继承机制、和出口机制,设置了Ｐｒｅ谓词和Ｐｏｓｔ谓词,表达力强,简明精确。本文是该语言的试用文本介绍。     

Z规格说明求精的正确性判定

软件求精是自动推理和形式化开发方法相结合而形成的一门新技术,它研究从抽象的形式格说明推演出具体的面向计算机的程序代码的全过程.其基本思想是用·个抽象程度低、过程性强程序     

基于连接法定理证明器的PROLOG系统

本文介绍以连接法定理证明器为基础的PROLOG系统及其特点。     

Z规格说明中的定理证明方法

形式规格说明使用数学的表示,以一种精确的方法描述了系统要做什么,而不考虑它是如何做的。规格说明本身提供了一个无歧义的、能与用户和同事一起讨论的书面文件,又可作为已完成程序的文档,帮助人们将来进行程序的维护和修改。对形式规     

形式方法与面向对象方法的结合探讨

文中讨论了形式方法和面向对象方法各自的优缺点，结合作者设计的面向对象形式规格说明语言ＯＯＺＳ，介绍了将这两种方法结合起来的三种途径，并对这三种途径进行分析，评价和对比，最后提出了今后的研究方向。