The post has been translated automatically. Original language: Russian
The thesis
Program requirements often live separately from the program itself. They are found in documentation, tasks, tests, or formal models.
Over time, these sources may diverge. The code changes, but the description remains the same. The tests don't always reflect the new rules either.
The executable specification suggests writing down important requirements so that development tools can use them directly.
Review
The usual specification explains to a person how the system should work.
The executable specification additionally has a precise form that the program can process.
It allows you to define acceptable values, conditions for performing operations, rules for changing the state, and restrictions that must be maintained.
For example, you can specify an acceptable speed range for the engine control system. For a speed change operation, you can determine under what conditions it is allowed and what the state should be after its completion.
This description can already be used for automatic verification.
The tool can create input data, control constraints during operation, or analyze possible execution options.
The specification becomes not only an explanation, but also a working part of the development process.
Decision
Let's imagine the operation of setting the engine speed.
There is a simple requirement: The speed must remain below the set limit.
The traditional approach requires writing this rule separately in the documentation, then writing several tests and, if necessary, creating a separate model for formal verification.
Another option is to write down the restriction itself in a form that is understandable to the development tools.
After that, the same rule can be applied at different stages.
During testing, the tool creates values and verifies the boundaries.
When executing the program, it may detect an attempt to enter an invalid state.
In the analysis, various ways of changing the speed can be investigated.
For a critical section, the same requirement can become the basis of a mathematical proof.
The point of the approach is not to replace all methods with one tool. More importantly, different verification methods rely on the same formulated requirement.
Dignities
This approach reduces the distance between the description of the system and its implementation.
The developer sees the limitations next to the logic they relate to.
The rule change is becoming more noticeable. It is less likely that the code already works in a new way, and the tests and documentation continue to describe the old behavior.
The executable specification also allows you to gradually strengthen the verification.
The usual tests are sufficient at an early stage. Then you can add an automatic search for boundary cases. Apply a more rigorous analysis for the most important parts.
However, it is not necessary to re-describe the meaning of the requirement for each tool.
Disadvantages
This method is not suitable for all requirements.
Some rules can be easily expressed by numerical limitation or condition condition. Others depend on the external environment, human actions, or complex processes.
There is also a risk of making the description too detailed. If the specification begins to repeat the entire implementation, its maintenance becomes a separate difficult task.
In addition, an accurate record of the requirement does not mean that the requirement itself was chosen correctly.
You can accurately check for an incorrect or incomplete rule.
Therefore, the quality of the result still depends on how well the developers understand the desired behavior of the system.
Conclusion
The executable specification links the requirements to the actual development.
It allows you to use a single formal description for several control methods: from routine tests to more rigorous analysis.
The next step is for the programming language to initially support such properties as part of the program.
In this case, testing and verification can be built not around separate sets of checks, but around explicitly defined rules of system behavior.
Тезис
Требования к программе часто живут отдельно от самой программы. Они находятся в документации, задачах, тестах или формальных моделях.
Со временем эти источники могут расходиться. Код меняется, а описание остаётся прежним. Тесты тоже не всегда отражают новые правила.
Исполняемая спецификация предлагает записывать важные требования так, чтобы инструменты разработки могли использовать их непосредственно.
Обзор
Обычная спецификация объясняет человеку, как должна работать система.
Исполняемая спецификация дополнительно имеет точную форму, которую может обработать программа.
В ней можно определить допустимые значения, условия выполнения операций, правила изменения состояния и ограничения, которые должны сохраняться.
Например, для системы управления двигателем можно указать допустимый диапазон скорости. Для операции изменения скорости можно определить, при каких условиях она разрешена и каким должно стать состояние после её завершения.
Такое описание уже можно применять при автоматической проверке.
Инструмент может создавать входные данные, контролировать ограничения во время работы или анализировать возможные варианты выполнения.
Спецификация становится не только пояснением, но и рабочей частью процесса разработки.
Решение
Представим операцию установки скорости двигателя.
Есть простое требование: скорость должна оставаться ниже установленного предела.
Традиционный подход требует отдельно записать это правило в документации, затем написать несколько тестов и при необходимости создать отдельную модель для формальной проверки.
Другой вариант — записать само ограничение в форме, понятной средствам разработки.
После этого одно и то же правило можно применять на разных этапах.
Во время тестирования инструмент создаёт значения и проверяет границы.
При выполнении программы он может обнаружить попытку перейти в недопустимое состояние.
При анализе можно исследовать различные пути изменения скорости.
Для критического участка то же требование может стать основой математического доказательства.
Смысл подхода не в том, чтобы заменить все методы одним инструментом. Важнее то, что разные способы проверки опираются на одинаково сформулированное требование.
Достоинства
Такой подход уменьшает расстояние между описанием системы и её реализацией.
Разработчик видит ограничения рядом с той логикой, к которой они относятся.
Изменение правила становится заметнее. Меньше вероятность, что код уже работает по-новому, а тесты и документация продолжают описывать старое поведение.
Исполняемая спецификация также позволяет постепенно усиливать проверку.
На раннем этапе достаточно обычных тестов. Затем можно добавить автоматический поиск граничных случаев. Для наиболее важных частей применить более строгий анализ.
При этом не обязательно заново описывать смысл требования для каждого инструмента.
Недостатки
Такой способ подходит не для всех требований.
Некоторые правила легко выразить числовым ограничением или условием состояния. Другие зависят от внешней среды, действий человека или сложных процессов.
Есть и риск сделать описание слишком подробным. Если спецификация начинает повторять всю реализацию, её сопровождение становится отдельной сложной задачей.
Кроме того, точная запись требования ещё не означает, что само требование выбрано правильно.
Можно безошибочно проверить неверное или неполное правило.
Поэтому качество результата по-прежнему зависит от того, насколько хорошо разработчики понимают нужное поведение системы.
Вывод
Исполняемая спецификация связывает требования с реальной разработкой.
Она позволяет использовать одно формальное описание для нескольких способов контроля: от обычных тестов до более строгого анализа.
Следующий шаг состоит в том, чтобы язык программирования изначально поддерживал такие свойства как часть программы.
Тогда тестирование и верификация могут строиться не вокруг отдельных наборов проверок, а вокруг явно заданных правил поведения системы.
Share
