Как по индукции доказать, что программа что-то делает? - PullRequest
Новая
       85

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

1 голос
/ 23 сентября 2009

У меня есть компьютерная программа, которая читает массив символов, операнды и операторы которых записаны в постфиксной нотации. Затем программа просматривает массив и обрабатывает результат, используя стек, как показано: 

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

Как по индукции доказать, что эта программа правильно оценивает любое выражение postfix? (взято из упражнения 4.16 Алгоритмы в Java (Sedgewick 2003))

Ответы [ 2 ]

5 голосов
/ 23 сентября 2009

Я не уверен, с какими выражениями нужно доказывать алгоритм. Но если они выглядят как типичные выражения 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).

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

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

0 голосов
/ 23 сентября 2009

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

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

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

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

...