Формальная верификация: различия между версиями

Нет описания правки
'''Формальная верификация''' — [[Формальные методы|формальное]] доказательство соответствия или несоответствия формального предмета верификации его формальному описанию. Предметом выступают алгоритмы, программы и другие доказательства.
В контексте программных и аппаратных систем формальная верификация — доказательство с помощью [[формальные методы|формальных методов]] корректности или некорректности (правильности или неправильности) алгоритмов, программ и систем в соответствии с формальным описанием их свойств.
 
Из-за рутинности даже простой формальной верификации и теоретической возможности её полной автоматизации под формальной верификацией обычно подразумевают автоматическую верификацию с помощью [[Компьютерная программа|программы]].
 
== Обоснование ==
== Доказательное программирование ==
Доказательное программирование — использовавшаяся в 1980-х годах в академических кругах технология разработки программ для ЭВМ с доказательствами правильности — доказательствами отсутствия ошибок в программах (понимая, в рамках данной теории, ошибки как несоответствия между программой и реализуемым ею алгоритмом).
 
== Автоматическая проверка доказательства ==
Доказательство может быть [[Автоматизированное доказательство|автоматизировано]] полностью лишь для очень небольшого круга простых теорий, поэтому важное значение получает его автоматическая проверка.
 
== См. также ==