【作者】 刘定飞; 钟珞;
【机构】 武汉工业大学自动化系; 武汉工业大学自动化系 武汉 430070; 武汉 430070;
【摘要】 本文给出一种支持程序验证的模块方法,并讨论了基于函数语义的模块验证。程序(特别是大型复杂的程序)可划分为若干个摸块,模块本身又可划分为若干个更小的子模块,其验证独立进行。将独立验证过的各子模块复合,完成上级模块或程序本身的验证。更多还原