RUS  ENG JOURNALS   PEOPLE   ORGANISATIONS   CONFERENCES   SEMINARS   VIDEO LIBRARY   PACKAGE AMSBIB
General information
Latest issue
Archive
Impact factor

Search papers
Search references

RSS
Latest issue
Current issues
Archive issues
What is RSS



Model. Anal. Inform. Sist.:
Year:
Volume:
Issue:
Page:
Find






Personal entry:
Login:
Password:
Save password
Enter
Forgotten password?
Register


Model. Anal. Inform. Sist., 2011, Volume 18, Number 4, Pages 168–180 (Mi mais207)  

Verification of backtracking and branch and bound design templates

N. V. Shilovabc

a Novosibirsk State University
b A. P. Ershov Institute of Informatics Systems Sib. Br. RAS
c Novosibirsk State Technical University

Abstract: 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.

Keywords: backtracking, branch-and-bound, abstract data type, partial correctness, total correctness, Floyd proof method, $n$-queen puzzle, knapsack problem.

Full text: PDF file (656 kB)
References: PDF file   HTML file
UDC: 519.681+519.683.8+519.688
Received: 11.10.2011

Citation: N. V. Shilov, “Verification of backtracking and branch and bound design templates”, Model. Anal. Inform. Sist., 18:4 (2011), 168–180

Citation in format AMSBIB
\Bibitem{Shi11}
\by N.~V.~Shilov
\paper Verification of backtracking and branch and bound design templates
\jour Model. Anal. Inform. Sist.
\yr 2011
\vol 18
\issue 4
\pages 168--180
\mathnet{http://mi.mathnet.ru/mais207}


Linking options:
  • http://mi.mathnet.ru/eng/mais207
  • http://mi.mathnet.ru/eng/mais/v18/i4/p168

    SHARE: VKontakte.ru FaceBook Twitter Mail.ru Livejournal Memori.ru


    Citing articles on Google Scholar: Russian citations, English citations
    Related articles on Google Scholar: Russian articles, English articles
  • Моделирование и анализ информационных систем
    Number of views:
    This page:252
    Full text:96
    References:18

     
    Contact us:
     Terms of Use  Registration  Logotypes © Steklov Mathematical Institute RAS, 2020