• Монотонность

• Предусловия и постусловия

• Инварианты

• Изоляция

• Индукция

• Удобство доказательства как метрика качества кода

• Как развивать этот навык

В этой статье я коротко опишу один приём, который помогает мне писать код быстрее и с меньшим числом ошибок. Я говорю «приём», но по факту это просто практика, которой я начал следовать с опытом, сам того не замечая.

Когда вы работаете над чем-то сложным, формируйте в уме некое подтверждение, что ваш код будет делать именно то, что вам нужно. Звучит вроде просто, но на деле всё оказывается сложнее. Чтобы начать делать это «на лету», не прерывая рабочий поток, потребуется упорная практика. Зато, когда вы освоите эту технику, то удивитесь, насколько чаще ваш код будет полноценно работать с первой или второй попытки. Невероятно впечатляет.

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

Монотонность

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

Вам наверняка известны монотонные функции из математики. Если говорить простым языком, то это функции, которые «не имеют обратного хода» — то есть возрастающая монотонная функция может только увеличиваться или оставаться прежней, а убывающая — только уменьшаться или также оставаться прежней (их ещё называют невозрастающими и неубывающими).

Принцип монотонного кода несколько туманнее, но он отражает ту же идею процесса, который может развиваться только в одном направлении. Хорошим примером такого процесса является создание контрольных точек (checkpointing). Если у вас есть скрипт, выполняющий несколько последовательных задач, то вы можете сохранять на диске его состояние, которое будет отражать число выполненных из них на текущий момент. Тогда в случае внезапного сбоя этого скрипта он сможет проверить сохранённое состояние, выяснить, где произошла остановка, и продолжить выполнение со следующего шага.

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

Ведение подобного журнала активности представляет простую идею, которая зачастую возникает в удивительных контекстах, таких как файловые системы с ведением журнала и упреждающая журнализация в базах данных. Ещё один, уже более продвинутый пример с базой данных — это LSM-дерево. Такие деревья используются в некоторых базах данных для хранения строк в памяти и на диске. Основную часть времени они работают исключительно аддитивно. Проще говоря — в LSM‑дереве ведётся журнал всех добавлений, удалений и обновлений, а также происходит сканирование созданного журнала для воссоздания правильного значения строки при её считывании. При этом с целью экономии памяти результаты устаревших операций периодически удаляются в процессе «уплотнения данных» (compaction). Пространство, занимаемое LSM-деревом, только растёт (за исключением периодов уплотнения, когда оно только уменьшается).

Можно сравнить это с B-деревом — более традиционной структурой базы данных, в которой удаление и обновление строк происходит по месту. В таких структурах обычно приходится проделывать намного больше работы: восстанавливать освобождённое после удаления пространство; реструктурировать содержимое, чтобы было место для добавления новых строк; обеспечивать достаточный объём буфера и так далее. Если интересно, почитайте на тему B-деревьев и LSM-деревьев, чтобы понять, какая из этих структур воспринимается более интуитивной.

Кроме того, отслеживание монотонности позволяет исключить широкий спектр возможных исходов. Ещё одной схожей концепцией является иммутабельность — когда вы создаёте иммутабельный объект, который не может быть изменён. Присвоить такому объекту значение можно только раз — в момент его создания. И отменить это присваивание нельзя. Такой механизм позволяет сразу отмести все сценарии, в которых объект может непредвиденно измениться.

Предусловия и постусловия

Предусловия и постусловия позволяют указывать ограничения поведения для функции. Предусловия функции — это те, которые должны быть истинны до её выполнения. Эти условия могут относиться ко входным данным либо более общим аспектам состояния или среды работы программы. Постусловия — это те, которые должны выполняться после возврата функцией результата. Как и в случае с предусловиями, они могут касаться чего угодно. Если предусловия функции до её запуска выполняются, а постусловия после её завершения нет, значит, есть ошибка в реализации этой функции — как минимум в плане установленных ограничений.

Эти элементарные и очевидные принципы не являются техниками для подтверждения работоспособности, но даже их простое учитывание поможет вам в построении цепочки рассуждений.

Иногда может оказаться так, что у вашей функции нет чётко прописанных предусловий и постусловий, и это тоже полезно знать!

Определение постусловий, в частности, является удачным способом выработки идей для модульных тестов. Это также поможет добавить защитные утверждения о выполнении предусловий и постусловий, чтобы в противном случае программа аварийно завершалась. Так будет проще рассуждать о том, что ваш код сделает, если сбоя не произойдёт. Это решение может показаться бессмысленным компромиссом, но обычно безопаснее будет завершить код аварийно, нежели позволить ему продолжить выполняться непредсказуемым образом.

Инварианты

Инварианты фрагментов кода — это компоненты, которые всегда должны оставаться истинными: до, во время и после выполнения программы. Как и в случае с предварительными и постусловиями, инвариант может подразумевать что угодно.

Иногда полезно оценивать согласованность выполнения через призму инвариантов. В таких ситуациях инвариант подразумевает, что «эта структура данных согласована/валидна», и вам нужно доказать себе, что код сохраняет этот инвариант везде и при любых условиях. Простым решением будет поделить код на небольшие «шаги» и убедиться, что на каждом таком шаге инвариант сохраняется. Это даст вам уверенность, что инвариант останется неизменен вне зависимости от того, какие шаги будут выполнены и в каком порядке.

Одним из старейших и самых известных примеров инварианта является балансовое уравнение, лежащее в основе двойной системы бухгалтерского учёта. Если коротко, то балансовое уравнение гласит, что общий объём дебета в учётной книге компании должен равняться общему объёму кредита. Легко доказать, что при правильном выполнении двойная система учёта сохранит этот инвариант. В отношении каждой транзакции все увеличения (или уменьшения) объёма кредита должны равняться всем увеличениям (или уменьшениям) дебета. Очевидно, если дебет и кредит находятся в балансе до проведения транзакции, они будут в балансе и после неё. Таким образом этот инвариант всегда сохраняется.

Ещё один способ сохранения определённых видов инвариантов подразумевает использование слушателя или метода жизненного цикла для отслеживания истинности инварианта в критических точках. Эта техника часто используется, когда нужно сохранить синхронность между несколькими элементами состояния — например, в C++ с помощью конструкторов и деструкторов обеспечивают, чтобы необходимая объекту память выделялась только на время его жизни. Нечто аналогичное делает useEffect в отношении компонентов React.

Поскольку инварианты должны сохраняться в любом возможном сценарии, ими проще оперировать в уме при внесении таких изменений, которые создают относительно мало новых путей выполнения.

Изоляция

Я давно убеждён, что значительная часть «искусства» создания ПО связана с изменением или расширением существующей системы без нарушения стабильности её элементов. При внесении изменений в кодовую базу иногда очень полезно уметь доказать, что поведение, которое вы не планировали менять, действительно осталось неизменным.

Есть одна техника, которую применяю в таких случаях лично я. Не уверен, как она точно называется, и лучше буду называть её не техникой, а просто моделью мышления. Смысл примерно такой: у каждого изменения есть «радиус действия», то есть изменение в одной части кода может привести к необходимости изменения другой для сохранения согласованности/корректности всей системы. Это второе изменение может потребовать третьего, уже в другой части кода. И так далее. Чтобы утвердить, на какое поведение изменение сможет/не сможет повлиять, нужно определить структурные «заграждения», которые не позволят изменению оказать влияние за пределами указанной точки. В некотором роде это похоже на инкапсуляцию.

Это весьма абстрактная идея, так что опишу конкретный пример с Nerve.

Nerve — это механизм запросов, который позволяет делать запрос ко множеству источников данных так, будто они являются одним огромным API. Пайплайн запросов Nerve состоит из планировщика запросов, вычисляющего конкретный пошаговый план выполнения запроса, и исполнителя запросов, реализующего этот план. Сам запрос может содержать вещественные (material) поля и виртуальные (virtual). Виртуальные поля, по сути, являются производными — то есть вещественное поле извлекается непосредственно из исходного API, а виртуальное — вычисляется в среде выполнения на основе других виртуальных или вещественных полей.

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

Одно из простых решений — это изменить планировщика и исполнителя запросов таким образом, чтобы они имели представление о вещественном поле, которое подтягивается в виде зависимости, а не указывается в запросе. Такие «вспомогательные поля» должны находиться под рукой, чтобы их можно было использовать для вычисления виртуальных полей, но включать их в итоговые результаты запросов не нужно. Но в этом дизайне нужно учесть и ряд других нюансов. Например, нам наверняка потребуются способы для подтягивания таких зависимостей в тех же запросах, которые мы делаем при подтягивании обычных вещественных полей. И так далее…

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

В этом случае мы уже не вносим никакие новые представления об особых типах полей. Вместо этого на этапе планировки запроса мы просто вычисляем зависимости каждого виртуального поля и добавляем их в этот запрос, после чего передаём их все исполнителю. Исполнитель понятия не имеет, что переданный ему запрос не является запросом пользователя. Он просто выполняет его как обычно, сначала подтягивая все вещественные поля и затем вычисляя все необходимые виртуальные (и ему никогда не требуется подтягивать зависимости виртуальных полей, так как они уже под рукой).

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

Основное преимущество этого решения в том, что такое изменение затрагивает лишь два небольших слоя пайплайна запроса — его начало и конец — сердцевина же при этом (сама суть механизма обработки запросов) остаётся неизменной. В частности, граница между планировщиком и исполнителем запросов выступает тем самым «заграждением», которое не позволяет изменению оказывать влияние вовне. В результате уже несложно доказать, что наши изменения не приведут к регрессии при выполнении запросов, которым не нужно подтягивать никакие зависимости (поскольку в таком случае мы выполняем только тот код, который не менялся).

Иногда подобный подход оказывается подходящим, иногда нет. Но при всех прочих равных он просто уменьшает когнитивную нагрузку за счёт того, что вы меняете минимум кода.

(Вы могли встречать обсуждение этой идеи в контексте принципа открытости/закрытости. Этот принцип включает в себя множество особенностей ООП, которые в нашем случае неактуальны. Актуальной же остаётся лежащая в его основе концепция: «Когда требования к ПО меняются, вы расширяете поведение [своей] программы через добавление нового кода, а не изменение старого, который работает»).

Индукция

Множество интересных программ построены с использованием рекурсивных функций или рекурсивных структур данных (и в некотором теоретическом смысле рекурсия является основой самих вычислений). В зависимости от области работы вы можете встречать рекурсию повсеместно или только изредка, но в любом случае понимание её принципов значительно облегчит вам жизнь.

Рекурсивная структура данных — это такая, которая содержит копию самой себя (не обязательно точную копию, но экземпляр такого же «типа»). В свою очередь, эта копия также может содержать свою копию, и так далее. Подобный рекурсивный процесс может продолжаться бесконечно или завершаться при достижении «базового случая». В качестве примера рекурсии можно назвать фрактал.

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

Списки тоже можно формировать рекурсивно, хотя обычно так их себе не представляют. Каждый рекурсивный список состоит из головы, то есть «первого» или крайнего левого элемента, а также хвоста, содержащего оставшиеся элементы списка. Хвост сам по себе тоже является списком, а базовым случаем здесь является пустой список (аналогичным образом можно рассматривать как рекурсию и натуральные числа — каждое очередное натуральное число получается прибавлением 1 к текущему натуральному числу, кроме 0, который является базовым случаем).

Рекурсивная функция — это функция, которая вызывает саму себя. Такие функции обычно используются для обработки рекурсивных структур данных, поскольку могут вызывать себя в отношении их рекурсивных копий (например, функция для обработки дерева может вызывать себя для всех его потомков).

Также существует доказательная техника, специально созданная для работы с рекурсивными структурами — индукция. Классическая версия индукции используется для доказательства, что некое утверждение P(n) является истинным для любого натурального числа n. Доказывается это в два шага:

• сначала доказывается верность P(0),

• затем доказывается, что P(n) подразумевает P(n+1).

Второй этап называется индуктивным, и предположение, что P(n) верно называется индуктивной гипотезой. Именно в этом этапе и кроется основной потенциал индукции — P зачастую намного проще доказать, когда есть индуктивная гипотеза. Суть индукции заключается в написании «инкрементальной» версии доказательства вместо попытки предоставить доказательство для всех чисел сразу.

Когда вы пишете рекурсивную функцию, попробуйте доказать себе её корректность с помощью индукции. Ниже я опишу простой пример, адаптированный из кодовой базы Nerve.

Не углубляясь в детали — в Nerve есть конкретный случай, когда нам нужно показать абстрактное синтаксическое дерево (AST) пользователю. AST имеет довольно сложную и громоздкую структуру, поэтому сначала нужно удалить узлы, которые пользователя наверняка не интересуют. Когда мы удаляем узел, его родитель должен «унаследовать всех его потомков» (в техническом смысле нам нужно произвести операцию стягивания ребра между удалённым узлом и его родителем).

Примечание по терминологии: с технической стороны «стягивание» — это термин, который применяется только к рёбрам, но я позволю себе вольность и буду также использовать его в отношении узлов и деревьев. Когда я говорю «стянуть узел», то имею в виду «стянуть ребро между узлом и его родителем».

Вот функция, которую мы используем в Nerve (не точная её копия, но суть сохранена):

function simplifyTree(root: Node): Node {
  let newChildren = [] as Array<Node>;

  for (const child of root.children) {
    const simplifiedChild = simplifyGraph(child);

    if (shouldContract(simplifiedChild)) {
      for (const grandChild of simplifiedChild.children) {
        newChildren.push(grandChild);    
      }
    } else {
      newChildren.push(simplifiedChild);
    }
  }

  root.children = newChildren;
  
  return root;
}

Нам нужно, чтобы функция максимально упрощала переданное AST. Иными словами, у нас здесь следующее постусловие: граф, возвращаемый simplifyGraph, нужно «полностью стянуть» — то есть в результате в нём не должно остаться доступных для стягивания рёбер.

Вот индуктивное доказательство того, что это условие выполняется:

• Начнём с базового случая. По определению корневой узел стянуть нельзя, так как у него нет родителя. Значит, базовый случай — один листовой узел — уже удовлетворяет постусловию. Если мы передадим simplifyGraph лист, он просто вернёт его как есть, значит, можно сделать вывод, что в базовом случае он работает корректно.

• А теперь сама магия — индуктивный шаг. Нам нужно доказать, что, если simplifyGraph верна для каждого поддерева дерева Т, то она верна и для Т. Очень важно, что теперь у нас есть доступ к индуктивной гипотезе, то есть мы можем предположить, что каждое поддерево (каждое дерево, уходящее корнем в simplifiedChild) далее стянуть невозможно.

  Единственное потенциальное стягивание, которое нужно учесть, происходит между simplifiedChild и root. Если мы определим, что simplifiedChild нужно стянуть, мы удалим его и привяжем всех его потомков к root. Проделав это для каждого simplifiedChild, мы будем уверены, что дерево, растущее от root, больше стянуть нельзя. Если бы это было возможно, то мы могли бы стянуть как минимум одно поддерево, что противоречит индуктивной гипотезе. Ч. Т. Д.

Научившись вести такое индуктивное рассуждение на интуитивном уровне, вы сможете намного эффективнее работать с рекурсивными функциями.

(При желании попробуйте убедить себя, что simplifyGraph работает корректно для любого возможного ввода, рассуждая холистически без использования индукции. Какой подход покажется вам более естественным?)

Удобство доказательства как метрика качества

Если коротко, то всё это время я говорил о том, что: «Вам следует выстраивать в уме небольшие доказательства относительно работы вашего кода». Но у этой статьи есть и скрытый посыл, а именно: «Вам следует стараться писать код так, чтобы для его работы было легко составлять доказательства».

Аналогичный скрытый посыл есть и у каждого раздела статьи:

• Стремитесь использовать монотонность и иммутабельность. → Пишите монотонный код с использованием иммутабельных структур данных.

• Отслеживайте предварительные и постусловия. → Начинайте с продумывания предусловий и постусловий, после чего выстраивайте код вокруг них. Структурируйте программу так, чтобы эти условия можно было легко осмыслить и проверить.

• Вы можете доказать, что функция сохраняет инвариант, доказав это в отношении каждой единицы её работы. → Разделяйте код на минимальные возможные единицы, которые могут сохранять инвариант.

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

• Используйте индукцию, чтобы доказывать правильность работы рекурсивных функций пошагово, а не разом. Предположите, что индуктивная гипотеза уже доказана, и отталкивайтесь от этого. → Пишите рекурсивные функции пошагово. Предположите, что рекурсивный вызов уже реализован, и напишите часть функции, которая создаёт случай n+1 из случая n. Затем отдельно реализуйте базовый случай.

Суть в том, чтобы оценивать качество кода было так же легко, как и понимать его. Если вы легко сможете доказать себе, что код корректен, это будет говорить о его грамотной структуре. И, напротив, если это вызывает сложности и раздражение, следует подчистить или реструктурировать код, чтобы сделать его проще.

Как показывают перечисленные выше идеи, можно (как минимум субъективно) спроектировать код с акцентом на максимальное удобство его доказательства.

Естественно, удобство доказательства — это не единственное важное измерение качества ПО (код также должен быть корректным, быстрым и удобным в использовании). Но я думаю, что оно очень важно. Всё же для того, чтобы создавать, расширять, улучшать и тестировать код, нужно понимать, что именно он делает, чего не делает и что может делать. Пусть это прозвучит громко, но я считаю, что удобство доказательства является важным катализатором успешного программирования.

Как развивать этот навык

Как я уже писал в начале, описанный мной механизм пошаговых рассуждений даст плоды, только когда вы сможете делать это на бессознательном уровне. Можно в некотором смысле сравнить это со слепой печатью, когда вы не ищете каждую клавишу, а набираете текст интуитивно. Но в любом случае для выработки такой интуиции требуется практика. Вряд ли здесь есть какие-то короткие пути. Нужно просто вложить в это усилия и время.

Пожалуй, лучшим способом будет написание (математических) доказательств. Их составление конкретно для программ определённо поможет, но мне кажется, что простое выстраивание доказательств по любой теме является отличным способом развить логическое мышление, которое очень пригодится при работе со сложными системами (но их нужно писать, а не просто читать. Тренируйтесь!). Лично я начал заниматься математикой уже давно и заметил, что написание доказательств повысило ясность мысли в различных обстоятельствах.

Если вы не знаете, с чего начать, то лично я прохожу курс по алгоритмам для студентов Стэнфорда на платформе EdX. Это интересный курс с акцентом на построении доказательств, который ведёт прекрасный профессор.

Ещё одно неплохое место для обучения — хоть мне и больно это говорить — Leetcode. Как и многие другие, я считаю, что в собеседованиях по Leetcode есть серьёзные недочёты. Тем не менее эта платформа полезна для личной практики, так как многие представленные там задачи достаточно сложны для развития вашей доказательной мускулатуры. При этом не обязательно засекать время (я обычно этого не делаю). Также старайтесь избегать каверзных задач, которые имеют некое «хитрое» решение. Лучше ищите такие, где сложность хотя бы отчасти заключается в правильном формулировании и реализации. Старайтесь добиться успешного решения с минимальным количеством попыток (ничего страшного, если будут возникать синтаксические ошибки).

Успехов вам в программировании и доказательстве!