Все-таки очень хочется от багов избавиться совсем. Разработка по времени тогда сократится значительно, случится счастье и технологический прорыв.
Я видела планы разработки составленные так, будто это счастье уже наступило. Существование багов просто игнорировалось и время на отладку запланировано не было. В конце таких проектов всех всегда ждал бардак и жуткое разочарование. Получалось такое глюкало, что было непонятно нужно ли это отлаживать или лучше сразу выкинуть и забыть. Мораль: если игнорировать реальность, то она больно бьет по ушам.
Итак, ближе к теме. Мне известны два прогрессивных метода, оба в целом не работают. Однако хорошо уже то, что есть люди, которые пытаются думать в этом направлении.
1. Формальное доказательство правильности программы.
Идея далеко не новая, выглядит красиво. Давайте докажем, что программа работает верно. На ВМиК МГУ читается курс по этой теме. По свидетельствам очевидцев доказать правильность программы, которая сортирует пузырьком - весьма нетривиальное занятие. О реально работающем проекте, который размером сильно больше такой сортировки, говорить не приходится.
Формальная верификация - статья в Википедии. Больше правильных ссылок дать не могу, потому что не знаю.
2. Статический анализ кода.
Выглядит уже более реалистично. Натравливаем на проект программу, которая анализирует код и пытается найти ошибки. Я не видела, чтобы эта метода была официально одобрена и использовалась в каких-нибудь компаниях серьезно. Однако, существуют статические анализаторы, которые стоят хороших денег с большим количеством нулей. Наверное их кто-то покупает. Я же встречала только ситуации, когда программисты из любопытства запускали какой-нибудь из таких анализаторов на своем проекте и просматривали результаты.
Народ говорит, что такие анализаторы много шумят не по делу, какие-то ошибки пропускают, но в целом выглядят интересно.
Тут много ссылок:
Static code analysis
Статический анализ кода C++ - обсуждение на Хабрахабре
Best tools noone uses: PREfast - статья на русском, немного про программы-анализаторы вообще, в основном про PREfast
dtjurev: Статический анализ С++ кода
That IACR preprint
3 дня назад
Atom feed
28 коммент.:
Насколько я знаю, в MS используется статическая верификация для поиска потенциальных уязвимостей (переполнение буфера, использование левых указателей и т.п.). Такая верификация встроена в компилятор Visual Studio начиная с 2005ой версии. Подробнее рассказывал Саймон на блогах gamedeff, если не ошибаюсь.
К слову говоря, в среде java статический анализ кода довольно популярен (PMD) и действительно позволяет выявлять типовые ошибки, в частности multithread issues. Так что на мой, взгляд, это никак не технологии будущего, — это суровая реальность. Особенно удобно если статический анализ кода выполняется автоматически во время build'а приложения.
На мой взгляд незаслуженно не упомянули методику TDD (test driven development).
Позволяет не менее эффективно отлавливать баги и стабилизировать поведение.
В целом, она то как раз и появилась в связи со сложностью формального доказательства правильности программы. Теперь правильность доказывает человек через ответную реакцию системы на требуемое ожидание.
А есть еще супер-мега-технология построения программ, когда верификация упрощается.
http://ru.wikipedia.org/wiki/Switch-%D1%82%D0%B5%D1%85%D0%BD%D0%BE%D0%BB%D0%BE%D0%B3%D0%B8%D1%8F
+1 за TDD. Позволяет поддерживать покрытие кода тестами близким к 100%, что в свою очередь позволяет избегать большого количества сюрпризов.
Code Contracts for C# (со статическим чекером, инвариантами и пр.)
http://msdn.microsoft.com/en-us/devlabs/dd491992.aspx
C# проверять относительно просто. С++ сложнее.
ну насчет формальной верификации - на эту тему есть достаточно активные разработки - вот, например, формально верифицированное ядро ОС. Насколько я помню, было еще формальное доказательство системы управления дорожным движением - это из крупных
Работы в области формальной верификации, наряду со статическим анализом, ведутся в MS вместе с некоторыми университетами Англии и Германии. Вообще эта тема популярна в автомобилестроении...
P.S. формальное доказательство имеет наиболиший успех в функциональных языках, поскольку легче учитывать побочные эффекты и т.п. вещи. Тут стоит посмотреть на Coq, Agda2, и т.п.
В Google и Sun начали использовать Findbugs для поиска ошибок/bad practices в java коде
Alexander Nikitin, Alex Ott, Alexey Kuznetsov, а поподробнее можете рассказать?
Ваши комментарии очень похожи, в том смысле, что говорится, "вот там-то и там-то используется то-то и то-то". Интересны, конечно, подробности. Что поймали, что не поймали, что нравится, что не нравится, подводные камни....
ну на доказанное ядро OS я ссылку дал, там много полезных ссылок :-)
Про систему управления дорожным движением - кажется вот это.
На базе Coq (через Why) есть еще системы верификации программ на Java и C
по поводу разработок MS - у меня в одном из университетов знакомый работает, и как-то на channel9 был рассказ про эти разработки (года 2 кажется назад)
Я знаком с системой, в которой к проблеме багов подошли радикально: строится два экземпляра системы, которые разрабатываются независимо двумя разными командами программистов.
Между собой команды не общаются, работают исключительно по ТЗ.
Входные данные и результаты перекрёстно сравниваются, и в случае расхождения система уходит в останов (в этой предметной области это допустимо, в отличии от неверного поведения системы).
Фактически, вся система балансирует на грани останова; если удалось добиться продолжительной работы, значит остались только очень редкие и требующие особых условий баги.
В принципе, этот опыт можно обобщить на тройную систему с голосованием.
Только дорого очень получается и долго.
http://sp.cmc.msu.ru/courses/fmsp/ - вот ссылка на курс, читаемый на ВМК. Действительно, написание формальной спецификации занимает объем кода сравнимый со специфицируемым, а процесс доказательства корректности занимает объем времени сравнимый с временем написания алгоритма )
Еще один пример - Singularity (http://research.microsoft.com/en-us/projects/singularity/) - исследовательская OS, код которой формально проверятся на правильность. Корректность выполнения программы не гарантируются, но гарантируется валидность указателей, корректность состояния комунникационных каналов и т.п.
PREfast/PREfix активно используются в MS (по крайней мере в Windows). Многие из ошибок выдаваемые PREfast/PREfix обязательны к исправлению.
Еще есть такая штука, как time travel debugging (не могу с ходу найти подходящую ссылку). Ход выполнения программы пишется в лог, котороый позволяет прокручивать код в вперед и назад в отладчике. В VS 2010 вроде появилось что-то похожее.
Ну код в TGV поездах на Аде и верифицирован.
Есть книжка Хольцманна
http://spinroot.com/gerard/popd.html
для протоколов.
Ну и сам Хольцман тоже есть с его интересами:
http://en.wikipedia.org/wiki/Gerard_Holzmann
2pustota: я что-то совсем забыл про эту книжку, хотя я когда-то читал ее
из более-менее современных есть еще "Principles of Model Checking", достаточно интересная, ну и серия книг по SPIN Checking
2Елена: а на ВМиК курс верификации кто читает?
C внедрением clang, в xcode от apple также появился статический анализатор. Немного информации по теме
>Еще есть такая штука, как time travel >debugging (не могу с ходу найти >подходящую ссылку). Ход выполнения >программы пишется в лог, котороый >позволяет прокручивать код в вперед и >назад в отладчике. В VS 2010 вроде >появилось что-то похожее.
В gdb есть такая штука как reverse debugging:
http://www.gnu.org/software/gdb/news/reversible.html
из статических анализаторов, пробовал:
cppcheck:
http://apps.sourceforge.net/trac/cppcheck/
но на реальном небольшом проекте (он медленно работает, поэтому лень на большом запустить),
он ничего не показал,
на сконструированных примерах, работает через раз, скажем такую ситацию находит
int *f(void)
{
int tmp;
return &tmp;
}
а такую уже нет
void f(int **p)
{
int tmp;
*p = &tmp;
}
При разработке бортового ПО для Airbus A340, A380 использовалась система ASTREE
На Западе в военных и авиационных разработках применяется SPARK для Ada (например).
Большой список инструментов для валидации C/C++ программ мне недавно подсказал один из читателей.
На предыдущем месте работы у нас по требованию заказчика в проекте использовался анализатор Coverity Prevent. В его использовании были и плюсы и минусы.
Из плюсов: обнаружение на основе анализа кода утечек ресурсов, переполнений буферов, мертвые ветки кода и т.п.; легко интегрируется с имеющейся build-процедурой; результаты анализа хранятся в БД с веб-интерфейсом и возможностью генерации различных отчетов.
Из минусов: в проекте никто не занимался настройкой правил анализа, поэтому результаты анализа часто раздражали разработчиков; фиксам по результатам анализа не всегда уделялось должное внимание, в результате получали сломанную функциональность.
А еще раннее использовали одну из разновидностей lint, но от него отказались т.к. никто не хотел заниматься настройкой правил анализа, а дефолтные правила были слишком жесткими.
Недавно в коммитах OpenBSD были фиксы, найденные с помощью сановского parfait. Вот например (не уверен, что это полный список):
http://marc.info/?l=openbsd-cvs&w=2&r=1&s=parfait&q=b
Не очень много фиксов, но в OpenBSD качественный код.
http://www.mail-archive.com/misc@openbsd.org/msg83116.html
Для питона есть весьма популярное средство pylint, и оно действительно немного помогает.
Был такой проект Verisoft. Там формально доказывали корректность микропроцессора, оси и прикладных программ типа почтового клиента, компилятора и тп. И в принципе, достаточно успешно.
Сколько ни видел попыток ввести статический анализ кода для C++ проектов, все были провальными. По моим ощущениям, статический анализатор кода для C++ бывает полезен только в одном случае - если он использовался с самого начала проекта. Все же попытки натравить анализатор на кучу уже существующего кода скорей всего закончатся провалом.
Есть ещё "не статический" анализ, не знаю правильного научного термина для него.
В частности, для отладки lock-free алгоритмов и других алгоритмов синхронизации есть прекрасная уттилита от нашего соотечественника Дмитрия Вьюкова: http://groups.google.ru/group/relacy/web
Она не позволяет проверять крупные куски кода, но всё равно на порядки проще статической верификации.
2kaa.python: вот здесь на 4-й странице в разделе "New Kinds of Debugging Tools" описывается опыт использования PolySpace для C++ проекта и там же есть комментарий специалиста PolySpace о качестве их анализатора. Сам документ относится к 2003-му году, так что, возможно, сейчас ситуация получше.
Я так же поинтересовался, где используется статический анализ и верификация программ. Тот же PolySpace описывает несколько C++ проектов. Вроде бы не очень больших по объему (речь идет, кажется о 15-20K строк). Сможет ли анализатор проглотить что-нибудь типа ACE или Qt -- большой вопрос :)
Так что, думаю, вы правы. На небольшом C++ проекте и с самого начала анализатор будет работать. А вот потом -- вряд ли.
2davemilter:
> скажем такую ситацию [cppcheck] находит [...] а такую уже нет [...]
Спасибо. Повесил тикет с вашим тест-кейсом: http://sourceforge.net/apps/trac/cppcheck/ticket/1198
QuickCheck - описывааем свойство функции и он его проверяет на случайно сгенерированных данных, делая сотни проб
Отправить комментарий