WikiDer > Расширенная статическая проверка

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 ВСПЭК. Однако в настоящее время не существует широко используемого языка программирования программного обеспечения, который обеспечивает расширенную статическую проверку в своей базовой среде разработки.

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

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

  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

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