| 用Petri网描述程序精化中的循环不变式 |
| |
| 引用本文： | 方静.用Petri网描述程序精化中的循环不变式[J].电脑学习,2011(4):14-15,19. |
| |
| 作者姓名： | 方静 |
| |
| 作者单位： | 华北科技学院现代教育技术中心,河北三河065201 |
| |
| 摘 要： | 形式化方法把程序看成规范,形式化开发方法包括形式规范和规范（程序）的精化。精化演算方法能够通过演算的方式,把规范逐步精化为程序。然而,演化的过程依赖于开发人员的经验,整个过程全部都是手动的。形式化方法的最高目标是软件自动化,使得能从规范自动开发出正确的程序。因而用Petri网来描述程序精化中的循环不变式,希望以此作为软件自动化的一个探索。
|
| 关 键 词： | 程序精化 循环不变式 Petri网 |
Model Loop Invariant in Software Refinement by Petri Net |
| |
| FANG Jing.Model Loop Invariant in Software Refinement by Petri Net[J].Computer Study,2011(4):14-15,19. |
| |
| Authors: | FANG Jing |
| |
| Affiliation: | FANG Jing(Modern Educational Technology Center;North China Institute of Science and Technology;Sanhe Hebei 065201;China) |
| |
| Abstract: | 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. |
| |
| Keywords: | Program Refinement Loop Invariant Petri Net |
| 本文献已被 维普 等数据库收录！ |
|
