Почему люди не используют формальные методы?

Насколько применимы SAT/SMT-солверы в дескрипционной логике?

Формальные методы повышают надёжность программного обеспечения, но их использование не распространено. Как вы это объясните?

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

Формальные методы подразумевают затраты большего времени на спецификацию, чем на тесты. Не ставит ли это под сомнение обычный цикл разработки?

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

В чем сложность использования формальных методов?

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

В каких случаях формальные методы наиболее применимы?

Их достаточно много. Например концепция распределенных систем: проблема в том, что в них не существует «главного». В протоколе маршрутизации узел сети не предпринимает решений за другие узлы. Информация меняется и на каждом узле заново определяется дальнейший маршрут, в зависимости от особенностей локальной сети. Таким образом, очень трудно проводить тесты в подобных условиях, так как эти условия исполнения никогда не повторяются. Формальные методы, отчасти, используются для разработки протоколов передачи, маршрутизации и криптографии. Эти методы все больше и больше применяются в задачах, которые неограниченны лишь разработкой софта. В частности, при изучении сложных систем. Необходимо реализовать объект, над которым будет производится дальнейшее размышление, строго соответствующее модели объекта.

В каких странах более всего используются формальные методы?

Европа немного впереди планеты всей. В частности Франция, Англия и Германия. Что же касается американцев, то и них много денег и хорошие методы работы. Люди, участвующие в проекте, очень ответственны. Это компенсирует часть проблемы. В профессиональном отношении, они придают огромное значение качеству специалистов. Кстати, в больших компаниях можно часто встретить высокопоставленных работников, которые сами являются специалистами (в тексте техниками). Технические знания высоко ценятся, это позволяет создавать качественные системы.

Являются ли формальные методы панацеей?

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

Jean-Raymond Abrial, независимый консультант и «изобретатель» формального метода B.