Доказательство корректности алгоритмов

Третий шаг состоит в том, чтобы доказать, что если алгоритм удовлетворяет спецификации, то он является алгоритмом поиска пути - удовлетворяет следующим утверждениям:

1. Алгоритм работает конечное время.

2. Агент корректно ходит по полю и не натыкается на препятствия.

3. Если существует путь к цели, то он будет найден.

4. Если пути не существует, то агент вернёт ответ о том, что цель недостижима.

Вначале докажем утверждение 3.

Лемма 5.5.1. Если путь к цели существует, то всегда своём пути агент либо дойдёт до цели, либо сохранится ближе, чем предыдущее сохранение.

Из формул f19 - f26следует, что до тех пор, пока агент не наткнулся на препятствие, он будет идти в сторону цели. Агент стартует из сохранённого состояния. Если путь в сторону цели свободен, то агент пойдёт в это сторону и будет находиться ближе, чем сохранённая клетка. Если агент упрётся в препятствие, то он в этот момент либо ближе, чем сохранённая клетка, либо в ней находится. Как только агент упёрся в препятствие, он начинает его обход либо по часовой стрелке, либо против (формулы f12 - f15).

Формулы f0 - f15утверждают, что если агент находится в состоянии обхода, то он будет обходить препятствие правильно. Так как агент обходит препятствие, то он будет в некоторый момент ближе, чем последняя сохранённая клетка. Следовательно (формула f29),агент сохранится ближе к цели, чем предыдущее сохранение, либо дойдёт до цели (в этом случае лемма

верна). Оторваться от препятствия агент может, только если он находится либо в «сохранённой» клетке, либо ближе, чем последнее сохранение и только если он совершает шаг в сторону цели. Следовательно, на следующем шаге, после того, как агент оторвётся от препятствия, он будет ближе, чем последнее сохранение. Поэтому он либо сохранится ближе последнего сохранения, либо дойдёт до цели и т. д.

Из леммы 5.5.1 следует, что можно построить последовательность из сохранённых клеток, каждая из которых ближе к цели, чем предыдущая.

Докажем утверждение 4.

Утверждение, что пути не существует равносильно тому, что есть препятствие, во время обхода которого не существует условий, при которых можно от него оторваться. Из формулы f29аналогично доказательству леммы 5.5.1 следует, что можно построить последовательность из сохранённых клеток, каждая из которых ближе предыдущей. Эта последовательность конечная.

Посмотрим на последнюю сохранённую клетку. Так как она последняя, то после неё агент никогда не подходил к препятствию ближе, чем расположена эта клетка.

Следовательно, это сохранение было сделано во время обхода препятствия, иначе, агент должен сделать шаг в сторону препятствия и стать ближе. Таким образом, у агента на всём пути после этой клетки не было возможности оторваться от этого препятствия, иначе, он бы стал ближе к цели, чем последняя сохранённая клетка.

Следовательно, весь остальной путь агента является обходом этого препятствия. Из формулы f30следует, что агент не вернёт результат, свидетельствующий о том, что путь найден. Из формулы f28следует, что агент либо вернёт результат, что цель недостижима, либо в будущем будет верно одно из следующих утверждений:

• можно будет построить бесконечную последовательность из сохранённых клеток, каждая из которых ближе предыдущей (в случае конечного расстояния до цели это невозможно);

• каждый следующий шаг агента будет в сторону цели (в случае конечного расстояния до цели это невозможно);

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

Следовательно, агент завершит работу и вернёт результат, что цель недостижима.

Из справедливости утверждений 3 и 4 следует справедливость утверждения 1.

Докажем теперь утверждение 2. Формула f17утверждает, что агент никогда не войдёт внутрь препятствия, следовательно, агенты, удовлетворяющие этой формуле, удовлетворяют и утверждению 2.

5.7.