97 этюдов для программистов. Опыт ведущих экспертов

Пиши код с умом Йехиль Кимхи

Попытки доказать корректность программного обеспечения вручную приводят к формальному доказательству, которое длиннее самого кода и содержит ошибки с большей вероятностью, чем сам код. Желательно применять автоматизированные средства, но это не всегда возможно. Ниже описывается срединный путь: полуформальное доказательство корректности.

Метод основан на разделении исследуемого кода на короткие фрагменты размером от одной строки, которая может содержать вызов функции, до блоков длиной не более 10 строк и обсуждении их корректности. Доказательство должно оказаться достаточно убедительным для вашего коллеги, играющего роль «адвоката дьявола».

Фрагменты следует выбирать таким образом, чтобы в конечной точке блока состояние программы (а именно счетчик адреса команд и значения всех «живых» объектов) удовлетворяло простому в описании свойству, а функциональность этого фрагмента (преобразование состояния) легко описывалась в виде одной независимой задачи. Соблюдение предложенных правил упрощает ведение доказательства. Такие свойства конечной точки фрагмента обобщают понятия пред-условий и пост-условий для функций, а также инвариантов для циклов и классов (в отношении экземпляров классов). Необходимо стремиться, чтобы фрагменты как можно меньше зависели друг от друга, что облегчает доказательство и очень пригодится, если предполагается изменять эти фрагменты.

Многие хорошо известные (хотя и, видимо, реже применяемые) и имеющие статус «качественных» практики написания кода также облегчают проведение доказательств. Таким образом, одно лишь намерение провести в будущем доказательство корректности своего кода способствует улучшению его стиля и структуры. Не стоит удивляться, что большинство подобных практик проверяется статическими анализаторами кода:

• Избегайте операторов goto, потому что они создают сильную зависимость между фрагментами, разнесенными в коде.

• Избегайте изменяемых глобальных переменных, потому что они делают зависимыми между собой все фрагменты, в которых используются.

• Область видимости каждой переменной должна быть наименьшей из возможных. Например, локальный объект можно объявить непосредственно перед первым использованием.

• Делайте объекты неизменяемыми (immutable), где это возможно.

• Улучшайте читаемость кода посредством пробелов — как горизонтальных, так и вертикальных. Например, выравнивайте отступы для родственных структур и разделяйте фрагменты кода пустыми строками.

• Пишите самодокументируемый код, выбирая содержательные (но достаточно короткие) имена для объектов, функций, типов и т. д.

• Если фрагмент оказывается вложенным, превратите его в функцию.

• Каждая функция должна решать единственную задачу и быть короткой. Ограничение длины функции 24 строками, введенное много лет назад, по-прежнему действует. Размер и разрешение экрана по сравнению с 60-ми годами прошлого века увеличились, но человеческие возможности восприятия остались прежними.

• У функции не должно быть много аргументов (хорошая практика — не более четырех). Это не ограничивает объем передаваемых функции данных: объединение родственных аргументов в одном объекте локализует инварианты объекта, что упрощает доказательство в плане проверки согласованности и состояний объектов.

• В общем случае каждая единица кода, начиная с фрагмента и заканчивая целой библиотекой, должна иметь ограниченный интерфейс. Сокращение потока информации упрощает доказательство. Это означает, что следует избегать методов, возвращающих внутреннее состояние (getters). Нужно не запрашивать у объекта информацию для обработки, а требовать, чтобы он выполнил работу с той информацией, которая у него уже есть. Иными словами, инкапсуляция — это ограниченные интерфейсы, и только они.

• Чтобы сохранить инварианты класса, следует избегать методов, присваивающих значения (setters). Они часто влекут нарушение инвариантов, определяющих состояния объекта.

Доказательство корректности кода, как и его обсуждение, позволит вам лучше в нем разобраться. Сообщайте о своих открытиях — это пойдет всем на пользу.