开云网页版_开云(中国)

首页 > 图书中心 > 学术著作 > 学术 > 经济学

程序正确性证明方法-武斌

丛书名：
著（译）者：武斌
资源下载：无资源下载
责任编辑：柳萍萍
字       数：124千字
开       本：16 开
印       张：8
出版版次：1-1
出版年份：2018-12-01
书       号：978-7-5642-3169-9/F.3169
纸书定价：39.00元   教师会员可用500积分申请样书

在线购买样书申请收藏分享按钮

程序验证是计算机程序设计领域的前沿研究课题，如何保证程序正确性是计算机科学的一个重大挑战。本书在前人研究的基础上，利用符号计算的思想和方法研究了程序验证领域的三个基本问题：循环不变式生成、程序终止性分析以及前置条件生成。本书主要研究了多项式循环程序的不变式生成问题。首次将有限点集消去理想的思想和方法应用于

同系列产品more >

: 亚洲新兴经济体国
孙立行
定价：28.00元
查看详情

: 2018中国财政透明
上海财经大学公共政策与研究中心
定价：68.00元
查看详情

: 合作团队的经济学
张军
定价：65.00元
查看详情

: 全国投资与建设研
黄汉江
定价：96.00元
查看详情

: 中外旧约章汇编
王铁崖
定价：1280.00元
查看详情

图书分类全部图书

程序验证是计算机程序设计领域的前沿研究课题，如何保证程序正确性是计算机科学的一个重大挑战。本书在前人研究的基础上，利用符号计算的思想和方法研究了程序验证领域的三个基本问题：循环不变式生成、程序终止性分析以及前置条件生成。本书主要研究了多项式循环程序的不变式生成问题。首次将有限点集消去理想的思想和方法应用于多项式循环程序的不变式生成，设计了一个多项式时间复杂度的循环不变式自动生成算法，可生成多项式等式型循环不变式。

前言 1

第一章　绪论 1
　1.1　程序正确性研究方法概述 3
　1.2　程序正确性研究概况 9
　1.3　符号计算简介 15

第二章　循环不变式的自动生成 22
　2.1　参系数半代数系统的实解分类及应用 23
　2.2　有限点集消去理想的Gröbner基 31
　2.3　基于消去理想的循环不变式自动生成 38
　2.4　本章小结 56

第三章　一类非线性循环程序的终止性分析 62
　3.1　齐次多项式函数循环条件的程序终止性分析 63
　3.2　一般情形 71
　3.3　本章小结 80

第四章　循环程序终止的前置条件的自动生成 81
　4.1　差分方程组的求解 82
　4.2　前置条件的自动生成算法 90
　4.3　本章小结 103

第五章　结束语 108

参考文献 110

致谢 130