如何通过归纳证明一个程序做了什么？

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中的算法(Sedgewick 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"情况也是如此,那么我们不需要尝试每一个案例,可能是一个很大的数字甚至是无限的)

回到基于堆栈的表达式评估器......一个最后的提示(除了Segfault上尉的出色解释之外,你会感到过度了解......).

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).

假设表达式有效(因此过早不提供太多运算符),操作数/运算符输入算法的顺序无关紧要; 它们总是让系统处于稳定的状态: - 在堆栈上有一个额外的操作数(但知道一个额外的操作数最终会到来)或者 - 堆栈中的操作数减少一些(但是知道操作数仍然存在)来的还少一个).

所以顺序无关紧要.