The post has been translated automatically. Original language: Russian
The thesis
The tests check the program from the outside. But some of the requirements can be fixed right next to the code.
To do this, use preconditions, postconditions, and invariants.
They describe what should be true before the operation is performed, after it, and throughout the entire operation of the system.
Review
The precondition sets the requirements for the input state.
For example, the transfer amount must be positive and the account must be active.
The postcondition describes the state after the operation is performed.
After the transfer, the money must be debited from one account and credited to another.
The invariant defines a rule that must always be maintained.
For example, the balance should not become negative or the engine speed should not exceed the permissible value.
Such conditions make the requirements explicit.
They cease to exist only in the documentation or in the developer's head.
Decision
Consider the operation of changing the engine speed.
You can write several tests for values 20, 50 and 90.
But you can also set a condition: the new value must be less than the set limit.
Additionally, an invariant can be defined: as long as the system is in operation, the speed always remains within the acceptable range.
Now it's not just the specific function call that is being checked.
The operation's compliance with the general rules of the system is checked.
Such conditions can be monitored during program execution, analyzed before launch, or used as a basis for stricter verification.
Dignities
The main advantage is that the requirements are right next to the program.
They are easier to maintain along with code changes.
Contracts are good at detecting boundary violations and incorrect states.
They also improve the understanding of the program. It is easier for the developer to see what conditions are required for the operation and what result it should guarantee.
Invariants are especially useful for systems with complex state.
They allow you to describe not individual scenarios, but properties that should always be preserved.
Disadvantages
The contract does not appear automatically.
It must be formulated correctly by the developer.
If an important requirement is not described, the system will not know about it.
There is another problem. Checking the condition during execution detects a violation only when the program has reached the appropriate state.
Again, this does not guarantee that all possible paths have been explored.
More rigorous verification requires additional analysis methods.
In addition, too many conditions can complicate the code if the language and tools do not support this development model well.
Conclusion
Contracts and invariants take an important step from external testing to explicitly describing the correctness of the program.
Now the requirements become part of the implementation itself.
But the question remains: is it possible to check these properties not only at runtime, but for multiple possible program paths at once?
Symbolic execution and other analysis methods are used for this purpose.
Тезис
Тесты проверяют программу снаружи. Но часть требований можно зафиксировать прямо рядом с кодом.
Для этого используют предусловия, постусловия и инварианты.
Они описывают, что должно быть истинно до выполнения операции, после неё и на всём протяжении работы системы.
Обзор
Предусловие задаёт требования к входному состоянию.
Например, сумма перевода должна быть положительной, а счёт должен быть активен.
Постусловие описывает состояние после выполнения операции.
После перевода деньги должны быть списаны с одного счёта и зачислены на другой.
Инвариант задаёт правило, которое должно сохраняться всегда.
Например, баланс не должен становиться отрицательным или скорость двигателя не должна превышать допустимое значение.
Такие условия делают требования явными.
Они перестают существовать только в документации или в голове разработчика.
Решение
Рассмотрим операцию изменения скорости двигателя.
Можно написать несколько тестов для значений 20, 50 и 90.
Но можно также задать условие: новое значение должно быть меньше установленного предела.
Дополнительно можно определить инвариант: пока система находится в рабочем состоянии, скорость всегда остаётся в допустимом диапазоне.
Теперь проверяется не только конкретный вызов функции.
Проверяется соответствие операции общим правилам системы.
Такие условия можно контролировать во время выполнения программы, анализировать до запуска или использовать как основу для более строгой верификации.
Достоинства
Главное преимущество заключается в том, что требования находятся рядом с программой.
Их проще поддерживать вместе с изменениями кода.
Контракты хорошо обнаруживают нарушения границ и неправильные состояния.
Они также улучшают понимание программы. Разработчику проще увидеть, какие условия обязательны для выполнения операции и какой результат она должна гарантировать.
Инварианты особенно полезны для систем со сложным состоянием.
Они позволяют описывать не отдельные сценарии, а свойства, которые должны сохраняться всегда.
Недостатки
Контракт не появляется автоматически.
Его должен правильно сформулировать разработчик.
Если важное требование не описано, система о нём не узнает.
Есть и другая проблема. Проверка условия во время выполнения обнаруживает нарушение только тогда, когда программа дошла до соответствующего состояния.
Это снова не гарантирует, что были исследованы все возможные пути.
Более строгая проверка требует дополнительных методов анализа.
Кроме того, слишком большое количество условий может усложнить код, если язык и инструменты плохо поддерживают такую модель разработки.
Вывод
Контракты и инварианты делают важный шаг от внешнего тестирования к явному описанию корректности программы.
Теперь требования становятся частью самой реализации.
Но остаётся вопрос: можно ли проверить эти свойства не только во время выполнения, а сразу для множества возможных путей программы?
Для этого применяют символическое выполнение и другие методы анализа.
Share
