Расширенная статическая проверка - Extended static checking

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

Методы, используемые в расширенной статической проверке, относятся к различным областям Информатика, включая статический анализ программы, символьное моделирование, проверка модели, абстрактная интерпретация, Решение SAT и автоматическое доказательство теорем и проверка типа. Расширенная статическая проверка обычно выполняется только на внутрипроцедурном уровне (а не на межпроцедурном) для масштабирования до больших программ.^[2] Кроме того, расширенная статическая проверка направлена ​​на то, чтобы сообщать об ошибках, используя спецификации, предоставленные пользователем, в виде предварительно и пост-условия, инварианты цикла и инварианты классов.

Расширенные статические шашки обычно работают путем распространения сильнейшие постусловия (соотв. самые слабые предпосылки ) внутрипроцедурно с помощью метода, начиная с предусловия (соответственно постусловия). На каждом этапе этого процесса создается промежуточное условие, которое фиксирует то, что известно в этой точке программы. Это сочетается с необходимыми условиями программного оператора в этот момент, чтобы сформировать условие проверки. Примером этого является утверждение о делении, необходимое условие которого состоит в том, что делитель быть ненулевым. Условие проверки, возникающее из этого, эффективно утверждает: учитывая промежуточное условие в этой точке, должно следовать, что делитель не равен нулю. Все условия проверки должны быть доказаны как ложные (следовательно, правильные с помощью исключен третий ), чтобы метод прошел расширенную статическую проверку (или «не удалось найти больше ошибок»). Как правило, для выполнения условий проверки используется автоматическая программа доказательства теорем.

Расширенная статическая проверка впервые появилась в ESC / Modula-3^[4] и позже, ESC / Java. Его корни берут начало в более упрощенных методах статической проверки, таких как статическая отладка.^[5] или же Lint (программное обеспечение) и FindBugs. Ряд других языков приняли ESC, в том числе Спецификация # и СПАРКАДА и VHDL ВСПЭК. Однако в настоящее время не существует широко используемого языка программирования программного обеспечения, который обеспечивает расширенную статическую проверку в своей базовой среде разработки.

Смотрите также

• Язык моделирования Java (JML)

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

1. К. Фланаган, K.R.M. Лейно, М. Лиллибридж, Г. Нельсон, Дж. Б. Сакс и Р. Стата. «Расширенная статическая проверка для Java». В Материалы конференции по проектированию и реализации языков программирования, страницы 234-245, 2002. doi: http://doi.acm.org/10.1145/512529.512558
2. «Расширенная статическая проверка». UWTV. Получено 2012-02-01.^{[постоянная мертвая ссылка ]}
3. Calysto: масштабируемая и точная расширенная статическая проверка, Домагой Бабич и Алан Дж. Ху. В материалах Международной конференции по разработке программного обеспечения (ICSE), 2008 г. Дои:10.1145/1368088.1368118
4. Расширенная статическая проверка для Modula-3, К. Рустан, М. Лейно и Грег Нельсон. В материалах конференции по созданию компиляторов, страницы 302-305, 1998. Дои:10.1007 / BFb0026418
5. Отлавливание ошибок в паутине программных инвариантов, К. Фланаган, М. Флатт, С. Кришнамурти. С. Вейрих, и M. Felleisen, страницы 23-32, 1996, dpi: http://doi.acm.org/10.1145/249069.231387

дальнейшее чтение

• Кормак Фланаган; К. Рустан М. Лейно, Марк Лиллибридж, Грег Нельсон, Джеймс Б. Сакс, Рэйми Стата (2002). Расширенная статическая проверка для Java. Труды конференции по проектированию и реализации языков программирования (PLDI). п. 234. Дои:10.1145/512529.512558. ISBN  978-1581134636.
• Бабич, Домагой; Ху, Алан Дж. (2008). Calysto: масштабируемая и точная расширенная статическая проверка. Труды Международной конференции по программной инженерии (ICSE). п. 211. Дои:10.1145/1368088.1368118. ISBN  9781605580791.
• Шахматы, Б.В. (2002). Повышение безопасности компьютера с помощью расширенной статической проверки. Материалы симпозиума IEEE по безопасности и конфиденциальности. С. 160–173. CiteSeerX  10.1.1.15.2090. Дои:10.1109 / SECPRI.2002.1004369. ISBN  978-0-7695-1543-4.
• Риу, Фредерик; Чалин, Патрис (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.
• Сюй, Дана Н. (2006). Расширенная статическая проверка для haskell. Труды семинара ACM по Haskell. п. 48. CiteSeerX  10.1.1.377.3777. Дои:10.1145/1159842.1159849. ISBN  978-1595934895.
• Лейно, К. Рустан М. (2001). Расширенная статическая проверка: десятилетняя перспектива. Информатика. Конспект лекций по информатике. 2000. С. 157–175. Дои:10.1007/3-540-44577-3_11. ISBN  978-3-540-41635-7.
• Detlefs, David L .; Лейно, К. Рустан М .; Нельсон, Грег; Сакс, Джеймс Б. (1998). «Расширенная статическая проверка». Отчет об исследовании Compaq SRC (159).