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 и проверить утверждение. В данном случае, конечно, доказательство общеизвестное и сводится к теореме, которая также доказывается общеизвестным доказательством... Но ведь возможно, что доказательство неверно, где-то ошибка? Тест поможет проверить несколько вариантов. Имеет смысл его вводить? >> Про "доказательство" тестами я ничего не писал. :-) > Да ну? А как же пресловутая проверка по "всем" состояниям? Это в теории. :-) -- To UNSUBSCRIBE, email to [email protected] with a subject of "unsubscribe". Trouble? Contact [email protected] Archive: http://lists.debian.org/[email protected]
