Спасибо Всем кто откликнулся на предыдущий зов!

Однако всё же несколько вопросов остались не рассмотренными.

1) Тестирование циклов. В теории сказано, что цикл разворачивают в линейный код и далее его покрывают в соответствии с выбранным критерием структурного тестирования (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);
}
}

(Как же всё таки на практике протестировать такой тривиальный пример?)

2) Формальные спецификации?
Допустим, написаны OCL ограничения как их работать с ними дальше? Возможно ли их сохранить в каком-либо формате, а затем передать в автоматизированную среду тестирования? Напишите ссылки на среды разработки формальных спецификаций (RSL, SDL, ...)

3) Да есть системы доказательства корректности (Isabelle, HOL, Coq). Можно ли их где нибудь скачать?