Помощь - Поиск - Пользователи - Календарь
Полная версия: О верификации
Форум «Всё о Паскале» > Pascal, Object Pascal > Теоретические вопросы
Altair
Давайте поговорим о качестве ПО...
Верификация.
Как ее проводят, и действительно ли она гарантирует отсутствие ошибок в программе ?

Lapp
Цитата(Altair @ 1.11.2006 22:05) *

действительно ли она гарантирует отсутствие ошибок в программе ?

Как ее проводят - мне кажется, принципы самые общие, точных рекомендаций нет (пусть меня поправят).
А вот отсутствие ошибок тебе не гарантирует никто и никогда (ну, кроме программы Hello, World! smile.gif ).
Более того, я думаю, можно гарантировать их наличие в любой мало-мальски сложной проге после любой верификации.
Altair
Нет!
Верификация это процесс, который именно гарантирует отсутствие ошибок.
А вот сведение их к минимуму - это тестирование..
Altair
Насколько я понимаю, процесс верификации,
это математический процесс, причем мета процесс - т.е. неизвестно, когда он закончиться для конкретной программы.
Причем в сети мало информации по этому...
Википедия
Lapp
Цитата(Altair @ 2.11.2006 9:26) *

Причем в сети мало информации по этому...
Википедия

Да уж если судить по этой ссылке, то вообще практически ноль - о переводе с латыни я худо-бедно сам догадался...

Альтаир, если ты имеешь в виду существование формальной возможности процесса, который находит все ошибки - ну, что ж, возможно, что таковое доказательство есть. А толку?..
Вот, скажем, была доказана "гипотеза четырех красок". Доказана с помощью компьютера, то есть сложного алгоритма, невозможного без компа - и наверняка там не обошлось без применения теорем типа такой. Но тем не менее, в первом доказательстве была-таки найдена ошибка! Правда, после ее исправления доказательство считается верным по сей день.. smile.gif
Не знаю, по делу ли я.. Но трудно представить себе наличие алгоритма верификации, верного для всех проблем.
xds
Цитата
...действительно ли она гарантирует отсутствие ошибок в программе ?

Цитата
Верификация это процесс, который именно гарантирует отсутствие ошибок.

Сам ответил smile.gif

Цитата
Как ее проводят <...>?

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

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

В прочем, объективность не существует как класс - выше изложено всего-лишь моё мнение smile.gif
Archon
А кто сможет гарантировать, что ошибки нет в самом алгоритме проверки на безошибочность?
Lapp
Цитата(xds @ 2.11.2006 17:34) *
Отсутствие ошибок не гарантировано в принципе.
Цитата(Archon @ 3.11.2006 1:23) *
А кто сможет гарантировать, что ошибки нет в самом алгоритме проверки на безошибочность?

Я так понял, что Альтаир говорил о приципиальной возможности существования такого алгоритма. Вопрос не праздный, конечно. Можно сравнить с известной "Гипотезой континуума", которая была решена, и решение гласило, что доказательство наличия или отсутствия промежуточной между алеф-ноль и алеф-один мощности не может быть получено вообще в рамках существующей системы аксиом. Так и здесь, вопрос заключается в том - а существует ли такой прцесс хотя бы теоретически? Мне кажется, интересующихся этой проблемой можно отослать к книге Пойа "Теория доказательств" - если не за решением, то хотя бы за правильной постановкой.
Но к практике это не имеет ни малейшего отношения. Более того, ошибки наверняка кроются не только в программных кодах, но и в проектах, и даже в ТЗ на программные системы. Как грится, "Оставь надежды.." smile.gif
Это текстовая версия — только основной контент. Для просмотра полной версии этой страницы, пожалуйста, нажмите сюда.