The post has been translated automatically. Original language: Russian
Usually, the quality of the program is checked by tests. The developer sets the input data, runs the code, and compares the result with the expected result.
This approach is necessary, but it has an obvious limitation: the test covers only those situations that have been selected for verification.
For some systems, this is not enough. If the cost of the error is high, we would like to get a stronger guarantee — to establish that certain undesirable behavior is impossible.
Formal verification solves this problem.
What does "right" mean?
Before proving anything, it is necessary to define the requirements precisely.
Let's take a function that selects the larger of two numbers. In the usual description, you can write:
the function should return the maximum value.
That's enough for a human. For mathematical verification, the requirement must be made precise.
If the input values are designated as a and b, and the result as r, then the result must be at least each input value and simultaneously coincide with one of them.
This creates a formal specification, a strict description of the required behavior.
It is the specification that defines what is considered correct in this case.
How does the proof differ from the test?
You can test the function using several examples.:
1 and 2, 100 and 7, -5 and -9.
But successful completion of these checks speaks only about these specific inputs.
During formal verification, another statement is considered.:
for any valid combination of input data, the result conforms to the specification.
The difference is fundamental.
Testing examines individual cases. Formal verification works with a property that must be preserved over the entire specified state space.
Before and after the execution
It is convenient to describe many requirements in terms of conditions before and after the operation.
For example, for division, it is necessary to require in advance that the divisor is not equal to zero. After performing the operation, the result must match the specified division rule.
The first condition is called a precondition, the second is a postcondition.
Then the task is formulated as follows:
if the initial conditions are met, does the program guarantee the required end state?
For cycles and long-term operating systems, additional properties are set that must be maintained during operation. Such properties are called invariants.
For example, if the account balance cannot be negative according to the rules of the system, this condition can be checked after each acceptable transaction.
How to work with a large number of states
Even a small program quickly generates a huge number of possible execution options.
The state is affected by variable values, memory contents, branches, loops, the sequence of previous actions, and external events.
It is often impossible to go through all the usual tests.
Formal methods allow us to describe entire sets of states at once and investigate whether a state exists among them that violates a given property.
If a violation is possible, the verification tool can show a counterexample: a specific situation in which the requirement is not met.
This result is especially useful to the developer because it turns an abstract problem into a reproducible scenario.
If the violation is impossible within the given model and accepted assumptions, the property can be considered proven.
What properties can be checked?
Formal verification is used not only to verify the result of calculations.
It can be used, for example, to establish that there is no way out of the allowed memory boundaries, check access rules, exclude a dangerous state of the system, or confirm the correctness of state transitions.
In critical systems, this approach is important: instead of the general phrase "the program is reliable", a specific property is formulated, after which its implementation is checked.
Therefore, the expression "formally verified program" requires clarification.
It's more correct to ask:
what properties of this program have been proven?
The proof depends on the specification
There is an important limitation.
Formal verification does not determine on its own what the user or the customer wanted. It checks the compliance of a given model.
Let's imagine that according to business rules, the maximum discount should be 20 percent, but the specification mistakenly specified 30 percent.
The program can flawlessly implement this specification, and mathematical verification will not detect a contradiction with the original business requirement if it was not included in the model.
Therefore, the quality of the specification is no less important than the quality of the implementation.
Mathematics can prove that a program meets the requirements, but the requirements themselves must first be formulated correctly.
Why Architecture matters
The more hidden states and complex interactions there are within a system, the more difficult it is to analyze it.
Therefore, it is desirable to take into account verifiability during the design process.
Clear component boundaries, small interfaces, explicit rules for changing state, and minimizing undefined behavior greatly simplify the proof of properties.
This leads to an important engineering conclusion:
It is useful to initially design a system that is planned to be formally tested with this goal in mind.
Formal verification is not just an additional check of the finished code. It can affect the software architecture itself.
What can be proved in the end
The correct wording sounds like this:
It can be mathematically proved that a program, under given conditions, conforms to a certain formal specification.
This is not a promise of the absolute absence of any errors.
But this is a much stronger statement than saying that the program has successfully passed a certain set of tests.
However, the problem of trust does not end there.
The source code is usually converted by the compiler into machine instructions, executed in the operating system environment, and only then gets into the processor.
Even a perfectly proven program depends on the correctness of these underlying components.
Therefore, the next question of the series:
is it possible to build a continuous chain of trust from the source code to the processor itself?
Обычно качество программы проверяют тестами. Разработчик задаёт входные данные, запускает код и сравнивает полученный результат с ожидаемым.
Этот подход необходим, но у него есть очевидное ограничение: тест охватывает только те ситуации, которые были выбраны для проверки.
Для некоторых систем этого недостаточно. Если цена ошибки высока, хотелось бы получить более сильную гарантию — установить, что определённое нежелательное поведение невозможно.
Такую задачу решает формальная верификация.
Что значит «правильно»
Прежде чем что-либо доказывать, необходимо точно определить требования.
Возьмём функцию, которая выбирает большее из двух чисел. В обычном описании можно написать:
функция должна вернуть максимальное значение.
Для человека этого достаточно. Для математической проверки требование нужно сделать точным.
Если входные значения обозначить как a и b, а результат как r, то результат должен быть не меньше каждого входного значения и одновременно совпадать с одним из них.
Так появляется формальная спецификация — строгое описание требуемого поведения.
Именно спецификация определяет, что в данном случае считается корректностью.
Чем доказательство отличается от теста
Можно проверить функцию на нескольких примерах:
1 и 2, 100 и 7, -5 и -9.
Но успешное прохождение этих проверок говорит только об этих конкретных входах.
При формальной верификации рассматривается другое утверждение:
для любого допустимого сочетания входных данных результат соответствует спецификации.
Разница принципиальная.
Тестирование исследует отдельные случаи. Формальная проверка работает со свойством, которое должно сохраняться на всём заданном пространстве состояний.
До и после выполнения
Многие требования удобно описывать через условия до начала операции и после её завершения.
Например, для деления необходимо заранее потребовать, чтобы делитель не был равен нулю. После выполнения операции результат должен соответствовать заданному правилу деления.
Первое условие называют предусловием, второе — постусловием.
Тогда задача формулируется так:
если начальные условия соблюдены, гарантирует ли выполнение программы требуемое конечное состояние?
Для циклов и длительно работающих систем дополнительно задают свойства, которые должны сохраняться во время работы. Такие свойства называют инвариантами.
Например, если баланс счёта по правилам системы не может быть отрицательным, это условие можно проверять после каждой допустимой операции.
Как работать с большим количеством состояний
Даже небольшая программа быстро порождает огромное число возможных вариантов выполнения.
На состояние влияют значения переменных, содержимое памяти, ветвления, циклы, последовательность предыдущих действий и внешние события.
Перебрать всё обычными тестами зачастую невозможно.
Формальные методы позволяют описывать сразу целые множества состояний и исследовать, существует ли среди них состояние, нарушающее заданное свойство.
Если нарушение возможно, инструмент проверки может показать контрпример: конкретную ситуацию, в которой требование не выполняется.
Такой результат особенно полезен разработчику, потому что он превращает абстрактную проблему в воспроизводимый сценарий.
Если же нарушение невозможно в пределах заданной модели и принятых предположений, свойство может считаться доказанным.
Какие свойства можно проверять
Формальная верификация применяется не только для проверки результата вычислений.
Она может использоваться, например, чтобы установить отсутствие выхода за разрешённые границы памяти, проверить правила доступа, исключить опасное состояние системы или подтвердить корректность переходов между состояниями.
В критических системах важен именно такой подход: вместо общей фразы «программа надёжна» формулируется конкретное свойство, после чего проверяется его выполнение.
Поэтому выражение «формально верифицированная программа» требует уточнения.
Правильнее спрашивать:
какие свойства этой программы были доказаны?
Доказательство зависит от спецификации
Есть важное ограничение.
Формальная верификация не определяет самостоятельно, чего хотел пользователь или заказчик. Она проверяет соответствие заданной модели.
Представим, что по бизнес-правилам максимальная скидка должна составлять 20 процентов, но в спецификации ошибочно указали 30 процентов.
Программа может безупречно реализовать эту спецификацию, и математическая проверка не обнаружит противоречия с исходным бизнес-требованием, если оно не было включено в модель.
Поэтому качество спецификации не менее важно, чем качество реализации.
Математика способна доказать соответствие программы требованиям, но сами требования сначала должны быть сформулированы правильно.
Почему архитектура имеет значение
Чем больше скрытых состояний и сложных взаимодействий внутри системы, тем труднее её анализировать.
Поэтому верифицируемость желательно учитывать ещё во время проектирования.
Чёткие границы компонентов, небольшие интерфейсы, явные правила изменения состояния и минимизация неопределённого поведения значительно упрощают доказательство свойств.
Отсюда следует важный инженерный вывод:
систему, которую планируется формально проверять, полезно изначально проектировать с учётом этой цели.
Формальная верификация — не только дополнительная проверка готового кода. Она может влиять на саму архитектуру программного обеспечения.
Что в итоге можно доказать
Корректная формулировка звучит так:
можно математически доказать, что программа при заданных условиях соответствует определённой формальной спецификации.
Это не обещание абсолютного отсутствия любых ошибок.
Но это значительно более сильное утверждение, чем сообщение о том, что программа успешно прошла некоторый набор тестов.
На этом, однако, проблема доверия не заканчивается.
Исходный код обычно преобразуется компилятором в машинные инструкции, выполняется в среде операционной системы и только затем попадает в процессор.
Даже идеально доказанная программа зависит от правильности этих нижележащих компонентов.
Поэтому следующий вопрос серии:
можно ли построить непрерывную цепочку доверия от исходного кода до самого процессора?
Share
