支持程序验证的模块方法

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