Что означает «петли должны быть свернуты, чтобы обеспечить завершение»? - PullRequest
Новая
       77

Что означает «петли должны быть свернуты, чтобы обеспечить завершение»?

3 голосов
/ 25 августа 2011

В статье о формальных методах (абстрактная интерпретация, если быть точным) я наткнулся на «петли должны быть свернуты до конца». Мне ясно, что означает завершение, но я не знаю, что такое свернутая петля, и как выполнять складывание на петле.

Может кто-нибудь объяснить, пожалуйста, что такое свернутая петля? И если это не подразумевается или не следует сразу же для определения свернутого цикла, как это обеспечивает завершение?

Спасибо

Ответы [ 2 ]

4 голосов
/ 26 апреля 2012

Складывание цикла - это действие, противоположное более известному развертыванию цикла , которое более известно как развертывание цикла .Для данного цикла развернуть означает повторить тело несколько раз, чтобы тест цикла выполнялся реже.Когда количество выполнений цикла заранее, цикл можно полностью развернуть, оставив простую последовательность инструкций.Например, этот цикл 

for i := 1 to 4 do
  writeln(i);

можно развернуть до 

writeln(1);
writeln(2);
writeln(3);
writeln(4);

См. Развертывание цикла C ++, границы для другого примера с частичным развертыванием.

Метафора состоит в том, что программа складывается сама по себе много раз;развертывание означает удаление некоторых или всех этих сгибов.

В некоторых методах статического анализа трудно иметь дело с циклами, поскольку для нахождения предусловия для точки входа в цикл (т. е. для нахождения инварианта цикла) требуетсявычисление с фиксированной точкой, которое вообще неразрешимо.Поэтому некоторые анализы раскрывают петли;для этого необходимо иметь разумную границу количества итераций, что ограничивает объем программ, которые можно анализировать.

В других методах статического анализа поиск хорошего инварианта является критической частью анализа.Это не помогает развернуть цикл, фактически частичное развертывание цикла увеличило бы тело цикла и затруднило бы определение хорошего инварианта;и полностью развернуть цикл было бы нецелесообразно или невозможно, если бы число итераций было большим или неограниченным.Не видя бумаги, я нахожу это заявление несколько удивительным, потому что код мог быть написан с развернутой формой, но могут быть программы, над которыми анализ работает только в более сложенной форме.

0 голосов
/ 25 августа 2011

У меня нет знаний об абстрактной интерпретации, поэтому я приму функциональный подход к программированию свертывания. : -)

В функциональном программировании сгиб - это операция, применяемая к списку, чтобы что-то делать с каждым элементом, обновляя значение на каждой итерации. Например, вы можете реализовать map следующим образом (на схеме): 

(define (map1 func lst)
  (fold-right (lambda (elem result)
                (cons (func elem) result))
              '() lst))

Что он делает, так это то, что он начинается с пустого списка (назовем это результатом), а затем для каждого элемента списка, с правой стороны, перемещающейся влево, вы вызываете func для элемента и cons его результат в списке результатов.

Ключевым моментом здесь в том, что касается завершения, является то, что при сгибе цикл гарантированно завершится, пока список конечен, поскольку вы каждый раз переходите к следующему элементу списка, и если список конечен, тогда со временем следующего элемента не будет.

Сравните это с циклом for в стиле C, который не работает со списком, а вместо этого имеет форму for (init; test; update). test гарантированно никогда не вернет false, и поэтому цикл не гарантированно завершится.

...