[prog] Прочитал несколько интервью Бертранда Мейера (часть 1)

Бертранд Мейер в своем блоге дал ссылки на ряд своих недавних интервью в русскоязычных изданиях. Два из них (в Коммерсанте и в Открытых системах) я прочитал. Интересно. Прежде всего потому, что, на мой взгляд, Бертранд Мейер занимает уникальную позицию – сильно посередине между прикладными разработками и научными исследованиями. И, в какой-то мере, является проводником научных достижений в мир прикладной разработки (хотя на эту тему, вероятно, можно сильно спорить).

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

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

Насколько я понимаю, сейчас можно проводить верификацию программ тремя способами:

1. Статический анализ корректности кода в отсутствии формальных спецификаций. Такой анализ выявляет “тривиальные ошибки” как то: отсутствие возврата значения из функции в какой-то из ветвей, обращения к неинициализированным переменным, потенциальные переполнения при выполнении арифметических операций, выходы за пределы массивов и т.д. Часть этих ошибок выявляют сами компиляторы (например, отсутствие return-ов или выбрасывание исключения, не задекларированного в секции throws в языке Java). Часть вылавливают специализированные статические анализаторы. Главное же в этом способе то, что он способен отыскивать “баги”, но ничего не может сказать о правильности работы кода. Т.е. можно написать программу без багов, которая будет делать совсем не то, что нужно. Например, переводить деньги со счета на счет без предварительной проверки допустимости такой операции (например, отсутствие достаточной суммы на исходном счете).

2. Проверка выполнения контрактов программных компонентов. В первую очередь здесь должна быть упомянута система Design By Contract из языка Eiffel (которую так же пытались сделать в D), а так же разного рода попытки реализовать ее в других языках (в виде специальных комментариев или аннотаций). В принципе, в примитивном виде эта практика реализуется даже в C на основе assert-ов. На мой взгляд, DbC – очень неоднозначная вещь. Имел опыт работы с ней во время изучения Eiffel-я. В чем-то она хороша, в чем-то нет. Как бы то ни было, контракты хорошо подходят для небольших повторно используемых компонент (например, библиотек контейнеров или стандартных алгоритмов), а вот доказательство правильной работы некоторого заточенного под конкретного заказчика приложения с помощью контрактов вряд ли можно сделать.

3. Проверка соответствия программы заранее определенным спецификациям. Т.е. сначала для приложения на каком-то формальном языке формируется точная и полная спецификация, затем на каком-то языке программирования эти спецификации воплощаются в реальный код (вручную или посредством кодогенерации), а затем посредством специализированных инструментов (в первую очередь статических анализаторов, а так же run-time анализаторов и генераторов наборов тестовых данных и воздействий) проверяется соответствие реализации исходной спецификации.

На мой дилетантский взгляд, стоимость и сроки разработки существенно возрастают при использовании средств верификации программ. Причем чем более серьезное (а значит и надежное, качественное) средство используется, тем дороже и длительнее будет разработка (в качестве примера можно вспомнить упомянутый мной когда-то проект Tokeneer, выполненный с использованием SPARK Pro).

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

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

Один из очевидных факторов – это полнота и корректность составления исходной спецификации. Но тут лучше слушать не меня, а тех, кто этим вопросом вплотную занимается.

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

Во-первых, не смотря на то, что в разных методиках (скажем, Test Driven Development) требуется писать тесты до кода, намного, намного чаще делается наоборот. Сначала пишется код, разработчик убеждается, что код делает то, что нужно (делая один или два теста для подтверждения работоспособности кода). И лишь потом приступает к более полному тестированию – проверке граничных условий, некорректных входных данных, отсутствия ресурсов и пр. Причем так делают даже при использовании того же TDD – изначально создавая минимальный набор тестов, показывающих работоспособность кода на тривиальных сценариях. И это неспроста, поскольку есть еще и…

Во-вторых, существует замечательный афоризм: Everything should be built top-down, except the first time (т.е. все нужно разрабатывать сверху-вниз, за исключением самого первого раза). И это очень точно описывает ситуацию с разработкой ПО. Нам ведь не так уж часто приходится делать одно и то же снова и снова. Даже в чем-то похожие задачи все равно различаются в деталях. И начиная что-то делать мы далеко не всегда даже знаем, получится ли что-нибудь или не, а если и получится, то что именно. Если же мы не знаем, что получится на выходе, то как можно заранее покрыть итог нашей работы формальными спецификациями?

На эту тему мне вспоминается случай, который произошел на заре моей профессиональной карьеры. Нужно было сделать отображение векторных картинок в окне с возможностью масштабирования и скролирования. Если бы это был наш формат и если бы мы сами отрисовывали картинку, то дело было простым. Но картинка сохранялась в WMF-файле (Windows Metafile) и отображалась средствами Windows (тогда еще 3.11). Я убил на это дело неделю, выкуривая те крохи документации по Windows API, которые были в моем распоряжении и проделывая по несколько неудачных экспериментов в день. В конце-концов, в состоянии, очень близком к отчаянию, я все-таки смог разобраться с премудростями SetWindowOrg, SetViewportOrg и деталями воспроизведения метафайла – WMF начал масштабироваться и скролироваться.

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

В случае же с формальной верификацией такой свободы, насколько мне представляется, нет. А значит и драйва, который разработчик иногда получает от программирования, тоже нет :( А какой же тогда смысл в программировании, если нет кайфа и драйва? ;)

PS. Кстати, в разработке прикладного ПО есть немалая доля субъективизма. Вот тоже отображение метафайла средствами ОС – как формально специфицировать корректность этого отображения? А ведь разработчик просто взглянув на картинку в состоянии точно дать ответ – правильно она отображена или нет. Если же взять такой пласт проблем, как расположение органов управления в диалоговых окнах, их цвета и размеры, моменты замораживания/размораживания и пр. составные части usabillity…