The post has been translated automatically. Original language: Russian
A musician can play dozens of correct notes, then make a mistake on just one, and the listener will notice it almost instantly. He does not need to calculate the frequency of a sound, determine the scale step, or compare a note with a table of acceptable values.
A person just hears that something is wrong. This capability does not exist by default for the program.
The error exists only with respect to the rule
The note itself is not right or wrong. It becomes like this only within a certain context: tonality, chord, rhythm, the previous phrase and the expected continuation.
The same thing happens in programming. The number 17, the line of text, or the case value alone do not contain an error. The error appears when the value violates some condition of the system.
Therefore, the first step to verifying a program is not to write validating code, but to determine what is generally considered correct.
This is the specification.
A person keeps the rules implicitly
An experienced musician rarely formulates all the rules he uses. He doesn't think before each note: "now the first part sounds like a chord, so these steps are allowed."
Most of the verification is done automatically. The hearing compares the result with the accumulated internal model and almost immediately notices a significant deviation.
The program must be given such a model explicitly. For example:
- The note must belong to a given set.;
- the phrase should fit into four bars.;
- The duration of each note should be acceptable.;
- certain beat positions must correspond to a given rhythm.;
- the sequence must not exceed the specified range.
After that, the program is already able to distinguish an acceptable result from an unacceptable one.
Checking the example is not enough
The easiest way to test a program is to run it several times and see the result.
If the generator has played ten phrases and they all sound normal, this does not mean that the eleventh one will not violate the rules. We've checked a few examples, but we haven't proven anything about all the possible outcomes.
This is how normal testing works. We select known cases, execute the program, and compare the result with the expected one.
This is useful, but there is an obvious limit to this approach: the space of options may be too large to test them all.
In a music generator, even a small set of notes and durations quickly creates hundreds of thousands of possible phrases. In a real program, the number of states can be incomparably higher.
Formal verification asks a different question
The test answers the question: "Does the program work correctly in these selected cases?"
Formal verification poses a stronger question: "Is it possible to prove that a given property holds for all valid cases?"
For example, we may require that the oscillator never produce a note outside of a given pentatonic. Instead of checking thousands of randomly created phrases, you can examine the algorithm itself and prove that it can't get any other result.
The property becomes part of the program design.
Instead of:
generate → listen → find an error
we strive to get:
set a rule → build a system → prove compliance with the rule.
But music immediately shows the limits of formality.
Let's say the program provably uses only the notes of a given pentatonic. Does this mean that all her phrases will sound good?
No.
You can play a completely meaningless sequence without violating any such rule. Formal verification guarantees only those properties that we were able to formulate.
This is fundamentally important not only for music. In the program, it is possible to prove the absence of going beyond the boundaries of the array, the correctness of the state change, or the implementation of the protocol, but this does not mean that the program itself solves the task a person needs.
The proof always refers to a specific specification.
If the specification is bad, the program may flawlessly meet the wrong requirements.
Falsehood can also be different
Even in music, the word "fake" is ambiguous. Sometimes it's just a note outside the selected scale. Such a case is relatively easy to describe.
But a musician can intentionally use a note outside the main scale, slightly change its pitch, or create tension before resolution. Technically, it looks like a violation of a simple rule, but musically it may turn out to be exactly what you need.
This means that a good rule system must distinguish between a gross error and an acceptable deviation.
The same thing happens in programming. A specification that is too strict prohibits useful behavior, and a specification that is too weak allows errors to occur.
Therefore, formalization is not a mechanical record of obvious limitations. This is a search for essential properties of the system.
Invariants
One of the most important concepts here is an invariant, a property that must be preserved regardless of what happens inside the system.
For a music program, such an invariant can be a condition: the total duration of events in each bar is always equal to the length of the bar.
For the banking system, the amount of money should not change without a corresponding operation. For memory management, the same area should not belong to two independent owners at the same time, if the architecture does not allow this.
Specific systems vary, but the principle remains the same: we are looking for properties whose violation means that the system has exceeded acceptable limits.
People often recognize such violations intuitively. Formal verification requires expressing this intuition in the form of a precise statement.
From hearing to proof
The music shows well why verification is needed at all. As long as everything sounds right, we hardly think about the rules. One wrong note immediately makes them noticeable.
In programming, an error often does not give such an obvious signal. It can manifest itself after a million operations, only with a rare combination of states, or after the program has been run in a real system.
Therefore, the machine does not have enough ability to create a result. We also need a way to define the boundaries of an acceptable result.
A person does this by hearing, experience, and intuition. In a mathematically described program, specifications, invariants, and formal verification play the same engineering role.
This is where programming ceases to be just the art of getting a machine to do something. The next level is to be able to formulate exactly what it should do and prove that the specified properties will not be violated.
Музыкант может сыграть десятки правильных нот, затем ошибиться всего на одной — и слушатель заметит это почти мгновенно. Ему не нужно вычислять частоту звука, определять ступень гаммы или сравнивать ноту с таблицей допустимых значений.
Человек просто слышит: что-то не так. Для программы такой способности по умолчанию не существует.
Ошибка существует только относительно правила
Сама по себе нота не бывает правильной или неправильной. Она становится такой только внутри некоторого контекста: тональности, аккорда, ритма, предыдущей фразы и ожидаемого продолжения.
То же происходит в программировании. Число 17, строка текста или значение регистра сами по себе не содержат ошибки. Ошибка появляется, когда значение нарушает некоторое условие системы.
Поэтому первый шаг к проверке программы — не написать проверяющий код, а определить, что вообще считается правильным.
Это и есть спецификация.
Человек хранит правила неявно
Опытный музыкант редко формулирует все правила, которыми пользуется. Он не думает перед каждой нотой: «сейчас первая доля, звучит такой аккорд, значит разрешены такие ступени».
Большая часть проверки происходит автоматически. Слух сравнивает результат с накопленной внутренней моделью и почти сразу замечает существенное отклонение.
Программе такой модели нужно дать явно. Например:
- нота должна принадлежать заданному набору;
- фраза должна укладываться в четыре такта;
- длительность каждой ноты должна быть допустимой;
- определённые позиции такта должны соответствовать заданному ритму;
- последовательность не должна выходить за установленный диапазон.
После этого программа уже способна отличать допустимый результат от недопустимого.
Проверить пример недостаточно
Самый простой способ проверки программы — запустить её несколько раз и посмотреть на результат.
Если генератор сыграл десять фраз и все они звучат нормально, это ещё не означает, что одиннадцатая не нарушит правила. Мы проверили несколько примеров, но ничего не доказали обо всех возможных результатах.
Так устроено обычное тестирование. Мы выбираем известные случаи, выполняем программу и сравниваем полученный результат с ожидаемым.
Это полезно, но у такого подхода есть очевидная граница: пространство вариантов может быть слишком большим, чтобы проверить их все.
В музыкальном генераторе даже небольшой набор нот и длительностей быстро создаёт сотни тысяч возможных фраз. В реальной программе число состояний может быть несравнимо больше.
Формальная верификация задаёт другой вопрос
Тест отвечает на вопрос: «Работает ли программа правильно в этих выбранных случаях?»
Формальная верификация ставит более сильный вопрос: «Можно ли доказать, что заданное свойство выполняется для всех допустимых случаев?»
Например, мы можем потребовать, чтобы генератор никогда не выдавал ноту вне заданной пентатоники. Вместо проверки тысячи случайно созданных фраз можно исследовать сам алгоритм и доказать, что другого результата он получить не способен.
Свойство становится частью конструкции программы.
Вместо:
сгенерировать → послушать → найти ошибку
мы стремимся получить:
задать правило → построить систему → доказать соблюдение правила.
Но музыка сразу показывает границу формальности
Допустим, программа доказуемо использует только ноты заданной пентатоники. Значит ли это, что все её фразы будут хорошо звучать?
Нет.
Можно сыграть совершенно бессмысленную последовательность, не нарушив ни одного такого правила. Формальная проверка гарантирует только те свойства, которые мы смогли сформулировать.
Это принципиально важно не только для музыки. В программе можно доказать отсутствие выхода за границы массива, корректность изменения состояния или выполнение протокола, но из этого не следует, что сама программа решает нужную человеку задачу.
Доказательство всегда относится к конкретной спецификации.
Если спецификация плохая, программа может безупречно соответствовать неправильным требованиям.
Фальшь тоже бывает разной
Даже в музыке слово «фальшь» неоднозначно. Иногда это просто нота вне выбранного звукоряда. Такой случай описать сравнительно легко.
Но музыкант может намеренно использовать ноту вне основной гаммы, слегка изменить её высоту или создать напряжение перед разрешением. Формально это выглядит как нарушение простого правила, а музыкально может оказаться именно тем, что нужно.
Значит, хорошая система правил должна различать грубую ошибку и допустимое отклонение.
В программировании происходит то же самое. Слишком жёсткая спецификация запрещает полезное поведение, слишком слабая пропускает ошибки.
Поэтому формализация — это не механическая запись очевидных ограничений. Это поиск существенных свойств системы.
Инварианты
Одним из важнейших понятий здесь является инвариант — свойство, которое должно сохраняться независимо от того, что происходит внутри системы.
Для музыкальной программы таким инвариантом может быть условие: суммарная длительность событий в каждом такте всегда равна длине такта.
Для банковской системы — сумма денег не должна изменяться без соответствующей операции. Для управления памятью — один и тот же участок не должен одновременно принадлежать двум независимым владельцам, если архитектура этого не допускает.
Конкретные системы различаются, но принцип остаётся тем же: мы ищем свойства, нарушение которых означает, что система вышла за допустимые границы.
Человек часто распознаёт подобные нарушения интуитивно. Формальная верификация требует выразить эту интуицию в виде точного утверждения.
От слуха к доказательству
Музыка хорошо показывает, зачем вообще нужна проверка. Пока всё звучит правильно, мы почти не думаем о правилах. Одна неправильная нота сразу делает их заметными.
В программировании ошибка часто не даёт такого очевидного сигнала. Она может проявиться через миллион операций, только при редком сочетании состояний или уже после того, как программа была запущена в реальной системе.
Поэтому машине недостаточно способности создавать результат. Нужен ещё способ определять границы допустимого результата.
Человек делает это слухом, опытом и интуицией. В математически описанной программе ту же инженерную роль выполняют спецификации, инварианты и формальная верификация.
Именно здесь программирование перестаёт быть только искусством заставить машину что-то сделать. Следующий уровень — уметь точно сформулировать, что она должна делать, и доказать, что заданные свойства не будут нарушены.
Share
