功能描述导引的程序综合

本文介绍一种从一程序的入口和出口断言中所含逻辑常量出现的情况,推断该程序的逻辑结构,再加上人的参与综合出该程序的方法。这方法的出发点与Dijkstra的“最弱前置条件程序推导”的基本思想颇为相近,但我们着重讨论了断言中出现的存在量词和受囿量词与相应的程序的关系。此外,我们采用的形式表示方式也与WP不同。我们曾用实例为据比较过这两种方法,感到有些用Dijkstra方法不易推导的程序,比如具有嵌套循环结构的程序,用本文的方法处理起来较为方便。