程序的结构合成

程序的结构合成（SSP）是一种基于命题微积分的（自动）程序合成的特殊形式。更确切地说，它使用直觉逻辑来描述程序的结构，使程序可以由子程序甚至计算机命令这样的片段自动组成。它假定这些片段已经被正确实现，因此不需要对这些片段进行正确性验证。SSP非常适用于面向服务的体系结构的服务的自动组成和大型模拟程序的合成。

自动程序合成开始于人工智能领域，用于自动解决问题的软件。实际适用的程序合成器出现得相当晚。在SSP中，设计一个解决问题的计划的方法是作为一个形式系统提出的。最近一个支持SSP的集成开发环境是CoCoViLa--一个基于模型的软件开发平台，用于实现特定领域语言和开发大型Java程序。

程序的结构合成是一种从已经实现的组件组成程序的方法，这些组件可以被视为函数。通过编写关于函数适用性的公理，在直觉命题逻辑中给出了合成的规范。前提条件可以是一个说明输入数据存在的命题，但它也可以表示一些其他条件，例如使用函数f所需的资源是可用的，等等。前提条件也可以是与上述公理形式相同的暗示，那么它就被称为子任务。子任务表示在应用函数f时必须有一个函数作为输入。这个函数本身必须在SSP的过程中被合成。

在这种情况下，公理的实现是一个高阶函数，即一个使用另一个函数作为输入的函数。xxx个输入是一个必须被合成的函数，用于从状态计算下一个状态，第二个输入是初始状态。高阶函数给SSP带来了通用性--合成程序中需要的任何控制结构都可以被预编程，然后用各自的规范自动使用。特别是，这里提出的最后一个公理是一个复杂程序的规范--用于在模型上模拟动态系统的仿真引擎，其中NextState可以从系统的状态中计算出来。