четверг, 5 января 2012 г.

[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…

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

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

мда

такая ситация, когда "что-то надо заставить работать", а исходники закрыты (или сложны непропорционально решаемой мной задаче) -- типа вывода wmf через апи виндов -- это то, что я всегда стараюсь избегать

и то, что оно несколько раз че-то вывело на взгляд вроде как правильно -- это ВОВСЕ не значит, что оно заработало правильно, так что наезд с этой стороны на формальные методы не катит

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

где-то на цитфоруме я читал критическую статью насчет формальных метов -- основной пойнт был в том, что они делаются не для практического применения, а для дисера

и видимо это основная причина, почему они в загоне

http://eao197.blogspot.com/2011/08/prog-specification-explosion.html есть мой комментарий и твой ответ, так что можно продолжить с той точки уже здесь

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

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

мой пойнт и ответ в том, что "формализация всех деталей" на самом деле может и не требоваться -- если подойти к делу правильно

вот пример

я видел жуткий баг при игре в покер -- дело в том, что около кнопки call высвечивается сумма которую игрок подтвердает, но поскольку в это же время кто-то другой может эту сумму поднять, то в момент, когда палец игрока уже почти давит на кнопку мыши, эта сумма может подскочить на двести баксов

т.е. запросто пролететь на 200 баксов -- если бы там эта сумма была с самого начала, игрок не стал бы колл-ить

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

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

правильный подход к проектированию тут заключается в моделировании игрока не как бесконечно-быстрой системы, а как параллельно-исполняющейся нити

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

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

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

правильная привычка будет переносить тяжесть борьбы с деталями именно на формальные методы верификации (при условии, как я сказал раньше, что они будут достаточно продвинуты, примерно как type inference)

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

первый момент, из-за которого формальная спецификация втрое длиннее программы -- это отсутствия аналога type inference для вывода

второй -- это попробуй формально записать " массив В является отсортированным массивом А"

отсортированность пишется элементарно, но вот "В является перестановкой А" это бойлерплейт, с которым, очевидно, будет трудно проводить какие-то логические выводы

третий, который может и является пересказом первого и второго -- это то, что некоторые алгоритмы (например, перестановка) ИЗНАЧАЛЬНЫ и не являвляются результатом стремления к выполнению некоторой формальной спецификации

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

ладно, насчет изначальности я не совсем прав -- там надо дальше думать

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

@имя:

Не понял двух вещей.

1. Про закрытые исходники и чужой API. Эта ситуация встречается сплошь и рядом. Есть устойчиво наблюдаемый положительный результат работы ПО (правильное отображение картинок, правильная работа внешних устройств и т.д.), но лично у меня нет никакого понятия о том, как эту правильность можно формализовать. Так что я продолжаю настаивать на том, что в ряде областей формальным методам (пока?) места нет. И не вижу опровежения в твоих словах.

2. Не понятно, как переход к другому взгляду на игрока в покер делает приминимым к нему формальных методов.

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

@Евгений

Упустил еще языки системы типов которых позволяют выражать формальные спецификации. Очень слабо это конечно позволяют и такие жестко типизированные языки как окамл или хаскель и даже C++, но сейчас появились и специализированные языки поддерживающие зависимые типы. Например ATS или Agda. По ATS кстати тут http://thedeemon.livejournal.com/tag/ats недавно неплохо отписался товарищ с rsdn. Странно что Мейер о них не упоминает, или у него как у Вирта аллергия на ФП? Хотя ATS и не ФП по сути.

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

1.

>правильная работа внешних устройств

ыыы! это называется "кажется, что работают"

вот скажем драйверы для Prolific PL2303 (это ком-порт через юсб для подключения мобильника) обрушили у меня винду ХР до синего экрана первый же раз, когда я выдернул устройство чуть раньше, чем надо (какой-то обмен данными еще не закончился)

я почти уверен, что у основных драйверописателей для видяхи (nvidia, ati) есть доступ к исходникам directx и прочей околовидео-фигни, а в том, что у них есть доступ к описанию железа -- никто и не сомневался

> лично у меня нет никакого понятия о том, как эту правильность можно формализовать.

формализовать можно все, но как это сделать удобно -- это вопрос к господам ученым

> в ряде областей формальным методам (пока?) места нет.

пока -- это чистый К.О.

а не пока -- можно продолжить спор

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

2. это такая политкорректная фраза чтобы не согласится, или и правда непонятно? мне вот непонятно, что тебе непонятно

взглядов на игрока в покер может быть 2:

А. он просто смотрит на интерфейс и давит на кнопки... ужасный баг говорите? да, да, че-то мы головой не додумали когда проектировали...

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

минимальная попытка формализовать "точно отобразить ситуацию" сразу приводит к вопросу -- а какую ситуацию? она ведь меняется

дальше строим модель: сервер -- задержки -- прога -- задержки --глаза игрока -- задержки -- мозг -- задержки -- рука -- задержки -- прога -- задержки -- сервер

и т.д.

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

короче: простая попытка формализовать ситуацию с целью последующего применения формальных методов уже приводит к нахождению гонок

вопрос -- нужно ли дальше там будет че-то верифицировать? ну если правильно спроектировать интерефейс (точнее, способ взаимодействия), то, возможно даже верификация будет тривиальна

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

а потом еще неясно противопоставление поиска и верификации

научные результаты находятся практически всегда путем поиска, хотя верификация очень помогает

а еще такой пример:

можно найти поиском как пропатчить (бинарную) программу, чтобы она не проверяла серийник, а потом формально доказать, что пропатченная версия работает ровно так же, как не пропатченная

такой высококачественный, формально верифицированный кряк, гы-гы

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

что касается покера, то я почти уверен, что эти разработчики отсылали из интерфейса на сервер голую команду "CALL" вместо "CALL $15" например

это значит, что юзер вообще мог не увидеть ту сумму, которую он коллит -- он видит $15 на кнопке, нажимает ее, а пока команда "CALL" идет 0.2 секунды до сервера, кто-то рядом с сервером поднимает ставку до $200

за такое поведение фирме, наверно, можно впаять срок за мошенничество

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

* кто-то рядом с сервером поднимает ставку до $200, и пришедший голый "CALL" рассматривается сервером как "CALL $200" вместо сделанного игроком "CALL $15"

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

@имя:

>или и правда непонятно? мне вот непонятно, что тебе непонятно

Это нормальное явление при обмене мнениями между людьми -- то, что прекрасно укладывается у тебя в голове, может быть совершенно непонятно другому человеку :)

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

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

@Rustam:

Про зависимые типы я не копенгаген, поэтому не затрагивал эту тему.

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

"они не знали"

1. они просто НЕ МОГЛИ об этом не знать, поскольку они сделали интерфейс так, что он показывал это асинхронное изменение ставки

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

______________________

насчет непонимание -- непонимание да, естественное явление; кстати, меня не понимают весьма часто;

и тут я правда затруднился понять, что тебе не ясно

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

@имя:

> они просто НЕ МОГЛИ об этом не знать, поскольку они сделали интерфейс так, что он показывал это асинхронное изменение ставки

Тогда остается две версии:

1. Это был действительно баг. И тогда есть открытый вопрос -- сколько подобных багов эти же разработчики допустили бы в спецификации, по которой бы потом проводилась верификация.

2. Такое поведение было сделано намеренно. И тогда аналогичным образом была бы составлена спецификация.

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

в обоих случаях -- а что, кто-то с пистолетом заставлял фирму

1. принять спецификацию, написанную разработчиками?

2. поручать писать спецификацию тем, я почти уверен, индусам, что слабали интерфейс, а не грамотным людям?

ведь денежную ответственность будет нести фирма, а не разрабы (если вообще будет; онлайн покер вообще в сша запрещен, а емнип в канаде разрешен)

если вспонить реальный случай когда в японии продали 10000 акций по 1 доллару вместо 1 акции по 10000 долларов, то емнип (фирма)-разработчик че-то по-мелочам заплатил, но только чтобы не терять постоянного заказчика -- так что разработчику плохая спецификация тоже не все равно, но вряд ли на него можно наехать судебно

а индусам, разово нанятым, пофиг

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

на самом деле, формальная верификация она возможна только после так сказать аксиоматизации предметной области

т.е. выбрали набор неопределяемых понятий; выбрали набор аксиом -- например, для гуя аксиомой может быть:

если виджет таков, что его bounding box не пересекается bounding box-ами других виджетов, то виджет отображается правильно

тут *сразу* возникает вопрос -- а что если bounding box пересекается с границами формы? поэтому аксиому надо уточнить

дальше аналогичная аксиома для "работает правильно" (т.е. обработка событий)

дальше аксиома для составных виджетов

... короче, довольно много работы

и последний, небольшой шаг -- это формальное (и 99% что тривиальное!) доказательство на основе этих аксиом, что виджеты, которые разложил наш layout manager, отображаются правильно и работают правильно

вот этот последний небольшой шаг люди почему-то считают чуть ли не всей формальной верификацией

видимо потому, что им в универе рассказывали про тройки хоара

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

* вот этот последний небольшой шаг люди почему-то считают чуть ли не всей формальной верификацией;

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

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

хотел написать "очевидно", а потом задумался...

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

имя комментирует...
Этот комментарий был удален автором.
имя комментирует...

s/неопределяемых/формально неопределяемых/

т.е. скажем "обычный виджет" это неформально определяемое понятие, его неформальное определение возможно будет "объект одного из классов Text, Label, Scrollbar, ListBox" -- но поскольку эти классы у нас формально не верифицированы, то определение неформально

а вот определение виджета типа "виджет это либо обычный виджет, либо составной виджет" и "составной виджет это tuple из других виджетов (подвиджетов); его bounding box это объединение bounding box-ов его подвиджетов" уже может рассматриваться как формальное, если у нас хотя бы неформально определены "bounding box", "объединение" и "обычный виджет"

____________________

з.ы. удаленный коммент не прошел typecheck после опубликования :-)

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

@имя:

Я не знаю, почему разработчики покера поступили именно так. Не исключено, что вмешались основные причины -- время и деньги ;)

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

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

Может как раз поэтому верификацией пока занимаются в академических кругах. Там можно тратить время на эксперименты с заранее неизвестным итогом. А вот в производстве есть ограничения и по срокам, и по бюджетам. И если кто-то начнет в реальном проекте с постоянно приближающимся дедлайном и меняющими требованиями выстраивать аксиоматику для контролов на формах, то проект просто не закончат в срок.

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

я рассуждаю в контексте

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

а вопрос в каком количестве *нужно* их применять, чтобы повысить качество/надежность ПО -- это другая половина

да, там влияет оплата, точка зрения заказчика и т.д. (к.о. напоминает, что качество всегда стоит денег и времени)

но даже и без желания заказчика и руководства -- в минимальном объеме бывает это необходимо

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

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

@имя:

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

Насколько я понимаю, изыскания в области зависимых типов в ФП как раз в этом направлении и идут. Хотя, повторюсь, в этой теме я не разбираюсь.