摘要
介绍了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.
出处
《微型机与应用》
2014年第5期82-83,86,共3页
Microcomputer & Its Applications
基金
国家自然科学基金项目(61262029)
关键词
形式化方法
程序正确性
循环不变式
界函数
formal methods
program correctness
loop invariant
boundary function
