Верификация шаблонов алгоритмов для метода отката и метода ветвей и границ

Курс проектирования и анализа алгоритмов является обязательной составляющей учебных программ по информатике всех уровней. В университетах этот курс обязательно включает изучение структур данных, методы проектирования алгоритмов, теорию сложности и т.д. Этот курс знакомит с такими методами проектирования алгоритмов, как жадные алгоритмы, динамическое программирование, метод разделяй и властвуй, метод отката, метод ветвей и границ. Обычно знакомство с этими методами происходит на примерах. Но (как показано в данной статье) они могут быть (полу)формализованы в виде "паттернов", специфицированы условиями частичной и/или тотальной корректности и обоснованы (доказаны) методом Флойда верификации алгоритмов. Такой формализованный подход может привести к новому, более глубокому пониманию этих методов. В статье демонстрируется перспективность такого подхода на примере метода отката и метода ветвей и границ. В частности, мы доказываем, что разработанные шаблоны корректны, если граничное условие - монотонная функция, а решающее условие - антимонотонная функция от множества уже проверенных вершин.

метод отката, метод ветвей и границ, абстрактные типы данных, частичная корректность, тотальная корректность, метод верификации Флойда, задача о расстанове ферзей, дискретная задача о ранце

1. Ахо А., Хопкрофт Дж., Ульман Дж. Построение и анализ вычислительных алгоритмов. М.: Мир, 1979.

2. Грис Д. Наука программирования. М.: Мир, 1984.

3. Дейкстра В.Э. Дисциплина программирования. М.: Мир, 1978.

4. Корнмэн Т, Лейзерсон Ч, Ривест Р. Алгоритмы: построение и анализ. М.: МЦНМО, 2000.

5. Непомнящий В.А. Верификация финитных итераций над наборами изменяемых структур данных. Кибернетика и системный анализ. Киев. 2007. №3. С.33-46.

6. Шилов Н.В. Основы синтаксиса, семантики, трансляции и верификации программ. Новосибирск: Новосибирский государственный университет, 2011.

7. Apt K.R., de Boer F.S., Olderog E.-R. Verification of Sequential and Concurrent Programs. Third edition. Springer, 2009.

8. Floyd R.W. Assigning meanings to programs. Proc. of a Symposium in Applied Mathematics. Mathematical Aspects of Computer Science // American Math. Society, Providence, R. I. 1967. Vol. 19. P. 19-32.

9. Golomb S.W. and Baumert L.D. Backtrack Programming // Journal of ACM. 1965. 12(4). P. 516-524.

10. Land A. H. and Doig A. G. An automatic method of solving discrete programming problems // Econometrica. 1960. 28(3). P. 497-520.

11. Kant E. Understanding and Automating Algorthm Design // IEEE Transactions on Software Engineering. 1985. SE-11(11). P. 1361-1374.

12. Smith D. R. Automating the design of algorithms // Formal Program Development. 1993. Lecture Notes in Computer Science. 755. P. 324-354.