如何通过感应来证明一个程序做一些事情？

Question

我有在字符数组该操作数和运算符写入后缀符号读取的计算机程序。然后该程序通过扫描该阵列通过使用堆栈如图工作出来的结果：

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（2003塞奇威克））

Answer 1

我不知道你需要证明对算法的表达式。但是，如果他们看起来像典型的RPN表达式，你需要建立类似以下内容：

1) algoritm works for 2 operands (and one operator)
   and 
   algorithm works for 3 operands (and 2 operators)
  ==> that would be your base case

2) if algorithm works for n operands (and n-1 operators)
  then it would have to work for n+1 operands.
  ==> that would be the inductive part of the proof

好运; - ）

拍摄心脏有关的数学证明，以及他们有时会混淆的名称。在的情况下的感应证明一个仍有望通过演绎逻辑，但随后这些事实和规则为“弄清楚”东西（一些事实或某些规则），有时放在一起构成了一个更广阔的道理，买诱导;那就是：因为基本情况被确定为真，因为一个证明，如果X是一个“n”的情况也是一样的，那么X也将是真正为“N + 1”的情况下，那么我们就需要想尽情况下，这可能是一个很大的数目或甚至无穷大）

返回的基于堆栈的表达式求值...最后一个提示（在addtion到段错误船长的优良解释你会觉得在告知...）。

The RPN expressions are  such that:
  - they have one fewer operator than operand
  - they never provide an operator when the stack has fewer than 2 operands 
    in it (if they didn;t this would be the equivalent of an unbalanced 
    parenthesis situation in a plain expression, i.e. a invalid expression).

假设表达式是有效的（并因此不提供过多的运营商太快），其中操作数/运营商被馈送到算法并不重要的顺序;他们总是留在稳定situtation系统：     - 无论是在栈上一个额外的操作数（但知识一个额外的操作最终会）或     - 与在堆栈上少一个操作数（但仍操作数来的数量也少了一个知识）

因此，顺序无关紧要。

Answer 2

您知道什么是诱导？你通常看到的算法是如何工作的？ （即使你不能证明这一点了吗？）

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

您证明然后认为该算法（减去结果=从堆线弹出），其转动的部分 RPN表达式成堆叠解析器的，并且证明它把它们转化成正确的堆叠

这可能有助于看看你的RPN表达的定义，并从它向后工作。