The Constrained Shortest Path Problem: A Case Study in Using ASMs
Дата
Авторы
Strötmann,Karl
Journal Title
Journal ISSN
Volume Title
Издатель
Journal of Universal Computer Science
Аннотация
Описание
This paper addresses the correctness problem of an algorithm solving the constrained shortest path problem. We define an abstract, nondeterministic form of the algorithm and prove its correctness from a few simple axioms. We then define a sequence of natural refinements which can be proved to be correct and lead from the abstract algorithm to an efficient implementation due to Ulrich Lauther [Lauther 1996] and based on [Desrosiers et al. 1995]. Along the way, we also show that the abstract algorithm can be regarded as a natural extension of Moore s algorithm [Moore 1957] for solving the shortest path problem.
Ключевые слова
abstract state machine , software verification , shortest path problem , constrained shortest path problem