The post has been translated automatically. Original language: Russian
Programming and formal methods are usually taught as two different disciplines.
First, a person learns how to write programs, debug them, and test them. And only much later he comes across the question: how to formulate exactly what a program should do.
We decided to try a different approach.
In the training materials on Sekura JS and SJV, the program is immediately viewed from two sides.
On the one hand, there is an implementation: variables, functions, conditions, memory, and calculations.
On the other hand, there are requirements for its behavior: what states are acceptable, under what conditions the transition can be performed, and what the state should be after the function is completed.
For example, a student writes a function that modifies a counter. A normal assignment would end after several tests gave the correct result.
In our scheme, this is only half the work.
The next step is to formulate a function property in SJV, check it, and then intentionally modify the program so as to obtain a counterexample.
After that, you need to understand the cause of the violation and fix the implementation.
It turns out to be a different learning cycle:
write — formulate a requirement — check — see a violation — fix it.
This is how a person learns not only to achieve the right result, but also to answer the question exactly what "right" means in general.
This is especially important for system programming. An error can occur only with a rare state of memory, an unusual input value, or a specific sequence of actions.
Several successful tests do not exclude this.
Therefore, we consider SJV not as a separate complex discipline after programming, but as a natural second language of the developer: in one language it describes what to do, in the other — what should be true.
Обычно программированию и формальным методам учат как двум разным дисциплинам.
Сначала человек учится писать программы, отлаживать их и проверять тестами. И только намного позже сталкивается с вопросом: как строго сформулировать, что именно программа должна делать.
Мы решили попробовать другой подход.
В учебных материалах по Sekura JS и SJV программа сразу рассматривается с двух сторон.
С одной стороны, есть реализация: переменные, функции, условия, память и вычисления.
С другой — требования к её поведению: какие состояния допустимы, при каких условиях можно выполнять переход и каким должно быть состояние после завершения функции.
Например, ученик пишет функцию, которая изменяет счётчик. Обычное задание закончилось бы после того, как несколько тестов дали правильный результат.
В нашей схеме это только половина работы.
Следующий шаг — сформулировать свойство функции в SJV, проверить его и затем намеренно изменить программу так, чтобы получить контрпример.
После этого нужно понять причину нарушения и исправить реализацию.
Получается другой цикл обучения:
написать — сформулировать требование — проверить — увидеть нарушение — исправить.
Так человек учится не только добиваться правильного результата, но и точно отвечать на вопрос, что вообще означает «правильно».
Для системного программирования это особенно важно. Ошибка может проявляться только при редком состоянии памяти, необычном входном значении или определённой последовательности действий.
Несколько удачных тестов этого не исключают.
Поэтому мы рассматриваем SJV не как отдельную сложную дисциплину после программирования, а как естественный второй язык разработчика: на одном языке он описывает что делать, на другом — что должно быть истинно.
Share
