The post has been translated automatically. Original language: Russian
We are used to testing programs with tests. The developer sets the input data, runs the program, and looks to see if the result matches the expected one. The more important cases are checked, the more confident we consider the program to be reliable.
But this approach has a natural limitation. The test shows the behavior of the program in a particular case, whereas there can be a huge number of possible states and sequences of events. This is where programming unexpectedly converges with mathematics: some properties of a program can not only be tested with examples, but also tried to prove.
The test checks a separate case
Let's imagine a program that manages a simple counter. Its value can increase and decrease, but according to the conditions of the task it should never become less than zero.
You can write dozens of tests: start with different values, run different sequences of commands, and make sure everything is working correctly. This is useful and necessary, but each such test examines only one specific sequence.
If there are thousands or millions of possible sequences, it becomes difficult to check them all in this way. The more system states and transition options between them, the faster the number of possible scenarios grows.
Therefore, another question arises: is it possible to study not individual examples, but the state change rule itself?
First you need to formulate the property
Mathematical verification does not begin with the launch of a program, but with an accurate statement about it.
In the case of a counter, it may sound simple: "the value is always greater than or equal to zero." For another system, the property may be an acceptable temperature range, the correct sequence of process steps, or maintaining a certain ratio between the values.
Such statements must be unambiguous. "It"s not enough for a computer to tell you that the system should work "correctly" or "intelligently." It is necessary to determine which specific property should be preserved.
And here comes one of the main concepts of formal verification — specification. It does not describe a sequence of commands, but rather the requirements for the behavior of the system.
States and transitions
It is convenient to represent many programs as a set of states and transition rules between them.
Let's take a simple example of a device with three states:
Off → Start → Work
From the """"Off" state, it can switch to "Startup", and after successful startup, to "Operation". For each transition, you can define the conditions under which it is allowed.
After that, you can ask mathematical questions. Can the system immediately switch from an off state to an operational one? Can it end up in a state that is not provided for by the model at all? Is there always an allowed continuation after the start of the launch?
We are no longer studying a single program launch, but the structure of all acceptable transitions.
An invariant is something that must be preserved.
Properties that should remain true for all acceptable actions of the system are especially useful. In mathematics and programming, they are called invariants.
Let's go back to the counter. If a problem condition requires that its value never become negative, this can be considered an invariant.
Then the reasoning is built in two stages. First, the initial state is checked: the condition is met. Then each operation is reviewed and it is checked whether it preserves this condition.
If all valid operations preserve the property, there is no need to manually iterate through each possible sequence of actions.
This is already very similar to the usual mathematical proof.
When there are few states, you can sort them out.
There is another approach. If the model is relatively small, the program can automatically build achievable states and check the required property in each of them.
Let's imagine a simple machine, timer, or a small data exchange protocol. Each has a limited number of states and allowed transitions. The computer can sequentially examine them and look for a condition that violates a given condition.
If there is such a condition, it is not only the fact of the error itself that is useful. You can get the sequence of steps that led to it.
This helps to see the problem not as an accidental failure, but as a consequence of specific system rules.
Formal verification is not a substitute for tests
It may seem that the mathematical proof makes the usual tests unnecessary. In practice, these are different tools.
Testing verifies real-world examples, component interactions, and specific program performance well. Formal methods are especially useful where it is important to establish some common property for a set of possible states.
In addition, the proof only applies to what was stated in the specification. If an important requirement is not included in it, no verification will detect it on its own.
You can ideally prove the correctness of a property that turned out to be the wrong property that was really needed.
Therefore, the quality of the requirements formulation is no less important than the verification itself.
Why is music appearing here again
In the previous examples in this series, music provided a convenient model. A person hears a phrase and often immediately notices that one note or one rhythmic accent is out of place.
But if you ask a person to explain the exact reason, the task becomes more difficult. We need to formulate a rule: which notes are acceptable, where the sound can start, how long the beat lasts, and which deviations we consider acceptable.
This wording is mandatory for the program. It does not possess our musical sense and therefore works only with explicitly defined properties.
From a mathematical point of view, the difference is very interesting. A person is able to first feel a violation, and then look for a rule that has been violated. In formal verification, the order is reversed: first, a rule is set, and then its compliance is checked.
A program as a mathematical object
Code is usually perceived as a set of commands for a computer. But the same program can be viewed differently: as a set of states and transition rules between them.
After that, mathematical concepts appear. There are acceptable values, transition conditions, state properties, and invariants that must be preserved.
And then the question "does the program work?" is divided into two different questions.
First, does it show the correct result in the examples we have tested?
The second question is: what properties of its behavior follow from the very design of the system?
The first question leads to testing. The second is for formal verification.
They don't compete with each other. Together, they provide a more complete picture of the program: tests show its work using concrete examples, and mathematics helps to reason about whole classes of possible behavior.
And this is perhaps the most interesting combination of mathematics and programming. The program can not only be executed. In some cases, it can be argued about in much the same way as a theorem.
Мы привыкли проверять программы тестами. Разработчик задаёт входные данные, запускает программу и смотрит, соответствует ли результат ожидаемому. Чем больше важных случаев проверено, тем увереннее мы считаем программу надёжной.
Но у этого подхода есть естественное ограничение. Тест показывает поведение программы в конкретном случае, тогда как возможных состояний и последовательностей событий может быть огромное количество. Здесь программирование неожиданно сближается с математикой: некоторые свойства программы можно не только проверить на примерах, но и попытаться доказать.
Тест проверяет отдельный случай
Представим программу, которая управляет простым счётчиком. Его значение может увеличиваться и уменьшаться, но по условиям задачи никогда не должно становиться меньше нуля.
Можно написать десятки тестов: начать с разных значений, выполнить разные последовательности команд и убедиться, что всё работает правильно. Это полезно и необходимо, но каждый такой тест исследует только одну конкретную последовательность.
Если возможных последовательностей тысячи или миллионы, проверить их все таким способом становится трудно. Чем больше состояний системы и вариантов перехода между ними, тем быстрее растёт число возможных сценариев.
Поэтому возникает другой вопрос: можно ли исследовать не отдельные примеры, а само правило изменения состояния?
Сначала нужно сформулировать свойство
Математическая проверка начинается не с запуска программы, а с точного утверждения о ней.
В случае со счётчиком оно может звучать просто: «значение всегда больше или равно нулю». Для другой системы свойством может быть допустимый диапазон температуры, правильная последовательность этапов процесса или сохранение определённого отношения между величинами.
Такие утверждения должны быть однозначными. Компьютеру недостаточно сказать, что система должна работать «правильно» или «разумно». Нужно определить, какое конкретное свойство должно сохраняться.
И здесь появляется одно из основных понятий формальной верификации — спецификация. Она описывает не последовательность команд, а требования к поведению системы.
Состояния и переходы
Многие программы удобно представить как набор состояний и правил перехода между ними.
Возьмём простой пример устройства с тремя состояниями:
Выключено → Запуск → Работа
Из состояния «Выключено» оно может перейти в «Запуск», а после успешного запуска — в «Работу». Для каждого перехода можно определить условия, при которых он разрешён.
После этого можно задавать уже математические вопросы. Может ли система сразу перейти из выключенного состояния в рабочее? Может ли она оказаться в состоянии, которое вообще не предусмотрено моделью? Всегда ли после начала запуска существует разрешённое продолжение?
Мы изучаем уже не отдельный запуск программы, а структуру всех допустимых переходов.
Инвариант — то, что должно сохраняться
Особенно полезны свойства, которые должны оставаться истинными при любых допустимых действиях системы. В математике и программировании их называют инвариантами.
Вернёмся к счётчику. Если условие задачи требует, чтобы его значение никогда не становилось отрицательным, это можно считать инвариантом.
Тогда рассуждение строится в два этапа. Сначала проверяется начальное состояние: условие выполняется. Затем рассматривается каждая операция и проверяется, сохраняет ли она это условие.
Если все допустимые операции сохраняют свойство, нет необходимости вручную перебирать каждую возможную последовательность действий.
Это уже очень похоже на обычное математическое доказательство.
Когда состояний немного, их можно перебрать
Есть и другой подход. Если модель сравнительно небольшая, программа может автоматически построить достижимые состояния и проверить требуемое свойство в каждом из них.
Представим простой автомат, таймер или небольшой протокол обмена данными. У каждого есть ограниченное число состояний и разрешённых переходов. Компьютер может последовательно исследовать их и искать состояние, нарушающее заданное условие.
Если такое состояние находится, полезен не только сам факт ошибки. Можно получить последовательность шагов, которая к ней привела.
Это помогает увидеть проблему не как случайный сбой, а как следствие конкретных правил системы.
Формальная проверка не заменяет тесты
Может показаться, что математическое доказательство делает обычные тесты ненужными. На практике это разные инструменты.
Тестирование хорошо проверяет реальные примеры, взаимодействие компонентов и конкретные результаты работы программы. Формальные методы особенно полезны там, где важно установить некоторое общее свойство для множества возможных состояний.
Кроме того, доказательство относится только к тому, что было сформулировано в спецификации. Если важное требование в неё не попало, никакая проверка сама его не обнаружит.
Можно идеально доказать правильность свойства, которое оказалось не тем свойством, которое действительно было нужно.
Поэтому качество формулировки требований не менее важно, чем сама проверка.
Почему здесь снова появляется музыка
В предыдущих примерах этой серии музыка давала удобную модель. Человек слышит фразу и часто сразу замечает, что одна нота или один ритмический акцент оказался не на месте.
Но если попросить человека точно объяснить причину, задача становится сложнее. Нужно сформулировать правило: какие ноты допустимы, где может начаться звук, сколько длится такт и какие отклонения мы считаем приемлемыми.
Для программы такая формулировка обязательна. Она не обладает нашим музыкальным ощущением и поэтому работает только с явно заданными свойствами.
С математической точки зрения разница очень интересна. Человек способен сначала почувствовать нарушение, а потом искать правило, которое было нарушено. При формальной проверке порядок обратный: сначала задаётся правило, а затем проверяется его соблюдение.
Программа как математический объект
Код обычно воспринимается как набор команд для компьютера. Но ту же программу можно рассматривать иначе: как множество состояний и правил перехода между ними.
После этого появляются математические понятия. Есть допустимые значения, условия переходов, свойства состояний и инварианты, которые должны сохраняться.
И тогда вопрос «работает ли программа?» разделяется на два разных вопроса.
Первый: показывает ли она правильный результат в проверенных нами примерах?
Второй: какие свойства её поведения следуют из самой конструкции системы?
Первый вопрос ведёт к тестированию. Второй — к формальной верификации.
Они не конкурируют друг с другом. Вместе они дают более полное представление о программе: тесты показывают её работу на конкретных примерах, а математика помогает рассуждать о целых классах возможного поведения.
И в этом, пожалуй, самое интересное соединение математики и программирования. Программу можно не только выполнить. В некоторых случаях о ней можно рассуждать почти так же, как о теореме.
Share
