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