Wie durch Induktion zu beweisen, dass ein Programm etwas tut?

Question

Ich habe ein Computerprogramm, das in einer Reihe von Zeichen liest, die Operanden und Operatoren in Postfix-Notation geschrieben. Das Programm scannt dann durch das Array das Ergebnis funktioniert durch einen Stapel mit wie folgt:

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

Wie kann ich durch Induktion beweisen, dass dieses Programm wertet richtig jeden postfix Ausdruck? (Aus Übung 4.16 Algorithmen in Java (Sedgewick 2003))

Answer 1

Ich bin nicht sicher, welche Ausdrücke, die Sie den Algorithmus gegen beweisen müssen. Aber wenn sie wie typische RPN Ausdrücke aussehen, müssen Sie etwa wie folgt herzustellen:

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

Viel Glück; -)

Nehmen Sie Herz mathematische Beweise über, und auch ihre manchmal verwirrenden Namen. Im Fall eines induktiven Beweis man noch wird erwartet, dass „herauszufinden,“ etwas (etwas Tatsache oder eine Regel), manchmal von deduktiven Logik, aber dann diesen Fakten und Regeln zusammen eine breitere Wahrheit bilden, kaufen Induktion; Das heißt: da der Basisfall als wahr etabliert ist und weil man bewies, dass, wenn X für ein „n“ Fall zutraf dann X auch für einen „n + 1“ Fall wahr wäre, dann müssen wir alle nicht versuchen Fall, der eine große Zahl oder sogar unendlich sein könnte)

Zurück auf dem Stack-basierten Ausdrucksauswerter ... Ein letzter Hinweis (zusätzlich zu Kapitän Segfault ausgezeichneter Erklärung wirst du fühlen über informiert ...).

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

Unter der Annahme, dass der Ausdruck gültig ist (und daher nicht zu bieten hat zu früh viele Betreiber), die Reihenfolge, in der der Operand / Betreiber in den Algorithmus eingespeist wird keine Rolle spielen; sie lassen immer das System in einem stabilen situtation:    - entweder mit einem zusätzlichen Operanden auf dem Stapel (aber das Wissen, dass ein zusätzliche Operanden werden schließlich kommen) oder    -. Mit einem weniger Operanden auf dem Stapel (aber das Wissen, dass die Anzahl der Operanden noch zu kommen, ist auch eine weniger)

So ist die Reihenfolge keine Rolle spielt.

Answer 2

Sie wissen, was Induktion? Haben Sie im Allgemeinen sehen, wie der Algorithmus funktioniert? (Auch wenn Sie es noch nicht beweisen können?)

Sie sollte Induktionsvoraussetzung sagen, dass nach dem N-ten Zeichen der Verarbeitung, der Stapel ist „richtig“. Ein „richtiger“ Stapel für einen vollen RPN Ausdruck hat nur ein Element (die Antwort). Für einen Teil RPN Ausdruck hat der Stapel mehrere Elemente.

Ihr Beweis ist dann diesen Algorithmus zu denken (minus dem Ergebnis = Pop aus Zeile Stack) als Parser, der Teil RPN Ausdrücke in Stapel dreht, und beweist, dass es sie in die richtigen Stapel dreht .

Es könnte auf Ihre Definition eines RPN Ausdruck suchen helfen und arbeiten nach hinten von ihm.