| 基于形式演算和不变式验证的可信算法程序构造 |
| |
| 引用本文： | 郑宇军,石海鹤,薛锦云,陈胜勇.基于形式演算和不变式验证的可信算法程序构造[J].中国通信学报,2011,8(4):58-64. |
| |
| 作者姓名： | 郑宇军 石海鹤 薛锦云 陈胜勇 |
| |
| 摘 要： |
|
| 收稿时间： | 2011-09-08; |
Formal Calculation and Invariant-Based Validation Establish Dependable Algorithmic Programs |
| |
| Zheng Yujun,Shi Haihe,Xue Jinyun,Chen Shengyong.Formal Calculation and Invariant-Based Validation Establish Dependable Algorithmic Programs[J].China communications magazine,2011,8(4):58-64. |
| |
| Authors: | Zheng Yujun Shi Haihe Xue Jinyun Chen Shengyong |
| |
| Affiliation: | 1College of Computer Science & Technology, Zhejiang University of Technology, Hangzhou 310023, Zhejiang Province, P. R. China
2provincial Lab of High-Performance Computing Technology, Jiangxi Normal University, Nanchang 330027, Jiangxi Province, P. R. China |
| |
| Abstract: | The paper presents a formal and practical approach to dependable algorithm development. First, starting from a formal specification based on the Eindhoven quantifier notation, a problem is regularly reduced to subproblems with less complexity by using a concise set of calculation rules, the result of which establishes a recurrence based algorithm. Second, a loop invariant is derived from the problem specification and recurrence, which certifies the transformation from the recurrence based algorithm to one or more iterative programs. We demonstrate that our approach covers a number of classical algorithm design tactics, develops algorithmic programs together with their proof of correctness, and thus contributes fundamentally to the dependability of computer software. |
| |
| Keywords: | formal methods algorithm calculation loop invariants program validation |
|
| 点击此处可从《中国通信学报》浏览原始摘要信息 |
|
点击此处可从《中国通信学报》下载全文 |
|
