Версия для печати темы

Нажмите сюда для просмотра этой темы в обычном формате

Форум «Всё о Паскале» _ Теоретические вопросы _ О верификации

Автор: Altair 2.11.2006 1:05

Давайте поговорим о качестве ПО...
Верификация.
Как ее проводят, и действительно ли она гарантирует отсутствие ошибок в программе ?


Автор: lapp 2.11.2006 6:26

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

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

Как ее проводят - мне кажется, принципы самые общие, точных рекомендаций нет (пусть меня поправят).
А вот отсутствие ошибок тебе не гарантирует никто и никогда (ну, кроме программы Hello, World! smile.gif ).
Более того, я думаю, можно гарантировать их наличие в любой мало-мальски сложной проге после любой верификации.

Автор: Altair 2.11.2006 12:15

Нет!
Верификация это процесс, который именно гарантирует отсутствие ошибок.
А вот сведение их к минимуму - это тестирование..

Автор: Altair 2.11.2006 12:26

Насколько я понимаю, процесс верификации,
это математический процесс, причем мета процесс - т.е. неизвестно, когда он закончиться для конкретной программы.
Причем в сети мало информации по этому...
http://ru.wikipedia.org/wiki/%D0%92%D0%B5%D1%80%D0%B8%D1%84%D0%B8%D0%BA%D0%B0%D1%86%D0%B8%D1%8F

Автор: lapp 2.11.2006 12:38

Цитата(Altair @ 2.11.2006 9:26) *

Причем в сети мало информации по этому...
http://ru.wikipedia.org/wiki/%D0%92%D0%B5%D1%80%D0%B8%D1%84%D0%B8%D0%BA%D0%B0%D1%86%D0%B8%D1%8F

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

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

Автор: xds 2.11.2006 20:34

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

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

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

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

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

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

В прочем, объективность не существует как класс - выше изложено всего-лишь моё мнение smile.gif

Автор: Archon 3.11.2006 4:23

А кто сможет гарантировать, что ошибки нет в самом алгоритме проверки на безошибочность?

Автор: lapp 3.11.2006 7:04

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

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