пятница, октября 12, 2007

Correct by construction

Существует много приемов, способов и методологий разработки программ. Один из них, не самый заезженный, но очень полезный — это Correct by construction. Суть его проста до безобразия: корректную программу можно построить только из корректных частей, корректно соединяя их друг с другом.

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

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

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

Здесь я говорю не о «защите от дурака», когда система не реагирует на неверное использование, а о том, чтобы вообще не допустить этого «дурака» к системе. А если нет дурака, то не нужна и защита от него.

Кстати, под интерфейсом я понимаю не только набор методов в классе, или функций в модуле, но еще и элементы языка программирования, ведь они тоже соединяют элементы программ (кстати, ни один из известных мне языков программирования не поддерживает полностью принцип Correct by construction, хотя некоторые и стремятся).

Что же подразумевается под корректными интерфейсом? Да собственно такой интерфейс, который физически нельзя использовать не по назначению. Примеры:

  • Если функция, в случае ошибки, возвращает -1, NULL, или любое другое магическое значение, то когда-нибудь это значение не будет обработано. А если функция возвращает опциональный тип (option, Maybe, или как он называется в вашем языке), то возможность забыть обработать ошибку отпадает сама собой.


  • Прямая работа с указателями или массивами в принципе не может дать гарантий безопасной работы с памятью. Но если к массивам можно достучаться только через функции вроде map, fold, iter, то no problemo: нет индексов — нет ошибок с индексами (а в будущем, надеюсь, проблема безопасного доступа к массивам по индексам решится при помощи dependent types).


  • Наличие явных функций open/close, create/destroy, alloc/free всегда оставляет возможность не освободить занятый ресурс. А если использовать RAII или функции типа with_resource, то у потенциального «дурака» в принципе не получится что-то забыть &mdash ведь не он теперь заведует ресурсом.


  • У вас много изменяемого состояния. Боитесь, что кто-то изменит его не в том порядке? Разбиваем на кусочки, делаем функциональный интерфейс, и уже ни у кого не получится перепутать вкл. и выкл.


  • Нельзя нажать на эту кнопку — так может ее вообще убрать или сделать disabled?


Список можно продолжать долго.

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

Система будет истинно корректной только тогда, когда ее нельзя некорректно использовать. И только из таких систем можно создавать еще большие корректные системы. Это и есть Correct by construction.

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

10 комментариев:

_winnie комментирует...

>(option, Maybe, или как он называется в вашем языке) то возможность забыть обработать ошибку отпадает сама собой.

Гхм, чем оно отличается от NULL для настоящего мужика?

NULL -> //об этом я подумаю завтра
_ -> do something


ИМХО, важнее не безопасность интерфейса, а его понятность.

Лучше ясное и понятное описание "вызвать в таком порядке", чем непонятная хитрозапутанная система только ради того, что бы не дать вызвать не в том порядке.

И обязательна "культура" человека, его использующего.

По поводу "забыть close после open":

Когда мы начинаем оптимизировать на "высоком уровне", то появляются всякие _сложные_ кеши "сделать close, если не пользовались в течении минуты, иначе хранить, вдруг воспользуются через секунду". Тут защиту от дурака при написании такой вещи ну никак не сделаешь.

Таки я за культуру пользователя и за понятность!

Unknown комментирует...

2 winnie:

>>(option, Maybe, или как он называется в вашем языке) то возможность забыть обработать ошибку отпадает сама собой.

>Гхм, чем оно отличается от NULL для настоящего мужика?

Примерно тем же, чем static_cast отличается от C-style cast.

Найти все использования функции fromJust в проекте значительно проще, чем найти все необработанные нулевые указатели, коды ошибок и т.д.

Vladimir Shabanov комментирует...

Таки я за культуру пользователя и за понятность!

Дык откуда ж она возьмется у настоящего мужыка? ;)

Лучше ясное и понятное описание "вызвать в таком порядке", чем непонятная хитрозапутанная система только ради того, что бы не дать вызвать не в том порядке.

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

то появляются всякие _сложные_ кеши...

Все-таки лучше сложный кеш, чем сложный resource leak.

Анонимный комментирует...

Только мне кажется что это перепечатка книги Solid Code?

Vladimir Shabanov комментирует...

Интересно. А эта книга где нибудь есть в электронном виде?

И что-то я именно Solid Code не нашел. Имелась ввиду Writing Solid Code?

Анонимный комментирует...

Да, имелась в виду Writing Solid Code - просто сейчас ее читаю, сразу в глаза бросилось. В интернете точно есть, находил недавно, правда все равно читаю в бумажном варианте.

Анонимный комментирует...

Использование опционального типа возвращаемого функцией значения есть de facto возвращение двух значений - "нормального" результата и характеристики результата (норма/ошибка); опциональный тип в Haskell - один из вариантов реализации этого подхода, но не единственный. При этом на самом деле возможность не обработать информацию об ошибке есть всегда :-)

Vladimir Shabanov комментирует...

> возможность не обработать информацию об ошибке есть всегда :-)

С той разницей, что с опциональным типом это необходимо делать явно (используя какой-нить fromJust).

Eklykti комментирует...

> Но если к массивам можно достучаться только через функции вроде map, fold, iter, то no problemo

Предлагается прокручивать 8999 элементов массива, чтоб достучаться до 9000ного?

Vladimir Shabanov комментирует...

Прямое обращение по индексу нужно не так часто. И если вместо fold/iter/map/foreach постоянно использовать for (i=0;...), то вероятность напороться на ошибку увеличивается.