Расширение (информатика) - Widening (computer science)

В Информатика, особенно проверка модели и абстрактная интерпретация, расширение относится как минимум к двум различным методам анализа абстрактных переходные системы где бесконечные прогрессии абстрактных состояний заменяются (вычисленным или предполагаемым[1]) наименьшая фиксированная точка. Использование термина в проверка модели тесно связан с ускорение техники, некоторые авторы резервируют ускорение для точных расчетов.[2]

Интуиция

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

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

Использование при проверке модели

Методы расширения и тесно связанные с ними ускорение методы используются в форвардный анализ систем в дисциплине проверка символьной модели. Эти методы обнаруживают циклы, то есть последовательности абстрактных переходов между состояниями, которые могут повторяться. Когда такая последовательность может повторяться снова и снова, приводя к новым состояниям (например, переменная может увеличиваться при каждом повторении), символьный анализ программы не будет исследовать все эти состояния за конечное время. Для нескольких важных семейств систем, таких как системы выталкивания, канальные системы или же счетные системы подклассы, поддающиеся так называемым ровное ускорение были идентифицированы[2] для которого существует полная процедура анализа, вычисляющая весь набор достижимых состояний. Этот тип форвардного анализа также связан с хорошо структурированные переходные системы, но одной только хорошо структурированной структуры недостаточно для завершения таких процедур (например, график покрываемости из Сеть Петри всегда конечен, но в целом он превышает истинное пространство состояний).

Использование в абстрактной интерпретации

Кусо и Кузо[3] ввели понятие расширения, определяя рамки абстрактная интерпретация. Пример расширения абстрактной области, которая появляется в абстрактной интерпретации[4][5] заменит верхнюю границу интервала на .

Рекомендации

  1. ^ Ахмед Буаджани и Тайссир Туили (2012), «Методы расширения для регулярной проверки моделей деревьев», STTT, Vol. 14, № 2, с. 145 - 165 [1]
  2. ^ а б Себастьен Бардин, Ален Финкель, Жером Леру и Филипп Шнобелен, Плоское ускорение при проверке символьной модели (2005), Automated Technology for Verification and Analysis, pp. 474-488, Springer.
  3. ^ Патрик Кузо и Радия Кузо, Абстрактная интерпретация: {A} Модель единой решетки для статического анализа программ путем построения или аппроксимации фиксированных точек (1977), Отчет о четвертом симпозиуме {ACM} по принципам языков программирования, Лос-Анджелес, Калифорния, США, январь 1977 г., стр. 238–252.
  4. ^ П. Кузо, Р. Кузо (август 1992 г.). «Сравнение подходов Галуа и расширения / сужения к абстрактной интерпретации» (PDF). В Морисе Брюнооге и Мартине Вирсинге (ред.). Proc. 4-й Int. Symp. по реализации языка программирования и логическому программированию (PLILP). LNCS. 631. Springer. С. 269–296.
  5. ^ Агостино Кортеси (август 2008 г.), Операторы расширения для абстрактной интерпретации (PDF)