Polyspace® Code Prover™ использует статическую верификацию, чтобы доказать отсутствие ошибок времени выполнения. Статическая верификация выводит динамические свойства программы, не выполняя её на самом деле. Статическая верификация значительно отличается от других методов, таких как отладка во время выполнения, поскольку верификация не полагается на определенный тест или набор тестов. Свойства, полученные из статической верификации, верны для всех выполнений вашей программы[1] .
Статическая верификация использует репрезентативные приближения программных операций и данных. Например, рассмотрим следующий код:
for (i=0 ; i<1000 ; ++i) {
tab[i] = foo(i);
}i никогда не переполняет область значений tabодин из подходов может заключаться в рассмотрении каждого возможного значения i. Такой подход требует тысячи проверок.При статической верификации программное обеспечение моделирует переменную по своей области. В этом случае программное обеспечение моделирует, что i относится к статическому интервалу, [0.. 999]. В зависимости от сложности данных, программное обеспечение использует более сложные модели, такие как выпуклые многогранники или целочисленные решетки для этой цели.
Приближение, по определению, приводит к потере информации. Например, верификация теряет информацию, которая i увеличивается на один каждый цикл в цикле. Однако даже без этой информации можно гарантировать, что область значений i меньше диапазона tab. Для установки этого свойства требуется только одна проверка. Поэтому статическая верификация является более эффективной по сравнению с традиционными подходами.
При выполнении приближений верификация не идет на компромисс с исчерпываемостью. Причина в том, что выполненные приближения являются верхними аппроксимациями или сверхприближениями. Другими словами, вычисленная область переменной является супермножеством ее фактической области.
[1] Свойства, полученные при статической верификации, имеют значение true только в том случае, если вы выполняете свою программу на тех же условиях, которые вы указали через опции анализа. Например, верификация по умолчанию предполагает, что указатели, полученные из внешних источников, являются ненулевыми. Если вы не задаете опцию Consider environment pointers as unsafe (-stubbed-pointers-are-unsafe)результаты верификации получаются в этом предположении. Они могут не иметь значения true во время выполнения программы, если предположение признано недействительным и из внешнего источника получен указатель со значением null.