maisМоделирование и анализ информационных системModeling and Analysis of Information Systems1818-10152313-5417Yaroslavl State Universitymais-1107Research ArticleОригинальные статьиArticlesВерификация шаблонов алгоритмов для метода отката и метода ветвей и границVerification of Backtracking and Branch and Bound Design TemplatesШиловНиколай ВячеславовичShilovN. V.shilov@iis.nsk.suИнститут систем информатики им. А.П. Ершова СО РАН, Новосибирский государственный университет и Новосибирский государственный технический университетRussian Federation201120122011184168180Copyright © Шилов Н.В., 20112011Шилов Н.В.Shilov N.V.Данная работа распространяется под лицензией Creative Commons Attribution 4.0.This work is licensed under a Creative Commons Attribution 4.0 License.https://www.mais-journal.ru/jour/article/view/1107

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

The Design and Analysis of Computer Algorithms is a must of Computer Curricula. It covers many topics that group around several core themes. These themes range from data structures to the complexity theory, but one very special theme is algorithmic design patterns, including greedy method, divide-and-conquer, dynamic programming, backtracking and branch-and-bound. Naturally, all the listed design patterns are taught, learned and comprehended by examples. But they can be semi-formalized as design templates, semi-specified by correctness conditions, and semi-formally verified by means of Floyd method. Moreover, this approach can lead to new insights and better comprehension of the design patterns, specification and verification methods. In this paper we demonstrate an utility of the approach by study of backtracking and branch-and-bound design patterns. In particular, we prove correctness of the suggested templates when the boundary condition is monotone, but the decision condition is anti-monotone on sets of "visited" vertices.

метод откатаметод ветвей и границабстрактные типы данныхчастичная корректностьтотальная корректностьметод верификации Флойдазадача о расстанове ферзейдискретная задача о ранцеbacktrackingbranch-and-boundabstract data typepartial correctnesstotal correctnessFloyd proof methodn-queen puzzleknapsack problemReferencesАхо А., Хопкрофт Дж., Ульман Дж. Построение и анализ вычислительных алгоритмов. М.: Мир, 1979.Ахо А., Хопкрофт Дж., Ульман Дж. Построение и анализ вычислительных алгоритмов. М.: Мир, 1979.Грис Д. Наука программирования. М.: Мир, 1984.Грис Д. Наука программирования. М.: Мир, 1984.Дейкстра В.Э. Дисциплина программирования. М.: Мир, 1978.Дейкстра В.Э. Дисциплина программирования. М.: Мир, 1978.Корнмэн Т, Лейзерсон Ч, Ривест Р. Алгоритмы: построение и анализ. М.: МЦНМО, 2000.Корнмэн Т, Лейзерсон Ч, Ривест Р. Алгоритмы: построение и анализ. М.: МЦНМО, 2000.Непомнящий В.А. Верификация финитных итераций над наборами изменяемых структур данных. Кибернетика и системный анализ. Киев. 2007. №3. С.33-46.Непомнящий В.А. Верификация финитных итераций над наборами изменяемых структур данных. Кибернетика и системный анализ. Киев. 2007. №3. С.33-46.Шилов Н.В. Основы синтаксиса, семантики, трансляции и верификации программ. Новосибирск: Новосибирский государственный университет, 2011.Шилов Н.В. Основы синтаксиса, семантики, трансляции и верификации программ. Новосибирск: Новосибирский государственный университет, 2011.Apt K.R., de Boer F.S., Olderog E.-R. Verification of Sequential and Concurrent Programs. Third edition. Springer, 2009.Apt K.R., de Boer F.S., Olderog E.-R. Verification of Sequential and Concurrent Programs. Third edition. Springer, 2009.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.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.Golomb S.W. and Baumert L.D. Backtrack Programming // Journal of ACM. 1965. 12(4). P. 516-524.Golomb S.W. and Baumert L.D. Backtrack Programming // Journal of ACM. 1965. 12(4). P. 516-524.Land A. H. and Doig A. G. An automatic method of solving discrete programming problems // Econometrica. 1960. 28(3). P. 497-520.Land A. H. and Doig A. G. An automatic method of solving discrete programming problems // Econometrica. 1960. 28(3). P. 497-520.Kant E. Understanding and Automating Algorthm Design // IEEE Transactions on Software Engineering. 1985. SE-11(11). P. 1361-1374.Kant E. Understanding and Automating Algorthm Design // IEEE Transactions on Software Engineering. 1985. SE-11(11). P. 1361-1374.Smith D. R. Automating the design of algorithms // Formal Program Development. 1993. Lecture Notes in Computer Science. 755. P. 324-354.Smith D. R. Automating the design of algorithms // Formal Program Development. 1993. Lecture Notes in Computer Science. 755. P. 324-354.

The authors declare that there are no conflicts of interest present.