26 июня 2009 · Комментарий

Без заголовка

Имя не сохранено · Оригинал в ЖЖ ↗ · Ссылка на запись

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