循环结构的形式化推导  

Formal derivation method of repetitive construct

作　　者：李贤贞[1,2] 吴茂念[1] 杨静[1] 

机构地区：[1]贵州大学计算机科学与信息学院,贵州贵阳550025 [2]中国科学院国家天文台,北京100012

出　　处：《微型机与应用》2014年第5期82-83,86,共3页Microcomputer & Its Applications

基　　金：国家自然科学基金项目(61262029)

摘　　要：介绍了Dijkstra的形式化推导方法的主要思想、步骤及要点。该方法主张程序开发和程序证明同时进行,先确定好描述程序功能的断言,再通过形式化方法推导出正确的程序。选择具有代表性的循环结构的实例进行推导证明,并对循环结构的形式化推导进行阐述说明。This document introduces the basic theory of Dijkstra′s formal derivation method, which be of the view that the development and demonstration of programs processed simultaneously,confirming the assert of describing the function of the program, and then deduced a correct and proper algorithm formally. And this document is added a representative example of struct to illustrate the theory.

关 键 词：形式化方法 程序正确性 循环不变式 界函数 

分 类 号：TP301[自动化与计算机技术—计算机系统结构]