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