"Гарантия корректности" как методика обхода багов

Вам когда-нибудь приходилось гарантировать корректность выполнения своей программы? На самом деле это большой объем работы, который не всегда возможно выполнить. В самих доказательствах могут быть ошибки, об этом говорится и в мудрости, взятой из Дао программирования:

Даже в идеальных программах есть ошибки.

Столкнувшись с этими трудностями, Саймон Пейтон-Джонс предложил вот такой выход:

“Я думаю, будет довольно продуктивно сразу обозначить, что в программе обязательно должно или не должно произойти. Например, “это дерево всегда должно быть сбалансировано”. Или “эта функция всегда должна возвращать число больше нуля”. Может быть, в будущем найдется более простой способ гарантировать правильную работу всей программы, но пока что его нет”.

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

Это основной тезис практических доказательств. И кстати: хорошие программисты сразу пытаются увериться в том, что все будет всегда работать как надо, но в одном они порой промахиваются. Они не делятся своими рассуждениями с другими. А ведь доказательство должно пройти проверку не только его создателем — важно проверить, верно ли оно, пересказав свои мысли кому-то еще.

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

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

Вот этот код может уверенно заявить о себе: здесь не могут возникнуть условия гонки (race conditions) и дедлоки. Обратите внимание на то, как именно программист решил эту проблему:

			//------------------------------------------
// Все вызовы к 'slicedMelon' должны
// находиться в этой секции. Необходимо,
// чтобы вы могли визуально убедиться в том, что
// у каждого LOCK есть соответствующий ему UNLOCK.
// Этот мьютекс нельзя использовать в другом месте.
//------------------------------------------
//
// Нет race conditions: эта переменная используется только с мьютексом
// Нет дедлоков: условие Коффмана №4
//
FUNCTION(getResetSlicedMelon,
`
   LOCK(slicedMutex)

   movl  _slicedMelonLocation(%rip), %r12d
   movl  $-1, _slicedMelonLocation(%rip)

   UNLOCK(slicedMutex)

   movl  %r12d, %eax
')

//'
// Сохраняет значение в slicedMelon
// Нет race conditions: для доступа нужен мьютекс
// Нет дедлоков: цепочек ожиданий тут нет
//
FUNCTION(putSlicedMelon,
`
   movl  %edi, %r12d

   LOCK(slicedMutex)
   
   movl  %r12d, _slicedMelonLocation(%rip)

   UNLOCK(slicedMutex)
')
		

Об условиях Коффмана можно почитать здесь.

Можно сделать и проще. Например, как говорит Кен Томпсон: “У моего кода есть одна отличительная черта: он простой, отрывистый и короткий. Так его может прочитать любой человек”.

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

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

			//-----------------------------------------------
// - Valve guard -
// Вся логика управления клапанами находится здесь.
// Клапаны управляются только и только этими функциями.
//-----------------------------------------------
//
// Открывает левый клапан, только если закрыт правый
// Возвращает true, если клапан был открыт
//
FUNCTION(openLeftValve,
`
   movl $ 0, rv

   ifEqual($ 0, _rightValveOpen(%rip),
      `movl $ 1, _leftValveOpen(%rip)
       movl $ 1, rv
       hardwareOpen(left)
   ')
')

//
// Открывает правый клапан, только если закрыт левый
// Возвращает true, если клапан был открыт
//
FUNCTION(openRightValve,
`
   movl $ 0, rv

   ifEqual( $ 0, _leftValveOpen(%rip),
      `movl  $ 1, _rightValveOpen(%rip)
       movl  $ 1, rv
       hardwareOpen(right)
   ')
')
		

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

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

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

Немного исходников из этой статьи (примеры написаны на M4, довольно редком языке).