分割图描述的正确性验证  

Correctness Verification of Decomposition Diagram Description

作　　者：滕至阳[1] 袁全生[1] 程正潮[1] 

机构地区：[1]东南大学计算机科学与工程系

出　　处：《高技术通讯》1998年第4期25-29,共5页Chinese High Technology Letters

基　　金：863计划资助项目

摘　　要：提出了针对决定性应用程序分割图描述的一种程序正确性验证方法。该方法把经过验证的分割图描述自动转换成Ｃ语言程序，在分割图级别上能够比较容易地构造程序模块的验证条件。A program correctness verification method corresponding to decomposition diagram description of deterministic application programs is presented in this paper. A C program is generated automatically from the decomposition diagram descriptions verified by this method. The method is easier to construct verification conditions of modules in the level of decomposition diagram than in the level of C program, because it is rather difficult to decompose a C program into modules with input and output attributes and find out data dependency relations among modules when directly verifying its correctness.

关 键 词：模块验证 程序正确性 分割图 软件工具 

分 类 号：TP311.56[自动化与计算机技术—计算机软件与理论]