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