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

Почему верификация Polyspace использует приближения

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

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

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

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

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

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