В прошлых публикациях уже немного касался Логики Хоара. На всякий случай напомню: логика Хоара — это метод структурирования доказательств корректности програм. В контексте разработки программного обеспечения Хоар предложил использовать пред- и постусловия для описания поведения программных компонентов. Предусловия определяют, какие условия должны быть выполнены до вызова функции, а постусловия — какие условия должны быть выполнены после.
Мне кажется от таких вещей разработчики часто отмахиваются, мол, какое-то академизированное понятие, зачем оно мне в “реальной” работе. Ведь многое из того, что рассказывают в университете и на некоторых, менее практически ориентированных курсах Computer Science на поверку оказывается не всегда хорошо применимо к работе в IT-индустрии.
Эта, однако, как-то прочно осела в уме как на самом деле очень практичный инструмент. Логика Хоара “встраивает” в голову очень, как мне кажется, правильный “майндсет”, а именно: думать о каждой структурной единцы программы (функция/метод, класс, не принципиально) с точки зрения триплета “предусловия-инструкция-постусловие(ия)”.
Во-первых, это позволяет думать о каждой функции как о своего рода “интерфейсе” для приёма данных -> преобразовании -> получении результата на выходе. Из таких небольших частей затем складывается единицы более высокого уровня, причём уверенность в понимании каждой такой трансформации превращается в уверенность в корректной работе всей системы в целом.
Во-вторых, можно вспомнить про принцип Лисков, а именно ту его часть которая говорит, что при наследовании:
- Нельзя ослабять предусловия.
- Нельзя делать более строгими постусловия.
На самом деле эти правила применимы к любым изменениям кода, а не только наследованию, потому что они придуманы с целью сделать код устойчивым к “разрушающим” модификациям. Ещё одно выражение принципа Лисков - “не делать сюрпризов” для пользователей кода. “Сюрпризом” может быть как раз например получение менее надежного результата, чем было заявлено ранее (ослабление постусловия), обратная же ситуация как правило не вызывает проблем.
Эта идея как раз напрямую связана с логикой Хоара. На практике это даёт нам своего рода метрику качества произведённой функции, по следующим критериям:
- Делать предусловия как можно менее строгими.
- Получать как можно более строгое/ограниченное постусловие(ия) (а ещё лучше, чтобы оно было только одно, но об этом чуть ниже).
А как добиться более строгости постусловий? Принцип единой ответственности гласит, что у каждого класса, модуля или функции должна быть только одна причина для изменения. Это важное правило помогает поддерживать код чистым, читаемым и легко модифицируемым. Но на практике это понятие всегда казалось мне довольно размытым, но если думать об этом как о произведении одного сторого постусловия, то всё становится более понятным.
Многие принципы CS оказываются тесно переплетены друг с другом и взаимно дополняют друг друга и будто бы ведут к какому-то единообразоному пониманию того, “как надо делать” программы. Да, за более чем полвека развития Computer Science будто уже были придуманы практически все фундаментальные идеи как писать код получше, но в мейнстрим к обычному разработчику они проникают очень неспешно. Открывая для себя потихоньку такие вот идеи может получится чуть меньше наводнять мир плохим, грязным и трудно поддерживаемым кодом.