The post has been translated automatically. Original language: Russian
The thesis
Tests and models exist alongside the program.
This creates a gap between the requirements and the code.
If an important condition can be written directly in the program, it can be checked automatically during analysis or execution.
This is how preconditions, postconditions, and invariants appear.
Review
The precondition describes what must be true before performing the operation.
The postcondition specifies the result to be obtained after its execution.
The invariant defines a rule that must always be maintained.
Consider the engine speed change function.
Before executing, you may require that the new value be within the acceptable range.
After the execution, you can check that the speed has actually changed to the set value.
The invariant may prohibit the operation of the engine in case of a system emergency.
Such conditions become part of the program description.
They no longer depend only on individual tests.
Decision
The basic idea is to separate the description of the required behavior from specific examples.
Instead of a test with a speed of 50, you can write a rule that the speed should always be less than the set limit.
Instead of checking a single money transfer, you can set a condition that the balance cannot become negative.
After that, the tools can use these rules in different ways.
They can be checked while the program is running.
They can be analyzed before launch.
Additional checks can be built on their basis.
With a more rigorous approach, you can try to prove that a violation of the condition is impossible.
Dignities
The main advantage is the explicit description of the requirements.
The developer does not need to restore the meaning of the program only by its code and tests.
The conditions are next to the logic they relate to.
This helps to detect errors earlier.
Some violations can be found even before the program is launched.
Contracts also make it easier to verify individual parts of a large system.
You can define separately what the function accepts and what it is required to guarantee.
Disadvantages
Contracts do not appear automatically.
They must be formulated correctly by the developer.
If an important rule is not written down, the system will not check it.
Conditions that are too complex can be difficult to analyze.
This is especially noticeable in programs with a large number of states and relationships between objects.
The run-time check also has a limitation.
It detects a violation only when the program has actually entered the appropriate state.
The very existence of an invariant does not mean that it has been proven for all possible execution paths.
Conclusion
Contracts and invariants take an important step from external testing to internal description of the correctness of the program.
Now the requirements are becoming part of its structure.
But the next question remains.
Is it possible to check such conditions not on separate runs, but for multiple possible program execution paths at once?
To do this, the methods of symbolic execution and automatic proof of properties are used.
Тезис
Тесты и модели существуют рядом с программой.
Это создаёт разрыв между требованиями и кодом.
Если важное условие можно записать прямо в программе, его можно проверять автоматически при анализе или выполнении.
Так появляются предусловия, постусловия и инварианты.
Обзор
Предусловие описывает, что должно быть истинно до выполнения операции.
Постусловие задаёт результат, который должен быть получен после её выполнения.
Инвариант задаёт правило, которое должно сохраняться всегда.
Рассмотрим функцию изменения скорости двигателя.
Перед выполнением можно потребовать, чтобы новое значение находилось в допустимом диапазоне.
После выполнения можно проверить, что скорость действительно изменилась на заданное значение.
Инвариант может запрещать работу двигателя при аварийном состоянии системы.
Такие условия становятся частью описания программы.
Они уже не зависят только от отдельных тестов.
Решение
Основная идея состоит в том, чтобы отделить описание требуемого поведения от конкретных примеров.
Вместо теста со скоростью 50 можно записать правило, что скорость всегда должна быть меньше установленного предела.
Вместо проверки одного перевода денег можно задать условие, что баланс не может стать отрицательным.
После этого инструменты могут использовать эти правила разными способами.
Они могут проверяться во время работы программы.
Их можно анализировать до запуска.
На их основе можно строить дополнительные проверки.
При более строгом подходе можно пытаться доказать, что нарушение условия невозможно.
Достоинства
Главное преимущество состоит в явном описании требований.
Разработчику не нужно восстанавливать смысл программы только по её коду и тестам.
Условия находятся рядом с логикой, к которой относятся.
Это помогает обнаруживать ошибки раньше.
Некоторые нарушения можно найти ещё до запуска программы.
Контракты также упрощают проверку отдельных частей большой системы.
Можно отдельно определить, что функция принимает и что обязана гарантировать.
Недостатки
Контракты не появляются автоматически.
Их должен правильно сформулировать разработчик.
Если важное правило не записано, система его не проверит.
Слишком сложные условия могут быть трудны для анализа.
Особенно это заметно в программах с большим количеством состояний и связей между объектами.
Проверка во время выполнения тоже имеет ограничение.
Она обнаруживает нарушение только тогда, когда программа действительно попала в соответствующее состояние.
Само наличие инварианта ещё не означает, что он доказан для всех возможных путей выполнения.
Вывод
Контракты и инварианты делают важный шаг от внешнего тестирования к внутреннему описанию корректности программы.
Теперь требования становятся частью её структуры.
Но остаётся следующий вопрос.
Можно ли проверить такие условия не на отдельных запусках, а сразу для множества возможных путей выполнения программы?
Для этого применяются методы символьного выполнения и автоматического доказательства свойств.
Share
