《程式正確性證明方法》是2018年12月上海財經大學出版社出版的圖書，作者是武斌。
基本介紹
- 書名：程式正確性證明方法
- 作者：武斌
- ISBN：9787564231699
- 定價：39元
- 出版社：上海財經大學出版社
- 出版時間：2018年12月
- 開本：16開
內容簡介,圖書目錄,
內容簡介
程式驗證是電腦程式設計領域的前沿研究課題，如何保證程式正確性是計算機科學的一個重大挑戰。本書在前人研究的基礎上，利用符號計算的思想和方法研究了程式驗證領域的三個基本問題：循環不變式生成、程式終止性分析以及前置條件生成。本書主要研究了多項式循環程式的不變式生成問題。首次將有限點集消去理想的思想和方法套用於多項式循環程式的不變式生成，設計了一個多項式時間複雜度的循環不變式自動生成算法，可生成多項式等式型循環不變式。
圖書目錄
前言 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
