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 -- To UNSUBSCRIBE, email to [email protected] with a subject of "unsubscribe". Trouble? Contact [email protected] Archive: http://lists.debian.org/[email protected]
