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

Model Loop Invariant in Software Refinement by Petri Net

作　　者：方静[1] FANG Jing（Modern Educational Technology Center;North China Institute of Science and Technology;Sanhe Hebei 065201;China）

机构地区：[1]华北科技学院现代教育技术中心,河北三河065201

出　　处：《智能计算机与应用》2011年第4期14-15,19,共3页Intelligent Computer and Applications

摘　　要：形式化方法把程序看成规范,形式化开发方法包括形式规范和规范（程序）的精化。精化演算方法能够通过演算的方式,把规范逐步精化为程序。然而,演化的过程依赖于开发人员的经验,整个过程全部都是手动的。形式化方法的最高目标是软件自动化,使得能从规范自动开发出正确的程序。因而用Petri网来描述程序精化中的循环不变式,希望以此作为软件自动化的一个探索。Formal method looks program as specification,and it includes formal specification and specification refinement.Refinement calculus can refine specification to program step by step by a calculus method.However,the refinement process depends on the experience of developers,and it is totally manual.The highest aim of formal method is software automation,so that correct program can be produced automatically from specification.This paper models loop invariant by Petri Net and starts a beginning exploration of software automation.

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

分 类 号：TP393[自动化与计算机技术—计算机应用技术;自动化与计算机技术—计算机科学与技术]