How to prove by induction that a program does something?

Question

I have a computer program that reads in an array of chars that operands and operators written in postfix notation. The program then scans through the array works out the result by using a stack as shown :

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

how do i prove by induction that this program correctly evaluates any postfix expression (taken from exercise 4.16 Algorithms in Java (Sedgewick 2003))

Answer 1

I'm not sure which expressions you need to prove the algorithm against. But if they look like typical RPN expressions, you'll need to establish something like the following:

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

Good luck ;-)

Take heart concerning mathematical proofs, and also their sometimes confusing names. In the case of an inductive proof one is still expected to "figure out" something (some fact or some rule), sometimes by deductive logic, but then these facts and rules put together constitute an broader truth, buy induction; That is: because the base case is established as true and because one proved that if X was true for an "n" case then X would also be true for an "n+1" case, then we don't need to try every case, which could be a big number or even infinite)

Back on the stack-based expression evaluator... One final hint (in addtion to Captain Segfault's excellent explanation you're gonna feel over informed...).

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

Assuming that the expression is valid (and hence doesn't provide too many operators too soon), the order in which the operand/operators are fed into the algorithm do not matter; they always leave the system in a stable situtation: - either with one extra operand on the stack (but the knowledge that one extra operand will eventually come) or - with one fewer operand on the stack (but the knowledge that the number of operands still to come is also one less).

So the order doesn't matter.

Answer 2

You know what induction is? Do you generally see how the algorithm works? (even if you can't prove it yet?)

Your induction hypothesis should say that, after processing the N'th character, the stack is "correct". A "correct" stack for a full RPN expression has just one element (the answer). For a partial RPN expression the stack has several elements.

Your proof is then to think of this algorithm (minus the result = pop from stack line) as a parser that turns partial RPN expressions into stacks, and prove that it turns them into the correct stacks.

It might help to look at your definition of an RPN expression and work backwards from it.