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

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

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). Можно ли их где нибудь скачать?

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

Hol и Coq я видел. Скачиваются по одной из первых ссылок при поиске в google.com
Спасибо Всем кто откликнулся на предыдущий зов!

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

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). Можно ли их где нибудь скачать?