自动程序设计（Automatic Programming）
自动程序设计主要有下面两个问题：
（一）程序验证（Program Verification）
程序验证是利用一个以验证过的程序系统来自动证明某一给定程序P的正确性。
设程序P的输入是x，它必须满足输入条件φ(x)；程序的输出是Z=P(x)，它必须满足输出条件
Φ（x,z),则这是程序的正确性有三种类型：
1、部分正确性
2、终止性
3、完全正确性
（二）程序综合（Program synthesis）
程序综合根据所给问题的具体描述由计算机自动生成满足要求的程序P。根据这个思想，所生成的程序P应对输入条件φ(x)和输出条件Φ(x,z)是完全正确的。目前程序综合的基本途径主要是程序变换，即通过对给定的输入、输出条件进行逐步变换，已构成所要求的程序。