Расширенная статическая проверка
Расширенная статическая проверка ( ESC ) — это собирательное название в информатике для ряда методов статической проверки правильности различных ограничений программы. [1] ESC можно рассматривать как расширенную форму проверки типов . Как и проверка типов, ESC выполняется автоматически во время компиляции (т.е. без вмешательства человека). Это отличает его от более общих подходов к формальной проверке программного обеспечения, которые обычно полагаются на доказательства, созданные человеком. Кроме того, он отдает предпочтение практичности, а не надежности, поскольку направлен на резкое сокращение количества ложных срабатываний (переоцененных ошибок, которые не являются реальными ошибками, то есть превышения строгости ESC) за счет введения некоторых ложноотрицательных результатов (реальная ошибка недооценки ESC, но это не требует внимания программиста или не является целью ESC). [2] [3] ESC может идентифицировать ряд ошибок, которые в настоящее время находятся за пределами проверки типов, включая деление на ноль , выход массива за пределы , переполнение целых чисел и разыменование null .
Методы, используемые в расширенной статической проверке, взяты из различных областей информатики, включая статический анализ программ , символическое моделирование , проверку моделей , абстрактную интерпретацию , решение SAT и автоматическое доказательство теорем и проверку типов . Расширенная статическая проверка обычно выполняется только на внутрипроцедурном, а не на межпроцедурном уровне для масштабирования до больших программ. [2] Кроме того, расширенная статическая проверка направлена на сообщение об ошибках, используя предоставленные пользователем спецификации в форме пред- и постусловий , инвариантов цикла и инвариантов классов .
Расширенные статические средства проверки обычно работают путем распространения сильнейших постусловий (соответственно самых слабых предусловий ) внутри процедур через метод, начинающийся с предусловия (соответственно постусловия). На каждом этапе этого процесса генерируется промежуточное условие, которое фиксирует то, что известно на этом этапе программы. Это объединяется с необходимыми условиями оператора программы в этот момент, чтобы сформировать условие проверки . Примером этого является оператор деления, необходимым условием которого является то, что делитель не равен нулю. Вытекающее из этого условие проверки фактически гласит: учитывая промежуточное условие в этой точке, должно следовать, что делитель не равен нулю . Все условия проверки должны быть ложными (следовательно, правильными посредством исключенного третьего ), чтобы метод прошел расширенную статическую проверку (или «не смог найти больше ошибок»). Обычно для выполнения условий проверки используется та или иная форма автоматического средства доказательства теорем.
Расширенная статическая проверка была впервые реализована в ESC/Modula-3. [4] и, позже, ESC/Java . Его корни берут начало в более упрощенных методах статической проверки, таких как статическая отладка. [5] или lint и FindBugs . ESC принят в ряде других языков, включая Spec#, SPARKada и VHDL VSPEC. Однако в настоящее время не существует широко используемого языка программирования, обеспечивающего расширенную статическую проверку в базовой среде разработки.
См. также
[ редактировать ]- Язык моделирования Java (JML)
Ссылки
[ редактировать ]- ^ К. Фланаган, К.РМ. Лейно, М. Лиллибридж, Г. Нельсон, Дж. Б. Сакс и Р. Стата. «Расширенная статическая проверка Java». В материалах конференции по проектированию и реализации языков программирования , страницы 234-245, 2002 г. doi: http://doi.acm.org/10.1145/512529.512558 .
- ^ Jump up to: а б «Расширенная статическая проверка» . УВТВ . Проверено 1 февраля 2012 г. [ постоянная мертвая ссылка ]
- ^ Бабич, Домагой; Ху, Алан Дж. (2008). Calysto: масштабируемая и точная расширенная статическая проверка . Материалы Международной конференции по программной инженерии (ICSE). АКМ Пресс. дои : 10.1145/1368088.1368118 .
- ^ Рустан, К.; Лейно, М.; Нельсон, Грег (1998). «Расширенная статическая проверка для модуля-3». Конспекты лекций по информатике — Международная конференция по построению компиляторов . Спрингер. стр. 302–305. дои : 10.1007/bfb0026441 . ISBN 978-3-540-64304-3 . ISSN 0302-9743 .
- ^ Фланаган, Кормак; Флэтт, Мэтью; Кришнамурти, Шрирам; Вейрих, Стефани; Феллейзен, Матиас (1996). «Отлов ошибок в сети инвариантов программ» (PDF) . Уведомления ACM SIGPLAN . 31 (5). Ассоциация вычислительной техники (ACM): 23–32. дои : 10.1145/249069.231387 . ISSN 0362-1340 .
Дальнейшее чтение
[ редактировать ]- Кормак Фланаган; К. Рустан М. Лейно, Марк Лиллибридж, Грег Нельсон, Джеймс Б. Сакс, Рэйми Стата (2002). «Расширенная статическая проверка Java». Материалы конференции ACM SIGPLAN 2002 по проектированию и реализации языков программирования . п. 234. дои : 10.1145/512529.512558 . ISBN 978-1581134636 . S2CID 47141042 .
{{cite book}}: CS1 maint: несколько имен: список авторов ( ссылка ) - Бабич, Домагой; Ху, Алан Дж. (2008). «Калисто». Материалы 13-й международной конференции по программной инженерии - ICSE '08 . п. 211. дои : 10.1145/1368088.1368118 . ISBN 9781605580791 . S2CID 62868643 .
- Шахматы, Б.В. (2002). «Повышение компьютерной безопасности с помощью расширенной статической проверки». Материалы симпозиума IEEE 2002 г. по безопасности и конфиденциальности . стр. 160–173. CiteSeerX 10.1.1.15.2090 . дои : 10.1109/SECPRI.2002.1004369 . ISBN 978-0-7695-1543-4 . S2CID 12067758 .
- Риу, Фредерик; Чалин, Патрис (2006). «Повышение качества корпоративных веб-приложений с помощью расширенной статической проверки: практический пример» . Электронные заметки по теоретической информатике . 157 (2): 119–132. дои : 10.1016/j.entcs.2005.12.050 . ISSN 1571-0661 .
- Джеймс, Перри Р.; Чалин, Патрис (2009). «Более быстрая и полная расширенная статическая проверка языка моделирования Java». Журнал автоматизированного рассуждения . 44 (1–2): 145–174. CiteSeerX 10.1.1.165.7920 . дои : 10.1007/s10817-009-9134-9 . ISSN 0168-7433 . S2CID 14996225 .
- Сюй, Дана Н. (2006). «Расширенная статическая проверка Haskell». Материалы семинара ACM SIGPLAN 2006 года по Haskell . п. 48. CiteSeerX 10.1.1.377.3777 . дои : 10.1145/1159842.1159849 . ISBN 978-1595934895 . S2CID 1340468 .
- Лейно, К. Рустан М. (2001). «Расширенная статическая проверка: десятилетняя перспектива». Информатика . Конспекты лекций по информатике. Том. 2000. стр. 157–175. дои : 10.1007/3-540-44577-3_11 . ISBN 978-3-540-41635-7 .
- Детлефс, Дэвид Л.; Лейно, К. Рустан М.; Нельсон, Грег; Сакс, Джеймс Б. (1998). «Расширенная статическая проверка». Отчет об исследовании Compaq SRC (159).