支持程序验证的模块方法

本文给出一种支持程序验证的模块方法,并讨论了基于函数语义的模块验证。程序(特别是大型复杂的程序)可划分为若干个摸块,模块本身又可划分为若干个更小的子模块,其验证独立进行。将独立验证过的各子模块复合,完成上级模块或程序本身的验证。