用Petri网描述程序精化中的循环不变式

摘要：

形式化方法把程序看成规范,形式化开发方法包括形式规范和规范(程序)的精化.精化演算方法能够通过演算的方式,把规范逐步精化为程序.然而,演化的过程依赖于开发人员的经验,整个过程全部都是手动的.形式化方法的最高目标是软件自动化,使得能从规范自动开发出正确的程序.因而用Petri网来描述程序精化中的循环不变式,希望以此作为软件自动化的一个探索.

关键词：程序精化、循环不变式、Petri网

所属期刊栏目：1

分类号：TP393(计算技术、计算机技术)

在线出版日期：2012-03-05（万方平台首次上网日期，不代表论文的发表时间）

页数：共3页

页码：14-15,19