The post has been translated automatically. Original language: Russian
The thesis
Usually, tests, requirements, and verification tools exist separately.
The developer writes the program. Then the tests. Another model is being created for strict verification.
Sekura JS offers a different approach: program properties are described next to its logic and become the basis for all types of verification.
Review
In Sekura JS, the module contains not only functions, but also conditions that must be preserved.
For example, the permissible speed and system status can be determined for an engine.
The speed change operation gets its own conditions. They describe when an action is allowed and what the state should be after it is performed.
This is how the program gets an explicit description of acceptable behavior.
These conditions can be used in different ways. At first, as regular checks. Then to build scripts automatically. Later, to analyze possible states and prove individual properties.
The main difference is that the source of the requirements remains the same.
Decision
A simple engine module may contain a rule:
module motor.sjs;
{
val.speed < 100;
}
function setSpeed {
value < 100;
val.speed' = value;
}The first part sets the state property.
The function determines the allowed value and the state change after the operation is performed.
From such a description, you can get the usual check: call a function with different values and make sure that the conditions are not violated.
The next level is to automatically search for the values and sequences of actions that lead to a violation.
A more rigorous level is to prove that when the operation conditions are met, the invariant is preserved for all acceptable values.
Thus, one record is gradually being used as a test, specification, and basis for proof.
Dignities
The developer does not have to independently maintain requirements, tests, and a formal model.
The properties are located next to the program and change with it.
Verification is built around the behavior of the system, not around the number of tests written.
It is especially important that strict verification can be introduced gradually. A regular module is first checked by tests. The critical properties then receive stronger confirmation.
This allows us to apply one approach both to ordinary application code and to systems where high confidence in correctness is required.
Disadvantages
This approach does not eliminate the main complexity of formal methods.
The properties must still be formulated correctly by a person.
An incomplete specification will give an incomplete guarantee.
Besides, automatic proof is not possible for every code. Complex calculations, external systems, and a large state space require constraints, additional models, or developer involvement.
Therefore, the presence of conditions in Sekura JS does not in itself mean proven correctness.
It is necessary to clearly distinguish between properties that have been tested, investigated by the analyzer, or actually proven.
Conclusion
Sekura JS considers testing and verification not as separate processes, but as different levels of work with the same program properties.
First, the property is checked using examples.
The system then searches for a violation automatically.
For the critical parts, you can proceed to proving that a violation is impossible under the given conditions.
The result should be not just the status of "tests passed", but a verifiable certificate.: which property is confirmed, in what way, and under what conditions.
It is this result that transforms testing from a set of examples into a consistent process of proving correctness.
Тезис
Обычно тесты, требования и средства верификации существуют отдельно.
Разработчик пишет программу. Затем тесты. Для строгой проверки создаётся ещё одна модель.
Sekura JS предлагает другой подход: свойства программы описываются рядом с её логикой и становятся основой для всех видов проверки.
Обзор
В Sekura JS модуль содержит не только функции, но и условия, которые должны сохраняться.
Например, для двигателя можно определить допустимую скорость и состояние системы.
Операция изменения скорости получает собственные условия. Они описывают, когда действие разрешено и каким должно стать состояние после его выполнения.
Так программа получает явное описание допустимого поведения.
Эти условия можно использовать по-разному. Сначала как обычные проверки. Затем для автоматического построения сценариев. Позже — для анализа возможных состояний и доказательства отдельных свойств.
Главное отличие состоит в том, что источник требований остаётся одним.
Решение
Простой модуль двигателя может содержать правило:
module motor.sjs;
{
val.speed < 100;
}
function setSpeed {
value < 100;
val.speed' = value;
}Первая часть задаёт свойство состояния.
Функция определяет допустимое значение и изменение состояния после выполнения операции.
Из такого описания можно получить обычную проверку: вызвать функцию с разными значениями и убедиться, что условия не нарушены.
Следующий уровень — автоматически искать значения и последовательности действий, которые приводят к нарушению.
Более строгий уровень — доказать, что при выполнении условий операции инвариант сохраняется для всех допустимых значений.
Таким образом одна запись постепенно используется как тест, спецификация и основание для доказательства.
Достоинства
Разработчику не приходится независимо поддерживать требования, тесты и формальную модель.
Свойства находятся рядом с программой и меняются вместе с ней.
Проверка строится вокруг поведения системы, а не вокруг количества написанных тестов.
Особенно важно, что строгую верификацию можно вводить постепенно. Обычный модуль сначала проверяется тестами. Критические свойства затем получают более сильное подтверждение.
Это позволяет применять один подход как к обычному прикладному коду, так и к системам, где требуется высокая уверенность в корректности.
Недостатки
Такой подход не устраняет главную сложность формальных методов.
Свойства всё равно должен правильно сформулировать человек.
Неполная спецификация даст неполную гарантию.
Кроме того, автоматическое доказательство возможно не для любого кода. Сложные вычисления, внешние системы и большое пространство состояний требуют ограничений, дополнительных моделей или участия разработчика.
Поэтому наличие условий в Sekura JS само по себе ещё не означает доказанную корректность.
Необходимо явно различать свойства, которые были проверены тестами, исследованы анализатором или действительно доказаны.
Вывод
Sekura JS рассматривает тестирование и верификацию не как отдельные процессы, а как разные уровни работы с одними и теми же свойствами программы.
Сначала свойство проверяется на примерах.
Затем система ищет нарушение автоматически.
Для критических частей можно перейти к доказательству того, что нарушение невозможно при заданных условиях.
Итогом должен стать не просто статус «тесты прошли», а проверяемое свидетельство: какое свойство подтверждено, каким способом и при каких условиях.
Именно такой результат превращает тестирование из набора примеров в последовательный процесс доказательства корректности.
Share
