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

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

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

Здравствуйте, Аноним, Вы писали:

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

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

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

Я более-менее подробно смотрел только PVS (читал пару туториалов, не более). Идея в следующем: написать спецификации, а затем смотреть, что из них получается — выводить теоремы и т.п. Предназначена для нахождения дыр в самих спецификациях.

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

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

А>Я более-менее подробно смотрел только PVS (читал пару туториалов, не более). Идея в следующем: написать спецификации, а затем смотреть, что из них получается — выводить теоремы и т.п. Предназначена для нахождения дыр в самих спецификациях.

Есть по крайней мере два способа использования формальных спецификаций — 1) анализ моделей и 2) использование моделей для тестирования. Первое ни в коей мере не заменяет второго: даже если модель полна, непротиворечива и обладает нужными свойствами, нет никаких гарантий, что реализованный программный продукт будет соответствовать этой модели. Делались попытки генерировать программный код из модели (например, для языка RSL был такой инструмент), но и это не помогает, потому что получающаяся правильная система обладает очень плохими характеристиками по производительности, а при "доводке" вносится количество ошибок, сравнимое с написанием заново. Кроме того, после такой "доводки" перегенерировать программу при изменении модели уже нельзя.

Реальные применения моделей для тестирования существуют. Ранее были инструменты для языков VDM и RSL. Возможно, они и сейчас есть, но в последние годы появились более интересные решения — ASML, разработанный в Microsoft, и UniTesK, разработанный нами, Институтом системного программирования РАН. Впрочем, весной этого года Microsoft приостановил развитие ASML и запустил новый проект по созданию языка спецификаций Spec#, двигаясь в том же направлении, что и UniTesK. Особенность этих подходов состоит в использовании расширений языков программирования для спецификаций — Spec# использует расширение языка C#, а UniTesK предлагает три языка на выбор — C, Java, C#.