¿Cómo demostrar por inducción que un programa hace algo?

Question

Tengo un programa informático que lee en una serie de caracteres que operandos y operadores escritas en notación de sufijo. Entonces, el programa escanea a través de la matriz funciona el resultado mediante el uso de una pila como se muestra:

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

¿Cómo puedo demostrar por inducción que este programa evalúa correctamente cualquier expresión de sufijo? (Tomado del ejercicio 4.16 Algoritmos en Java (Sedgewick 2003))

Answer 1

No estoy seguro de qué expresiones que necesita para probar el algoritmo contra. Pero si se ven como expresiones típicas RPN, tendrá que establecer algo como lo siguiente:

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

Buena suerte; -)

¡Ánimo en relación con las pruebas matemáticas, y también sus nombres a veces confuso. En el caso de un inductiva una prueba todavía se espera que "averiguar" algo (algún hecho o alguna regla), a veces por deductivos lógica, pero luego estos hechos y reglas poner en conjunto constituyen una verdad más amplia, comprar inducción; Es decir: debido a que el caso base se establece como verdadero y porque uno demostró que si X es cierto para un caso de "n", entonces X también sería cierto para un caso "n + 1", entonces no es necesario probar cada caso, lo que podría ser un número grande o incluso infinito)

De vuelta en el evaluador de expresiones basado en pila ... Una última pista (en addtion a excelente explicación del capitán segfault que vas a sentir más informado ...).

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

Suponiendo que la expresión es válida (y por tanto no proporciona demasiados operadores demasiado pronto), el orden en que el operando / operadores se introducen en el algoritmo no importa; siempre dejan el sistema en un situtation estable:    - ya sea con un operando adicional en la pila (pero el conocimiento de que un operando adicional eventualmente llegará) o    -. Con uno menos operando en la pila (pero el conocimiento de que el número de operandos aún por venir es también uno menos)

Así que el orden no es importante.

Answer 2

Usted sabe lo que es la inducción? ¿Por lo general se ve cómo funciona el algoritmo? (Incluso si no se puede demostrar aún?)

Su hipótesis de inducción debe decir que, después de procesar el carácter N-sima, la pila es "correcta". Una pila "correcta" para una expresión RPN completa tiene sólo un elemento (la respuesta). Para una expresión RPN parcial la pila tiene varios elementos.

Su prueba es entonces que pensar en este algoritmo (menos el resultado = emergente desde la línea de pila) como un analizador que convierte parciales expresiones RPN en pilas, y demostrar que las convierte en las pilas correctas .

Podría ayudar a mirar a su definición de una expresión RPN y trabajar hacia atrás de ella.