Formal Calculation and Invariant-Based Validation Establish Dependable Algorithmic Programs

摘要：

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 regu-larly 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 al-gorithm design tactics, develops algorithmic pro-grams together with their proof of correctness, and thus contributes fundamentally to the dependability of computer software.

关键词： formal methods algorithm calculation loop invariants program validation

作者: Zheng Yujun Shi aihe Xue Jinyun Chen Shengyong

作者单位: College of Computer Science & Technology,Zhejiang University of Technology,Hangzhou 10023,Zhejiang P Provincial Lab of High-Performance Computing Technology,Jiangxi Normal University,Nanchang 330027,Ji Provincial Lab of High-Performance Computing Technology, Jiangxi ormal niversity,Nanchang 330027,Jia College of Computer Science & Technology, Zhejiang University of Technology, Hangzhou 310023, Zhejia

会议类型: 国际会议

会议名称: 2011年中国计算机学会服务计算学术会议(CCF NCSC2011)

会议地点: 济南

会议语种:英文

页码: 58-64

在线出版日期: 2011-08-18（万方平台首次上网日期，不代表论文的发表时间）