结构化程序理论

结构化程序定理，也称为 Böhm–Jacopini 定理，是编程语言理论的一个结果。 它指出，如果一类控制流图（在此上下文中历史上称为流程图）仅以三种特定方式（控制结构）组合子程序，则它可以计算任何可计算函数。 这些都是

• 执行一个子程序，然后执行另一个子程序（顺序）
• 根据布尔表达式的值（选择）执行两个子程序之一
• 只要布尔表达式为真，就重复执行子程序（迭代）

然而，受制于这些约束的结构化图表可以使用位形式的附加变量（存储在原始证明中的额外整数变量中），以便跟踪原始程序由程序位置表示的信息。 该结构基于 Böhm 的编程语言 P''。

该定理构成了结构化编程的基础，结构化编程是一种避开 goto 命令并专门使用子例程、序列、选择和迭代的编程范例。

该定理通常归功于 Corrado Böhm 和 Giuseppe Jacopini 1966 年的一篇论文。 David Harel 在 1980 年写道，Böhm–Jacopini 论文广受欢迎，尤其是在结构化编程的支持者中。 Harel 还指出，由于其相当技术性的风格 [1966 年的 Böhm–Jacopini 论文] 显然被引用的次数多于详细阅读的次数，并且在回顾了 1980 年之前发表的大量论文之后，Harel 认为 Böhm 的内容—— Jacopini 证明通常被误认为是一个民间定理，它本质上包含一个更简单的结果，这个结果本身可以追溯到冯诺依曼和克莱恩的论文中现代计算理论的起源。

Harel 还写道，更通用的名称是由 H.D. 提出的。 米尔斯在 1970 年代初作为结构定理。

这个版本的定理用单个全局 while 循环替换了所有原始程序的控制流，该循环模拟程序计数器遍历原始非结构化程序中所有可能的标签（流程图框）。 Harel 将这个民间定理的起源追溯到两篇标志着计算开始的论文。 一个是 1946 年对冯诺依曼体系结构的描述，它解释了程序计数器如何根据 while 循环运行。 Harel 指出，结构化编程定理的民间版本使用的单循环基本上只是为在冯诺依曼计算机上执行流程图提供了操作语义。 Harel 追溯该定理的民间版本的另一个更古老的来源是 Stephen Kleene 1936 年的范式定理。

Donald Knuth 批评了这种形式的证明，指出原始程序的结构在这种转换中完全丢失了，从而导致如下所示的伪代码。 同样，布鲁斯·伊恩·米尔斯 (Bruce Ian Mills) 写过这种方法，块结构的精神是一种风格，而不是一种语言。 通过模拟冯诺依曼机，我们可以在块结构语言的范围内生成任何意大利面条代码的行为。

Böhm 和 Jacopini 的论文中的证明是通过对流程图的结构进行归纳来进行的。 因为它在图形中使用了模式匹配，Böhm 和 Jacopini 的证明作为程序转换算法并不真正实用，因此打开了在这个方向进一步研究的大门。

Böhm–Jacopini 证明并没有解决是否为软件开发采用结构化编程的问题，部分原因是构造更有可能使程序变得模糊而不是改进程序。 相反，它标志着辩论的开始。 Edsger Dijkstra 的著名信件 Go To Statement Considered Harmful 随后于 1968 年发表。

一些学者对 Böhm-Jacopini 结果采取了纯粹主义的方法，并认为即使像 break 和 return 这样的指令从循环中间返回也是不好的做法，因为在 Böhm-Jacopini 证明中不需要它们，因此他们主张所有循环都应该有 一个出口点。 这种纯粹的方法体现在 Pascal 编程语言（设计于 1968 年至 1969 年）中，直到 1990 年代中期，它还是介绍性教学的首选工具。