循环结构的形式化推导

• 作者: 吴茂念 李贤贞 杨静
• 来源期刊: 微型机与应用
• 学科: 工学
• 关键词: 形式化方法 程序正确性 循环不变式 界函数
• 年，卷（期）: 2014,（5）
• 所属期刊栏目: 技术与方法
• 页码范围: 82-83,86
• 页数: 3页
• 分类号: TP301
• 字数: 2160字
• 语种: 中文

摘要

介绍了 Dijkstra 的形式化推导方法的主要思想、步骤及要点。该方法主张程序开发和程序证明同时进行，先确定好描述程序功能的断言，再通过形式化方法推导出正确的程序。选择具有代表性的循环结构的实例进行推导证明，并对循环结构的形式化推导进行阐述说明。

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	杨静	贵州大学计算机科学与信息学院	45	178	7.0	11.0
2	吴茂念	贵州大学计算机科学与信息学院	14	39	3.0	5.0