4551
правка
Ресинхронизация схемы: инкрементный подход: различия между версиями
Перейти к навигации
Перейти к поиску
м
Ресинхронизация схемы: инкрементный подход (посмотреть исходный код)
Версия от 19:43, 27 мая 2017
, 27 мая 2017→Основные результаты
Irina (обсуждение | вклад) |
Irina (обсуждение | вклад) |
||
| Строка 47: | Строка 47: | ||
Разработка алгоритма заключается в построении процедуры, такой, что ее выполнение завершится через конечное число шагов, а при завершении она будет удовлетворять заданному предикату. В случае задачи ресинхронизации с минимальной длительностью должен удовлетворяться предикат P0 | Разработка алгоритма заключается в построении процедуры, такой, что ее выполнение завершится через конечное число шагов, а при завершении она будет удовлетворять заданному предикату. В случае задачи ресинхронизации с минимальной длительностью должен удовлетворяться предикат <math>P0 \and P1 \and P2 \and P3 \;</math>. Этот предикат также называется ''постусловием''. Можно утверждать, что любой нетривиальный алгоритм будет содержать по меньшей мере один цикл; в противном случае продолжительность обработки пропорциональна просто длине текста. Следовательно, некоторая часть постусловий будет итеративно удовлетворяться в цикле, тогда как оставшаяся часть будет изначально удовлетворяться в процессе инициализации и оставаться инвариантной во время выполнения цикла. | ||
Первое решение, которое необходимо принять, касается разбиения постусловий на возможные инварианты цикла и его цель. Из четырех конъюнктивных членов предикат P3 задает условие оптимальности и является самым сложным из всех. Следовательно, он будет рассматриваться как цель при выполнении цикла. С другой стороны, предикаты P0 и P1 легко могут быть удовлетворены при помощи простой инициализации: | Первое решение, которое необходимо принять, касается разбиения постусловий на возможные инварианты цикла и его цель. Из четырех конъюнктивных членов предикат P3 задает условие оптимальности и является самым сложным из всех. Следовательно, он будет рассматриваться как цель при выполнении цикла. С другой стороны, предикаты P0 и P1 легко могут быть удовлетворены при помощи простой инициализации: | ||
r | |||
r, t := 0, d. | |||
Основываясь на этих соображениях, мы планируем разработать алгоритм согласно следующей схеме. | Основываясь на этих соображениях, мы планируем разработать алгоритм согласно следующей схеме. | ||
r | r, t := 0, d | ||
do <math>\{ P0 \and P1 \} \;</math> | |||
:P2 ! update t | :P2 ! update t | ||
:P3 ! update r odfP0 Л P1 Л P2 A P3g : | :P3 ! update r odfP0 Л P1 Л P2 A P3g : | ||