Верификация

Верифика́ция (от лат. verum «истинный» + facere «делать») в различных сферах деятельности человека может подразумевать:

• подтверждение того, что заданные требования выполнены, через предоставление объективных свидетельств;
• оценка соответствия продукта, услуги или системы нормам, требованиям, спецификациям или установленным условиям;
• проверка, подтверждение, метод доказательств каких-либо теоретических положений, алгоритмов, программ и процедур путём их сопоставления с опытными (эталонными или эмпирическими) данными, алгоритмами и программами;
• методика распознавания на соответствие правде;
• в науке, проверка теоретических положений на соответствие реальности при помощи эксперимента.

В значении доказуемости, проверяемости объяснений (моделей) объектов/явлений, в зависимости от степени подтверждаемости реальностью (эмпирически, фактами), образует понятия:

• Гипотеза — недоказанное утверждение (предположение) на основе ряда подтверждающих её наблюдений или суждений, понятий, постулатов (в науке).
• Концепция — модель с подтверждающими её истинность фактами или без них (см. Философия).
• Теория — объяснение с предоставлением доказательств максимальной степени (см. Наука).

Формальная верификация в информатике

Формальная верификация — доказательство с помощью формальных методов правильности или неправильности программы (системы) в соответствии с формальным описанием свойств программы (системы).

Методы формальной верификации:

• Метод аксиоматической семантики Хоара
• Метод индуктивных утверждений Флойда
• Доказательное программирование (proofing programming)
• Автоматическое доказательство теорем (Theorem proving)
• Проверка моделей (Model checking)
• Символьное выполнение (Symbolic execution)
• Абстрактная интерпретация (Abstract Interpretation).

Принцип верификации Венского кружка

В действительности идея верифицируемости не является отправной идеей представителей Венского кружка и была еще ранее сформулирована — хотя и не вполне ясно — Витгенштейном:

Предложение можно понять тогда, если мы знаем, при каких условиях оно может быть истинным. Это означает, что требуется не знание того, является ли предложение истинным или ложным, но знание обстоятельств, которые позволяют установить его истинность.ЛФТ, 4.024

Принцип верификации был выдвинут Венским кружком, в котором состоял философ-позитивист Мориц Шлик в 20-е годы XX века. Члены кружка полагали, что в науке должны остаться два класса научных предложений — аналитические истины, не имеющие предметного содержания, и фактические истины, эмпирические факты конкретных наук, значение которых может быть проверено особым способом — принципом верификации. «Очищающая» науку от метафизики процедура верификации с помощью протокольных предложений эмпирического характера лежит в основе всей программы логического позитивизма.

Верификация — процедура проверки истинности знаний. Она предполагает, что сложные предложения нужно разделить на протокольные. Истинность протокольных предложений абсолютно несомненна, так как соответствует наблюдаемой действительности. Форма протокольного предложения выглядит так: «NN наблюдал такой-то и такой-то объект в такое-то время и в таком-то месте». Сведение сложных предложений к протокольным называется редукцией. Таким образом, вся деятельность учёного сводится к проверке протокольных предложений и их обобщению. В результате процедуры верификации все метафизические вопросы попадали в категорию бессмысленных и отбрасывались. Причина этого кроется в том, что философские вопросы не могут быть посредством логической цепочки рассуждений сведены к эмпирическим утверждениям, которые их могут подтвердить или опровергнуть.

Также Шлик указывал на то, что основой нашего эмпирического знания являются так называемые констатации, как он называл предложения о «теперешнем восприятии». Такие предложения, как полагал философ, являются также однозначно определенно разрешимыми, как и предложения аналитического характера. На этой основе и было выдвинуто требование полной верификации, которое можно было бы сформулировать следующим образом:

Предложение $\Sigma$ имеет значение тогда и только тогда, когда оно не является аналитическим предложением или противоречием, и если логически следует из непротиворечивого конечного класса предложений $\Phi$, причём элементами этого класса предложений являются предложения наблюдения.

Таким образом, верификация была критерием истинности, но одновременно и способом выявления значения, и принципом разграничения эмпирического осмысленного знания и метафизического, неосмысленного.

Однако вскоре стало очевидным, что такой прямой верификационизм невозможен в тех случаях, когда мы имеем дело с событиями прошлого, с общими суждениями и т. д. Тогда этот критерий был ослаблен и появился критерий принципиальной верификации, или верифицируемости: оговаривались условия практической проверки того или иного факта. Типичным примером стало в те годы рассуждение об обратной стороне Луны, которое в принципе можно будет подтвердить, когда будет построен летательный аппарат, который облетит Луну. Уязвимым было и само понятие протокольных предложений. Внешним критиком выступал К. Поппер, считавший, что следует вводить принцип фальсификации (опровержения) в качестве критерия научности.

См. также

• Доказательство
• Фальсифицируемость
• Валидация
• Идентификация

Литература

• Синицын С. В., Налютин Н. Ю. Верификация программного обеспечения. М.:БИНОМ, 2008, 368 c. ISBN 978-5-94774-825-3