The post has been translated automatically. Original language: Russian
The usual test answers the question: did the program work on the examples we selected?
Formal verification raises a tougher question: can a program violate a given property with at least one valid state and set of input data?
This is exactly how SJV works now.
We describe the acceptable program states and the conditions that must be met after calling the function. For example: the counter should increase exactly by the transmitted value, the operating mode should change only in a certain way, and the rest of the data should remain unchanged.
After that, SJV does not check several pre-selected cases, but the entire range of values set by such conditions.
If a violation is possible, the check should find a specific example: the initial state, the input data, and the result in which the contract is not executed.
If there is no such example in the specified area, the program receives confirmation of the checked property.
It is important here not to turn the word "proven" into magic.
Formal verification always has limits. It refers to a specific program, a specific specification, and an explicitly defined execution model. If some of the behavior is not yet supported by the verification system, the result should not be "everything is correct", but an honest message that proof cannot be obtained.
For us, this is one of the basic principles of SJV.
It is better to get a rejection of confirmation than false confidence in correctness.
That is why formal verification differs from another set of tests. Her task is not to increase the number of test examples, but to answer a stronger question: is it possible to violate the property at all in the area that we formally asked.
Обычный тест отвечает на вопрос: сработала ли программа на выбранных нами примерах?
Формальная верификация ставит вопрос жёстче: может ли программа нарушить заданное свойство хотя бы при одном допустимом состоянии и наборе входных данных?
Именно так сейчас работает SJV.
Мы описываем допустимые состояния программы и условия, которые должны выполняться после вызова функции. Например: счётчик должен увеличиться ровно на переданное значение, режим работы должен измениться только определённым образом, а остальные данные должны остаться без изменений.
После этого SJV проверяет не несколько заранее выбранных случаев, а всю область значений, заданную такими условиями.
Если нарушение возможно, проверка должна найти конкретный пример: исходное состояние, входные данные и результат, при котором контракт не выполняется.
Если такого примера в заданной области нет, программа получает подтверждение проверяемого свойства.
Здесь важно не превращать слово «доказано» в магию.
Формальная верификация всегда имеет границы. Она относится к конкретной программе, конкретной спецификации и явно заданной модели исполнения. Если часть поведения пока не поддерживается системой проверки, результат должен быть не «всё правильно», а честное сообщение о том, что доказательство получить нельзя.
Для нас это один из основных принципов SJV.
Лучше получить отказ от подтверждения, чем ложную уверенность в корректности.
Именно поэтому формальная верификация отличается от ещё одного набора тестов. Её задача не увеличить число проверочных примеров, а ответить на более сильный вопрос: возможно ли нарушение свойства вообще в той области, которую мы формально задали.
Share
