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

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

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.

Здравствуйте, Paralax, Вы писали:

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

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

Нам тоже

А вообще, на мой взгляд, ты слишком много хочешь для одного вопроса на форуме.
По твоим вопросам знающий человек (я не из них ) книжку написать сможет.

А вот задал бы ты, например, вопрос только про средства автоматического тестирования,
то сразу бы получил ссылки на Rational Robot, SilkTest
и семейство "фреймфорков" для модульного тестирования (CppUnit, JUnit)

По поводу специфицирования...
Наверное все зависит от типа систем. Кое-что удается совершенно формально специфицировать,
а многие вещи — нет. В жизни очень часть спецификации системы
предназначены прежде всего для людей, чтобы разработчик понял что нужно разрабатывать
а тестер — что и как нужно тестировать...

То, что удается формально специфицировать, то можно пытаться формально верефицировать...
Например протоколы, парсеры...

Здравствуйте, Paralax, Вы писали:


Я тож не большой спец.
Но мода на верификацию прошла давно. По крайней мере, в России литература последняя где-то середины восьмидесятых.
После нее был Дейкстра "Дисциплина программирования", в которой излагается идея и кое-какой формальный аппарат выводах правильных программ. Потом Грис целый учебник написал "Наука программирования". Может там ссылки найдешь.

Здравствуйте, LaptevVV, Вы писали:

LVV>Но мода на верификацию прошла давно. По крайней мере, в России литература последняя где-то середины восьмидесятых.
Ну что Вы. На Западе это можно сказать самый писк(не в IT, конечно).

Можно поискать по VDM или Z notation.
Для начинающих неплохая книга: Caroll Morgan, Programming from specifications. Где-то я ее видел.

Здравствуйте, Paralax, Вы писали:

P>2) Автоматизация верификации. Есть ли инструментарий автоматизирующий верификацию (понятно, что речь идёт о частичной верификации)?
Инструментов масса. Например, "редакторы доказательств". Они ничего не доказывают, но проверяют ваши доказательства.
Пытаются применять и общие "системы доказательства теорем" (Isabelle, HOL, Coq).

Ну и самый простой способ найти информацию google:"formal methods"

Здравствуйте, Трурль, Вы писали:

Т>Здравствуйте, Paralax, Вы писали:

P>>2) Автоматизация верификации. Есть ли инструментарий автоматизирующий верификацию (понятно, что речь идёт о частичной верификации)?
Т>Инструментов масса. Например, "редакторы доказательств". Они ничего не доказывают, но проверяют ваши доказательства.
Т>Пытаются применять и общие "системы доказательства теорем" (Isabelle, HOL, Coq).

А на практике их используют?

Здравствуйте, Трурль, Вы писали:

LVV>>Но мода на верификацию прошла давно. По крайней мере, в России литература последняя где-то середины восьмидесятых.
Т>Ну что Вы. На Западе это можно сказать самый писк(не в IT, конечно).
Ну. надо сделать конечно, уточнение — в России. Позащищали диссеры, как обычно, и забыли.
Т>Можно поискать по VDM или Z notation.
Т>Для начинающих неплохая книга: Caroll Morgan, Programming from specifications. Где-то я ее видел.
Спасибо за информацию, посмотрим.

Здравствуйте, bkat, Вы писали:

B>А на практике их используют?
Наукой зафиксированы единичные случаи.

Здравствуйте, Трурль, Вы писали:

Т>Здравствуйте, bkat, Вы писали:

B>>А на практике их используют?
Т>Наукой зафиксированы единичные случаи.

Интересно, если нечто (я имею реализацию) можно формально доказать (верифицировать),
то это возможно только при наличии формальных спецификаций.
Но если такие спецификации существуют, то скорей всего можно
и автоматически строить код (кодогенерация), который бы решал эту задачу.
Но тогда этот код нет смысла верифицировать.
Достаточно просто верифицировать/протестировать кодогенератор.
Т.е. получается, что в тех случаях, когда верификация кода возможна,
то она одновременно и бесполезна

Здравствуйте, bkat, Вы писали:

B>Интересно, если нечто (я имею реализацию) можно формально доказать (верифицировать),
B>то это возможно только при наличии формальных спецификаций.
B>Но если такие спецификации существуют, то скорей всего можно
B>и автоматически строить код (кодогенерация), который бы решал эту задачу.
B>Но тогда этот код нет смысла верифицировать.
B>Достаточно просто верифицировать/протестировать кодогенератор.
B>Т.е. получается, что в тех случаях, когда верификация кода возможна,
B>то она одновременно и бесполезна

Возьмем такую спецификацию sqrt(x) = t: |t*t-x|< err.
Сгенерировать по ней код для sqrt пока задача нереальная.
В то же время доказательства различных программ, вычисляющих эту функцию достаточно просты.

Здравствуйте, bkat, Вы писали:

B>Интересно, если нечто (я имею реализацию) можно формально доказать (верифицировать),
B>то это возможно только при наличии формальных спецификаций.
B>Но если такие спецификации существуют, то скорей всего можно
B>и автоматически строить код (кодогенерация), который бы решал эту задачу.
B>Но тогда этот код нет смысла верифицировать.
B>Достаточно просто верифицировать/протестировать кодогенератор.
B>Т.е. получается, что в тех случаях, когда верификация кода возможна,
B>то она одновременно и бесполезна

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

Например, возьмем спецификацию команд машины и требование для любого N найти первые N простых чисел за кол-во операций не более f(N). Вот и сделай для этого для кодогенератор. Точно так же можно специфицировать требования к уборщику мусора, контейнеру, базе данных.

Здравствуйте, Трурль, Вы писали:

Т>Здравствуйте, bkat, Вы писали:

B>>Интересно, если нечто (я имею реализацию) можно формально доказать (верифицировать),
B>>то это возможно только при наличии формальных спецификаций.
B>>Но если такие спецификации существуют, то скорей всего можно
B>>и автоматически строить код (кодогенерация), который бы решал эту задачу.
B>>Но тогда этот код нет смысла верифицировать.
B>>Достаточно просто верифицировать/протестировать кодогенератор.
B>>Т.е. получается, что в тех случаях, когда верификация кода возможна,
B>>то она одновременно и бесполезна

Т>Возьмем такую спецификацию sqrt(x) = t: |t*t-x|< err.
Т>Сгенерировать по ней код для sqrt пока задача нереальная.
Т>В то же время доказательства различных программ, вычисляющих эту функцию достаточно просты.

Должны ли быть программа, вычисляющая sqrt, написана каким-то особым образом,
допускающим верификацию? Или можно успешно верифицировать любую реализацию?

Здравствуйте, mihoshi, Вы писали:

M>Здравствуйте, bkat, Вы писали:

B>>Интересно, если нечто (я имею реализацию) можно формально доказать (верифицировать),
B>>то это возможно только при наличии формальных спецификаций.
B>>Но если такие спецификации существуют, то скорей всего можно
B>>и автоматически строить код (кодогенерация), который бы решал эту задачу.
B>>Но тогда этот код нет смысла верифицировать.
B>>Достаточно просто верифицировать/протестировать кодогенератор.
B>>Т.е. получается, что в тех случаях, когда верификация кода возможна,
B>>то она одновременно и бесполезна

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

M>Например, возьмем спецификацию команд машины и требование для любого N найти первые N простых чисел за кол-во операций не более f(N). Вот и сделай для этого для кодогенератор. Точно так же можно специфицировать требования к уборщику мусора, контейнеру, базе данных.

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

SPARK.

B>А что теория рекомендует?

Вот здесь есть пример доказательства методом Хоара.

Здравствуйте, bkat, Вы писали:

B>Должны ли быть программа, вычисляющая sqrt, написана каким-то особым образом,
B>допускающим верификацию? Или можно успешно верифицировать любую реализацию?

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

Здравствуйте, Paralax, Вы писали:


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



P>Что такое фундированные множества и как они используются в индуктивных утверждениях Флойда?

Если мне не изменяет память, то фундированные множества — это множества которые не имеют бесконечно убывающих цепей. В качестве примера такого множества можно привести {1 / 2**n}. Эти множества часто используют для доказательства полной корректности (завершаемости) дизайна алгоритма.

P>Существуют ли совершенно иные механизмы формальной верификации?

Здравствуйте, bkat, Вы писали:

B>А можно, очень кратко рассказать об идеях верификации программ.
B>Ну есть у нас с одной стороны спецификация, а с другой — текст программы.
B>Дальше что?
B>Первое, что приходит в голову — это попытка выявить классы эквивалентности входных данных
B>и пробные запуски этой функции с учетом найденных классов...
B>А что теория рекомендует?

Во-первых, это все надо свести к набору формальных утверждений (термов), описывающих машину и программу. Кстати, если программа — функциональная, то это сделать обычно проще на порядки. Потом взять набор правил выведения одних вернгых утверждений из других, типа "Для любых утверждений A и B если верно A и верно B и верно 'Если А и В, то С', то верно С". Теперь можно бать выражения из верных, подставлять их в правила и получать новые верные утверждения. Цель игры — получить верное утверждение "Эта программа решает эту задачу на этой машине". Если это удалось и утверждения, изначально принятые верными были действительно таковыми, то программа абсолютно верна.

Можно доказывать примерно так, как ты сказал, разбить на классы эквивалентности, локазать, что внятри одного класса программа ведет себя одинаково (т.е. верно или неверно для всех элементов класса), "провести пробный запуск" для каждого класса тем или иным способом и удостовериться в правильности для всех запусков. Это будет доказательством.

Программы автоматизации доказательств (HOL, Coq, Isabelle) котролируют процесс выведения. В некоторых случаях они могут сами найти цепочку применений правил для выведения заданного утверждения, в некоторых — нет. Но в любом случае не дают ошибиться при выводе.