Документация

Почему при проверке в полиспейсе используются аппроксимации

Polyspace ® Code Prover™ использует статическую проверку для подтверждения отсутствия ошибок во время выполнения. Статическая проверка выводит динамические свойства программы без ее фактического выполнения. Статическая проверка значительно отличается от других методов, таких как отладка во время выполнения, поскольку проверка не зависит от конкретного тестового случая или набора тестовых случаев. Свойства, полученные при статической проверке, верны для всех выполнений ^{программы [}1].

Статическая проверка использует репрезентативные аппроксимации программных операций и данных. Например, рассмотрим следующий код:

for (i=0 ; i<1000 ; ++i)  {
   tab[i] = foo(i); 
}

При статической проверке программное обеспечение моделирует переменную по своей области. В этом случае программное обеспечение моделирует i принадлежит статическому интервалу [0.. 999]. В зависимости от сложности данных программное обеспечение использует для этой цели более сложные модели, такие как выпуклые многогранники или целые решетки.

Приближение, по определению, приводит к потере информации. Например, проверка теряет информацию, которая i увеличивается на один каждый цикл в цикле. Однако даже без этой информации можно гарантировать, что диапазон i меньше диапазона tab. Для установления этого свойства требуется только одна проверка. Поэтому статическая проверка является более эффективной по сравнению с традиционными подходами.

При выполнении аппроксимаций проверка не идет на компромисс с полнотой. Причина заключается в том, что выполняемые аппроксимации являются верхними аппроксимациями или сверхаппроксимациями. Другими словами, вычисленная область переменной является надмножеством ее фактической области.