如何通过归纳证明程序做了某事？答案

【问题标题】：How to prove by induction that a program does something?如何通过归纳证明程序做了某事？
【发布时间】：2009-09-22 21:52:17
【问题描述】：

我有一个计算机程序，它读取以后缀表示法编写的操作数和运算符的字符数组。然后程序扫描数组，使用堆栈计算结果，如下所示：

get next char in array until there are no more
if char is operand
    push operand into stack
if char is operator 
    a = pop from stack
    b = pop from stack
    perform operation using a and b as arguments
    push result
result = pop from stack

我如何通过归纳证明这个程序正确地计算任何后缀表达式？（取自练习 4.16 Java 算法（Sedgewick 2003））

【问题讨论】：

这与标准归纳有何不同？证明基本情况，然后假设大小为 n-1 的情况为真，这意味着情况 n 为真。这是关于归纳时必须做的事情的简要总结。
我遇到的问题是找出基本情况和归纳步骤是什么。基本情况是 n = 3，数组是：操作数操作数运算符，我如何证明上面的程序计算正确？

标签： math proof postfix-notation induction

【解决方案1】：

我不确定您需要针对哪些表达式来证明该算法。但如果它们看起来像典型的 RPN 表达式，则需要建立如下内容：

1) 算法适用于 2 个操作数（和一个运算符）和算法适用于 3 个操作数（和 2 个运算符） ==> 那将是你的基本情况 2) 如果算法适用于 n 个操作数（和 n-1 个运算符）那么它必须适用于 n+1 个操作数。 ==> 这将是证明的归纳部分

祝你好运;-)

请注意数学证明，以及它们有时令人困惑的名称。在归纳证明的情况下，人们仍然期望“弄清楚”某些东西（某些事实或某些规则），有时通过演绎逻辑，但随后这些事实和规则放在一起构成一个更广泛的道理，买归纳；那就是：因为基本情况被确定为真，并且因为有人证明如果 X 对于“n”情况为真，那么 X 对于“n+1”情况也为真，那么我们不需要尝试每个情况，可能是一个很大的数字，甚至是无限的）

回到基于堆栈的表达式评估器...最后一个提示（除了 Segfault 船长的出色解释之外，您会觉得信息量过大...）。

RPN 表达式是这样的： - 它们的运算符比操作数少一个 - 当堆栈的操作数少于 2 个时，它们从不提供运算符在其中（如果他们没有；这将相当于不平衡普通表达式中的括号情况，即无效表达式）。

假设表达式有效（因此不会过早提供太多运算符），将操作数/运算符输入算法的顺序无关紧要；他们总是让系统处于稳定状态： - 堆栈上有一个额外的操作数（但知道最终会出现一个额外的操作数）或 - 堆栈上的操作数少了一个（但知道还剩下的操作数也少了一个）。

所以顺序无关紧要。

【讨论】：

谢谢，这为我指明了正确的方向，让我意识到我对算法的数学证明一无所知，所以我应该等到我学会了，然后再回来针对这个问题

【解决方案2】：

你知道什么是感应吗？你通常看到算法是如何工作的吗？（即使你还不能证明呢？）

你的归纳假设应该说，在处理完第 N 个字符之后，堆栈是“正确的”。完整 RPN 表达式的“正确”堆栈只有一个元素（答案）。对于部分 RPN 表达式，堆栈有多个元素。

然后您的证明就是将此算法（减去结果 = 从堆栈行弹出）视为将部分 RPN 表达式转换为堆栈的解析器，并证明它将它们转换为正确的堆栈.

查看您对 RPN 表达式的定义并从其逆向工作可能会有所帮助。

【讨论】：