【一种自动程序综合的研究】玄顺姬.pdf
摘要 本文提出了一种软件设计规格描述语言SL、它以一阶谓词逻辑为 基础。本文还提出了基于定理证明的一种新的,把数学归 纳证明过程和简化证明过程配合使用,在证明过程中采取了假定与等值 替换并用的方法,SL语言有以下几个特点:它是一个面向软件 概要设计级的形式描述语言,它能刻划出程序“做什么”的功能规格说 明,而不是“如何做”的算法.采用一阶谓词逻辑描述程序规格.本系统采用的定理证明方法分三步进行:公式化简,公式 分解,公式证明。
目 第一章 前言 .1 引言 .1 相关工作 .1 本文 第二章 软件规格描述 s2 软件规格描述言 2 规格描述语言(SL)说明 2 SL规格描述语言的例子 S2 小结 第三章 定理证明系统 .3 机器证明的数学归纳法 3 基本概念 3 归纳法原理 3 定义原理 .3 定理证明系统 3 类型信息与简化 3 项的重写简化 3 删除不必要的项及表达式 3 使用等式 3 用归纳与递归原理分解公式 3 证明公式 3 机器证明的一个例子 S3 小结 第四章 程序抽取技术 .4.
第一章前言 .1引言 随着计算机科学的不断发展以及软件技术的不断提高,软件的形式 化开发和软件设计的自动化越来越受到人们的关注,也是计算机科学研 究中人们感兴趣的一个研究课题 近几十年来,计算机科学有了长足的进步,尤其是计算机硬件能力 得到很大提高,不断推出功能强大、更新换代的新产品,而软件的生产 相对发展较慢,远远不能适应客观需求,出现了所谓的“软件危机”,目前,软件领域存在三大问题,即功能不强、质量欠佳、生产率低。为 了从根本上解决这些问题,必须研究软件工程新技术,如集成化技术、自动化技术及智能化技术等,其中软件自动化是提高软件生产率的根本 途径 早在五十年代,程序人员从程序设计实