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

[Ares_ekb]

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

[worldmind]

Это подводит нас к качеству профессионального образования.

[worldmind]

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

[click0]

Формальная логика, а конкретно — многозначная логика.

[rotarepo]

«Но в то же время есть ещё один способ справиться со взрывом пространства состояний: бросить на него больше оборудования»

Только всего оборудования на Земле не хватит для решения даже относительно простых задач. Автор похоже не вникал в суть того, что он переводит. Реально методы, основанные на исследовании пространств состояний, работают только для очень ограниченного круга небольших по размеру задач. Вот о том, какие это задачи, и стоило бы сказать.

[xfaetas]

Кто-нибудь пробовал обучить этому искусственный интеллект?

[amazed]

Обычно сначала реализуется какой-то сложный алгоритм, который со всей очевидностью должен работать как надо во всех случаях, а потом находится случай, когда он делает не то что нужно. Для меня единственный способ обнаружить такую ситуацию — долго дебажить код по шагам в разных ситуациях и размышлять что еще здесь не учтено. Это если я пишу код сам. Если я только ставлю задачу, а ее решает программист с тестировщиками, то тут получается все плохо: программист торопится сделать и сдать а тестировщик не понимает алгоритм настолько глубоко, чтобы проверить все или отличить ситуацию когда что-то идет не так от ситуации, когда он что-то сделал не так. Приходится вмешиваться в тестирование и разработку, тратить много времени. В итоге бывает проще решить всю задачу в одиночку. Какое-то организационное решение этой проблемы наверняка существует, но не знаю какое. Распространенный вариант — вообще избегать задач, которые требуют сложных алгоритмов или поручать их полностью одиночкам-универсалам.

[JC_IIB]

Очень интересная статья. В каменты призывается 0xd34df00d :)

[ebt]

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

[Shm-Alex]

В 70 годы было полно инженеров, которые чертили за кульманами детали, собирали эти чертежи в сборки, по чертежам вытачивали реальные детали и в конце концов собирали большую ракету, и возникла мысль что также можно поступить и с производством software
Нарисовать sofware requrement (чертёж детали) и написать код по требованиям (выточить деталь) проверить соответствие кода требованиям и будет работать также как как в производстве из железяк.
Но тут возникла проблемка. чертёж детали стал настолько же сложным как и сама деталь. Модель стала сложна так же как её реализация в коде, проверить что реализация соответствует модели можно только если ещё раз её реализовать иначе тесты утопают в бесконечном количестве тестовых примеров и их результатов и вообще не понятно то что зафиксировано в требованиях это то, что нужно непосредственно заказчику.
Все до сих пор в тупике. Ну просто это не работает и всё. Можно покрыть код тестами на 100% по MC/DC но это не даст гарантии что требования реализованые в коде есть имплементация скрытых, потаённых и ещё не высказанных желаний потребителей этого SW.
Есть методики которые позволяют увеличить надёжность того что реализовано( например ). Но цель их не верификационные / валидационные процессы по отношению к артефактам возникшим в процессе разработки и не какое-то формальное доказательство соответствия одного другому, а доскональное изучение человеком в ручном режиме того что делает программный комплекс.

[Gryphon88]

Как фактически пишется верифицированный код? С [неверифицированного] нуля, или есть коллекция уже верифицированных библиотек, которая пополняется и используется в проектах?

[Ares_ekb]

Я не очень спец в этом и наверное есть много вариантов. Один вариант: код или какие-нибудь фрагменты кода импортируются, например, в Isabelle HOL. В Isabelle HOL формулируются ограничения для этого кода и доказывается, что импортированный код соответствует этим ограничениям. Например, есть функция для сортировки массива, транслируем её в Isabelle HOL и доказываем, что сохраняется количество элементов в массиве, что элементы результирующего массива действительно отсортированы, что сортировка происходит за определенное время в зависимости от длины массива или что этот алгоритм не зацикливается и т.д.

Другой вариант, пишем код изначально в Isabelle HOL, доказываем там всё что нужно. А потом преобразуем код в Haskell, Scala и т.п.

[dargo]

Есть так же метод Б (https://en.wikipedia.org/wiki/B-Method) с практическим применением например для автономной ветки метро или космического корабля Ариан-5.

Желающие могут самостоятельно попробовать — «Atelier B is an industrial tool that allows for the operational use of the B Method to develop defect-free proven software (formal software)». На выходе автоматически генерируется код на С или Ада.

Ссылки:
www.atelierb.eu/en
www.atelierb.eu/wp-content/uploads/sites/3/dbprotect/formations/slides/formation-atelier-b-formation-niveau-1-en.pdf

Интервью Jean-Raymond Abrial (создатель метода Б) для журнала 01net о формальных методах в 2002г (извиняюсь за корявый перевод).

www.01net.com/actualites/jean-raymond-abrial-consultant-le-zero-defaut-nexiste-pas-mais-on-peut-tout-de-meme-sen-approcher-173964.html

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

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

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

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

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

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

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

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

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

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

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

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

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

[PsyHaSTe]

Советую читать оригинал. Пытался читать тут, но сдался, пытаясь понять фразу

> Доказательства трудны, и это очень неприятная работа. Трудно «бросить программирование и уйти в цирк».

Открыл оригинал, нашел там

> Proofs are hard. Obnoxiously hard. “Quit programming and join the circus” hard.

Проблема серьезная, перевод ужасен.