Здравствуйте уважаемые!

Интересен следующий перечень вопросов:

1) Формальная верификация. Существуют ли методы верификации кроме аксиоматического метода Хоара и индуктивных утверждений Флойда? Что такое фундированные множества и как они используются в индуктивных утверждениях Флойда?
Существуют ли совершенно иные механизмы формальной верификации?

2) Автоматизация верификации. Есть ли инструментарий автоматизирующий верификацию (понятно, что речь идёт о частичной верификации)? Если можно то перечислите их или киньте ссылки.

3) Формализация спецификаций. Использовал ли кто нибудь языка OCL для формализации спецификаций? Или данный язык ограничений не подходит для подобных задач?!

4) Тестирование циклов. В теории сказано, что цикл разворачивают в линейный код и далее его покрывают в соответствии с выбранным критерием структурного тестирования (C0, C1, C2). Однако, как это выполнимо на практике ? Существуют ли методики целенаправленного тестирования циклов ? Или например как в ручную протестировать процедуру построения функции проекции яркости изображения по адресу "pcand":

void CSomeClass::MakeProjection(BYTE *pprojection)
{
DWORD mean;

::ZeroMemory(pprojection,m_width);

for (BYTE *i=pcand;i<pcand+m_width;i++)
{
mean = 0;
for (BYTE *j=i;j<i+m_pixels;j+=m_width) mean+=*j;
*pprojection++=(BYTE)(mean/m_height);
}
}

5) Автоматизация тестирования. Существующий инструментарий? Есть ли ПО автоматизирующее структурное тестирование?


Paralax.