Как с помощью индукции доказать, что программа что-то делает?

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", тогда нам не нужно пробовать каждый случай, который может быть большим числом или даже бесконечным)

Вернемся к вычислителю выражений на основе стека...Последний совет (в дополнение к превосходному объяснению капитана Сегфолта вы почувствуете себя слишком информированным ...).

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

Предполагая, что выражение является допустимым (и, следовательно, не предоставляет слишком много операторов слишком рано), порядок, в котором операнд / операторы вводятся в алгоритм, не имеет значения;они всегда оставляют систему в стабильном состоянии .:- либо с одним дополнительным операндом в стеке (но зная, что один дополнительный операнд в конечном итоге появится), либо - с меньшим количеством операндов в стеке (но знание того, что количество операндов еще впереди, также на один меньше).

Так что порядок не имеет значения.

Answer 2

Вы знаете, что такое индукция?Вы вообще понимаете, как работает алгоритм?(даже если вы пока не можете это доказать?)

Ваша гипотеза индукции должна гласить, что после обработки N-го символа стек является "правильным"."Правильный" стек для полного выражения RPN содержит только один элемент (ответ).Для частичного выражения RPN стек состоит из нескольких элементов.

Ваше доказательство состоит в том, чтобы думать об этом алгоритме (за вычетом результата = pop из строки стека) как о анализаторе, который превращает частичный Преобразуйте выражения RPN в стеки и докажите, что это превращает их в правильные стеки.

Это могло бы помочь взглянуть на ваше определение выражения RPN и работать в обратном направлении от него.