[Date Prev][Date Next] [Thread Prev][Thread Next] [Date Index] [Thread Index]

Re: Несколько вопросов вразброс



On 11.07.2012 04:18, Stanislav Maslovski wrote:
> On Tue, Jul 10, 2012 at 09:53:02PM +0400, "Артём Н." wrote:
>> On 08.07.2012 17:23, Stanislav Maslovski wrote:
>>> На практике ситуация такова: случаев, где возможно *полное* формальное
>>> доказательство правильности программы *больше*, чем случаев, где для этого
>>> достаточно *простых* тестов. 
>>> Как правило, построение *полного* теста эквивалентно решению исходной
>>> программной задачи, и, поэтому, не имеет никакой ценности для доказательства.
>> Понятно. А вообще, случаев, когда:
>> 1. возможно полное доказательство;
>> 2. доказательство имеет практическое значение;
>> много?
> Они есть. Этого уже достаточно.
Недостаточно. Достаточно было бы, если бы их на практике было просто
применить... Часто ли это применяется и просто ли?

>>>>> Можно 1000 раз успешно прогнать *все*
>>>>> комбинации входных переменных некой процедуры, а на 1001-м получить
>>>>> ошибку, например, из-за утечки памяти, или из-за переполнения какой-нибудь
>>>>> переменной-счётчика, которая не обнуляется между вызовами, и т.п.
>>>> Значит не были протестированы _все_ состояния.
>>> Задолбал! :)
>> Не, ну я здесь прав. ;-)
> Нет. Повторюсь: построение *полного* теста в общем случае эквивалентно решению
> исходной программной задачи. Как ты собираешься доказывать правильность
> самого теста? Ещё одним тестом? И так до бесконечности?
М... Ну да. Про тест я не подумал. Но, если тест - просто тупой перебиратель
результата..? Т.е., в итоге-то поведение программы всё-равно определяется тем,
что подали на входы (да, если не брать в расчёт временные характеристики
изменения входов)?

>>> Вот тебе элементарный пример: докажи теорему Пифагора *тестами* =)
>> Возможно повысить уверенность в том, что алгоритм доказательства теоремы
>> реализован правильно, используя тесты.
> Это ещё что за новая сущность? "алгоритм доказательства теоремы"?
Я именно про конкретный случай. Есть доказательство по опр. алгоритму. Тесты
позволят повысить уверенность в нём. Сейчас вспомнил, что за теорема. :-)
Например, в вики приведён пример док-ва через подобные треугольники.
И там a/c = |HB|/a, где H - точка деления гипотенузы c высотой.
В тесте возможно было бы задать конкретный треугольник через a, b и c, затем
вычислить нахождение точки H и проверить утверждение.
В данном случае, конечно, доказательство общеизвестное и сводится к теореме,
которая также доказывается общеизвестным доказательством...
Но ведь возможно, что доказательство неверно, где-то ошибка?
Тест поможет проверить несколько вариантов.
Имеет смысл его вводить?

>> Про "доказательство" тестами я ничего не писал. :-)
> Да ну? А как же пресловутая проверка по "всем" состояниям?
Это в теории. :-)


Reply to: