Re: Несколько вопросов вразброс
On Tue, Jul 10, 2012 at 09:53:02PM +0400, "Артём Н." wrote:
> On 08.07.2012 17:23, Stanislav Maslovski wrote:
> > На практике ситуация такова: случаев, где возможно *полное* формальное
> > доказательство правильности программы *больше*, чем случаев, где для этого
> > достаточно *простых* тестов.
> > Как правило, построение *полного* теста эквивалентно решению исходной
> > программной задачи, и, поэтому, не имеет никакой ценности для доказательства.
> Понятно. А вообще, случаев, когда:
> 1. возможно полное доказательство;
> 2. доказательство имеет практическое значение;
> много?
Они есть. Этого уже достаточно.
> >>> Можно 1000 раз успешно прогнать *все*
> >>> комбинации входных переменных некой процедуры, а на 1001-м получить
> >>> ошибку, например, из-за утечки памяти, или из-за переполнения какой-нибудь
> >>> переменной-счётчика, которая не обнуляется между вызовами, и т.п.
> >> Значит не были протестированы _все_ состояния.
> > Задолбал! :)
> Не, ну я здесь прав. ;-)
Нет. Повторюсь: построение *полного* теста в общем случае эквивалентно решению
исходной программной задачи. Как ты собираешься доказывать правильность
самого теста? Ещё одним тестом? И так до бесконечности?
> >> Я неправильно выразился. Полное доказательство корректности достаточно сложной
> >> системы провести на практике невозможно ввиду слишком больших затрат ресурсов (и
> >> ещё возможно, из-за отсутствия метода доказательства). Так?
> > Нет. Я утверждал, что во многих случаях *полное* формальное
> > доказательство *возможно* с конечными ресурсами и за конечное время.
> > Просто это доказательство строится совсем не тем способом, который ты
> > себе представляешь.
> Каким?
Примерно так, как доказывают теоремы в математике: исходя из общих
свойств операторов программы, её исходных данных и конечного
результата.
> > Вот тебе элементарный пример: докажи теорему Пифагора *тестами* =)
> Возможно повысить уверенность в том, что алгоритм доказательства теоремы
> реализован правильно, используя тесты.
Это ещё что за новая сущность? "алгоритм доказательства теоремы"?
> Про "доказательство" тестами я ничего не писал. :-)
Да ну? А как же пресловутая проверка по "всем" состояниям?
> Кстати, а что насчёт Ада?
[...]
> Что про него можете сказать?
Кроме общих мест - ничего.
--
Stanislav
Reply to: