Хабрахабр

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

На Software Engineering Stack Exchange я увидел такой вопрос: «Что мешает широкому внедрению формальных методов?» Вопрос был закрыт как предвзятый, а большинство ответов представляли собой комментарии типа «Слишком дорого!!!» или «Сайт — это не самолёт!!!» В каком-то смысле это верно, но мало что объясняет. Я написал эту статью, чтобы дать более широкую историческую картину формальных методов (FM), почему они на самом деле не используются и что мы делаем для исправления ситуации.

На самом деле существует не так много формальных методов: всего несколько крошечных групп. Прежде чем начать, нужно сформулировать некоторые условия. В широком смысле есть две группы формальных методов: формальная спецификация изучает запись точных, однозначных спецификаций, а формальная проверка — методы доказательства. Это означает, что разные группы по-разному применяют термины. Мало того, что мы используем разные термины для кода и систем, мы часто используем разные инструменты для их верификации. Сюда входят и код, и абстрактные системы. А если кто-то говорит, что делает формальную верификацию, обычно это относится к верификации кода.
Для ясности разделим проверку на верификацию кода (CV) и верификацию дизайна (DV) и таким же образом разделим спецификации на CS и DS. Чтобы ещё больше всё запутать, если кто-то говорит, что создаёт формальную спецификацию, обычно это означает и верификацию дизайна. Начнем с CS и CV, затем перейдём к DS и DV. Такие термины обычно не используются в широком сообществе FM.

Это может быть разница между доказательствами утверждений «система никогда не выходит из строя и не принимает неправильный пароль» или «система никогда не выходит из строя и блокирует учётную запись, если трижды ввести неправильный пароль». Кроме того, возможна частичная верификация, где проверяется только подмножество спецификации, или полная верификация. В основном, будем предполагать, что мы делаем полную проверку.

Большинство людей неявно выделяют высоконадёжные программы, такие как медицинские устройства и самолёты. Также следует уточнить тип программного обеспечения, которое мы формализуем. Это слишком оптимистичный взгляд: в большинстве высоконадёжного ПО не используются формальные методы. Люди предполагают, что для них формальные методы широко используются, а для остального не нужны. Вместо этого мы сосредоточимся на «обычном» софте.

Кроме того, я специализируюсь на формальной спецификации (DS и DV), поэтому больше вероятность ошибки там, где я говорю о верификации кода. Наконец, дисклеймер: я не профессиональный историк, и хотя пытался тщательно проверить информацию, в статье могут быть ошибки. Если увидите, пишите мне, я исправлю (и ещё: я зарабатываю на проведении семинаров по TLA+ и Alloy, поэтому очень предвзято отношусь к этим языкам; я пытаюсь быть максимально объективным, но сами понимаете: предвзятость — это предвзятость).

Получение спецификации

Прежде чем доказать корректность кода, нужно получить эталон истины. Это означает некую спецификацию, что должен делать код. Мы должны точно знать, что результат соответствует спецификации. Недостаточно сказать, что список «отсортирован»: мы не знаем, что сортируем, какие критерии используем и даже что мы подразумеваем под «сортировкой». Вместо этого можно сказать: «Список целых чисел l отсортирован в порядке возрастания для любых двух индексов i и j, если i < j, то l[i] <= l[j]».

Спецификации кода делятся на три основных вида:

  1. Первый — написание независимых от кода операторов. Напишем нашу функцию сортировки, а в отдельном файле напишем теорему «это возвращает сортированные списки». Это самая старая форма спецификации, но так по-прежнему работают Isabelle и ACL2 (ML изобрели специально для помощи в написании таких спецификаций).
  2. Второй внедряет спецификации в код в виде пред- и постусловий, утверждений и инвариантов. К функции можно добавить постусловие, что «возвращаемое значение является отсортированным списком». Спецификации на основе утверждений первоначально формализовали как логику Хоара. Они впервые появились в языке программирования Euclid в начале 1970-х годов (неясно, кто первым их начал использовать: Euclid или SPV, но, насколько я знаю, Euclid раньше представили общественности). Этот стиль также называют контрактным программированием — самая популярная форма верификации в современной индустрии (здесь контракты используются как спецификации кода).
  3. Наконец, есть системы типов. По соответствию Карри — Ховарда любую математическую теорему или доказательство можно закодировать как зависимый тип. Мы определим тип «отсортированные списки» и объявим для функции тип [Int] -> Sorted [Int].

На Let's Prove Leftpad можно посмотреть, как это выглядит. HOL4 и Isabelle — хорошие примеры спецификаций «независимой теоремы», SPARK и Dafny — спецификаций «вложенного утверждения», а Coq и Agda — «зависимого типа».

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

Какие спецификации правильные?

Верификация проверяет, что код соответствует спецификации. Возникает вопрос: откуда мы знаем, что у нас правильная спецификация? Поиск правильной спецификации — одна из самых больших проблем в формальных методах. Это также одно из главных возражений против них. Но скептики подразумевают здесь не совсем то, что имеют в виду специалисты по формальным методам.

Если вы формально докажете, что ваш код сортирует список, а клиент на самом деле хочет Uber для супов (tm), вы просто потратили кучу времени. Когда посторонние спрашивают «Как ты получишь верные спецификации?», то обычно думают о валидации, то есть спецификациях, которые не соответствуют требованиям клиента. Мол, только быстрые итерации и короткие циклы обратной связи способны подтвердить ваши требования.

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

Мы думаем о наших требованиях в человеческих, а не математических терминах. Проблема с поиском правильной спецификации более фундаментальна: мы часто не знаем, что туда записать. Я могу объяснить человеку, показав кучу фотографий деревьев и птиц, но это лишь конкретные примеры, а не описание идеи. Если я говорю: «Программа должна отличать деревья от птиц», то о чём идёт речь? На самом деле, чтобы перевести это в формальную спецификацию, нужно формализовать человеческие концепции, а это серьезная проблема.

Здесь можно определить соответствующие спецификации, и эксперты делают это всё время. Не поймите меня неправильно. Вот почему многие из последних успехов верификации кода объясняются чётким отображением того, что мы хотим, в то, что мы можем выразить. Но написание соответствующих спецификаций — навык, который нужно развивать, также как навыки программирования. Спецификация для него: «Не допускать ошибок компиляции». Например, CompCert — формально верифицированный компилятор C.

Когда у вас есть спецификация, всё равно нужно доказать, что код ей соответствует. Но всё это не имеет отношения к верифицакии.

Доказательство спецификации

Первое в истории средство верификации кода — это метод в стиле Дейкстры «подумайте о том, почему это правда», который в основном предназначен для ALGOL. Например, я могу следующим образом «доказать» правильность сортировки методом вставки:

  1. Базовый вариант: если в пустой список добавить один элемент, это будет единственный элемент, поэтому он будет отсортирован.
  2. Если у нас есть отсортированный список с k элементами и добавить один элемент, то мы вставляем элемент так, чтобы он был после всех меньших чисел и перед всеми большими числами. Это означает, что список по-прежнему отсортирован.
  3. По индукции, сортировка методом вставки отсортирует весь список.

Очевидно, что в реальности доказательство будет выглядеть более строго, но это общая идея. Дейкстра и другие использовали такой стиль, чтобы доказать правильность множества алгоритмов, включая многие основы параллелизма. Это также стиль, с которым связаны слова Кнута: «Остерегайтесь ошибок в этом коде; я лишь доказал, что он правильный, но не запускал его». Можно легко испортить математическое доказательство так, что никто не заметит. По некоторым оценкам, примерно в 20% опубликованных математических доказательств присутствуют ошибки. У Питера Гуттманна есть отличное эссе о доказательствах работоспособности смехотворной программы, где тонны «проверенного» кода сразу падают, если их запустить.

Первая программа для доказательства теорем вышла в 1967 году. В то же время мы изучали способы автоматического доказательства математических теорем. Программист формулирует некие свойства кода, а затем создаёт проверяемое доказательство, что у кода есть эти свойства. В начале 1970-х такие программы начали использовать для проверки кода на Pascal, а в середине десятилетия появились специальные формальные языки. Первые программы для доказательства теорем просто помогали людям проверять доказательства, а более сложные инструменты могли самостоятельно доказать части теоремы.

Что приводит к следующей проблеме.

Доказательства трудно получить

Доказательства трудны, и это очень неприятная работа. Трудно «бросить программирование и уйти в цирк». Удивительно, но формальные доказательства кода часто более строгие, чем доказательства, которые пишут большинство математиков! Математика — очень творческая деятельность, где ответ на теорему действует только в том случае, если ты его покажешь. Творчество плохо сочетается с формализмом и компьютерами.

Любой математик сразу поймёт, что такое индукция, как она работает вообще и как действует в данном случае. Возьмём тот же пример с сортировкой методом вставки, где мы применили индукцию. То же самое с доказательством от противного, доказательством через контрапозицию и т. д. Но в программе для доказательства теорем нужно всё строго формализовать. Например, что a + (b + c) = (a + b) + c. Кроме того, нужно формализовать все предположения, даже такие, где большинство математиков не утруждают себя доказательствами. Вы либо должны доказать это (трудно), либо декларировать это как истину по ассоциативному закону сложения (опасно), либо купить библиотеку теорем у того, кто уже смог это доказать (дорого). Программа для проверки теорем априори не знает, что это правда. Одна из первых широко распространённых программ SPADE преподносила полную арифметическую библиотеку как главное достоинство. Ранние программы для доказательства теорем соревновались по количеству встроенных тактик доказательства и связанных библиотек теорем.

Можете поручить это программе или написать самостоятельно. Далее, нужно получить само доказательство. Для чрезвычайно узких случаев, таких как логика высказываний или проверка типов HM, оно «всего лишь» NP-полное. Обычно автоматическое определение доказательства неразрешимо. Это означает, что вам нужно хорошо знать: По сути мы сами пишем бóльшую часть доказательства, а компьютер проверяет его правильность.

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

Что ещё хуже, палки в колёса вставляет компьютерная специфика. Помните, я говорил, что опасно предполагать ассоциативный закон сложения? Некоторые языки его не соблюдают. Например, в C++ INT_MAX. ((-1) + INT_MAX) + 1 — это INT_MAX. -1 + (INT_MAX + 1), что неопределяемо. Если предположить ассоциативное сложение в C++, то ваше доказательство окажется неверным, а код будет сломан. Нужно или избегать этого утверждения, или доказать, что для вашего конкретного фрагмента никогда не возникнет переполнение.

Но в большинстве языков есть конкретные функции, которые мешают доказательствам. Вы можете сказать, что неопределённое сложение — это ошибка, а нужно использовать язык с несвязанными целыми числами. Возьмите следующий код:

a = true;
b = false;
f(a);
assert a;

Это всегда так? Не факт. Может, f изменит a. Может, его изменит параллельный поток. Возможно, b присвоен алиас a, так что его изменение тоже изменит a (примечание: алиасы настолько мешают написанию доказательств, что Джону К. Рейнольдсу пришлось создать совершенно новую логику разделения, чтобы справиться с этой проблемой). Если что-то такое возможно в вашем языке, то следует явно доказать, что здесь такого не происходит. Тут поможет чистый код, в другом случае он может разрушить доказательство, поскольку заставляет использовать рекурсию и функции более высокого порядка. Кстати, и то, и другое является основой для написания хороших функциональных программ. Что хорошо для программирования — плохо для доказательства! (Примечание: в этой лекции Эдмунд Кларк перечислил некоторые сложные для проверки свойства: «плавающие запятые, строки, определяемые пользователем типы, процедуры, параллелизм, универсальные шаблоны, хранилище, библиотеки...»).

Но чем менее выразителен язык, тем сложнее на нём писать. У формальных верификаторов возникает дилемма: чем выразительнее язык, тем труднее на нём что-то доказать. И ничто из того, что мы обсуждали до сих пор, на самом деле не доказывает реальные программы, это лишь попытки подступиться к написанию доказательств. Первые рабочие формальные языки являлись очень ограниченными подмножествами более выразительных языков: ACL2 был подмножеством Lisp, Euclid был подмножеством Pascal и т. д.

Но становятся проще. Доказательства трудны. Помогает и технический прогресс: чем быстрее компьютеры — тем быстрее поиск. Исследователи в данной области добавляют новые эвристики, библиотеки теорем, предварительно проверенные компоненты и т. д.

Революция SMT

Одной из инноваций в середине 2000-х годов стало включение SMT-решателей в состав программ для доказательства теорем. В широком смысле, SMT-решатель может превратить (некоторые) математические теоремы в проблемы соблюдения ограничений. Это превращает творческую задачу в вычислительную. Возможно, вам всё ещё понадобится снабжать его промежуточными проблемами (леммами) как шаги в теореме, но это лучше, чем доказывать всё самостоятельно. Первые SMT-решатели появились примерно в 2004 году, сначала как академические проекты. Пару лет спустя Microsoft Research выпустила Z3, готовый SMT-решатель. Большим преимуществом Z3 было то, что он стал намного удобнее в использовании, чем другие SMT, которые, честно говоря, практически ничего не говорили. Microsoft Research использовала его внутри компании, чтобы помочь доказать свойства ядра Windows, поэтому они не ограничились минимальным UX.

Таким образом, люди могли работать на более выразительных языках, поскольку теперь проблемы выразительных заявлений стали решаться. SMT нанёс удар под дых FM-сообществу, потому что внезапно сделал тривиальными многие простые доказательства и позволил подступиться к очень сложным проблемам. Это невероятно быстрый темп: целых четыре целых строчки в день (примечание: предыдущий рекорд принадлежал seL4, разработчики которого писали по две строчки в день на С. Невероятный прогресс очевиден в проекте IronFleet: используя лучшие SMT-решатели и передовой язык верификации, Microsoft смогла написать 5000 строк проверенного кода Dafny всего за 3,7 человеко-лет!

Доказательства трудны.

Зачем это нужно?

Самое время отступить назад и спросить: «В чём смысл?» Мы пытаемся доказать, что какая-то программа соответствует какой-то спецификации. Корректность — это диапазон. Есть две части верификации: насколько объективно «правильна» ваша программа и насколько тщательно вы проверили правильность. Очевидно, что чем больше проверено, тем лучше, но проверка стоит времени и денег. Если у нас есть несколько ограничений (производительность, время выхода на рынок, стоимость и т. д.), полная проверка корректности не обязательно является оптимальным вариантом. Тогда возникает вопрос, какая минимальная проверка нам нужна и чего это стоит. В большинстве случаев вам достаточно, например, 90% или 95% или 99% корректности. Может, стоит потратить время на улучшение интерфейса, а не на проверку оставшегося 1%?

Вполне комфортно говорить, что кодовая база, которую мы хорошо протестировали и хорошо типизировали, в основном корректна кроме нескольких исправлений в продакшне, и мы даже пишем больше четырёх строчек кода в день. Тогда вопрос: «Действительно ли проверка 90/95/99% значительно дешевле, чем 100%?» Ответ «да». И это просто расширение тестов, не говоря уже о фаззинге, тестировании на основе свойств или тестировании модели. Фактически, подавляющее большинство сбоев в работе распределённых систем можно было бы предотвратить чуть более полным тестированием. Вы можете получить действительно выдающийся результат с этими простыми трюками без необходимости добиваться полного доказательства.

Всё равно гораздо легче перейти от 90% до 99%, чем от 99% до 100%. Что, если типизация и тесты не обеспечивают достаточной верификации? Ни доказательств, ни формальной проверки, ни даже модульного тестирования. Как упоминалось ранее, Cleanroom — это практика разработчиков, включающая всестороннюю документацию, тщательный анализ потока и обширный код-ревью. Программирование Cleanroom не замедляет темп разработки, и уж точно идёт быстрее, чем 4 строчки в день. Но правильно организованный Cleanroom уменьшает плотность дефектов до менее чем 1 бага на 1000 строк кода в продакшне (примечание: цифры из исследования Стэвли в работе Toward Zero-Defect Programming> но лучше всегда относитесь скептически и проверяйте первоисточники). Вам не нужна полная верификация, чтобы написать хороший софт или даже почти идеальный. И сам по себе Cleanroom — лишь один из многих методов разработки высоконадёжного ПО, которые находится посредине между обычной разработкой и верификацией кода. Есть случаи, когда она необходима, но для большинства отраслей это пустая трата денег.

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

Частичная верификация кода

Для повседневных задач слишком дорого делать полную проверку. Как насчёт частичной? Ведь можно получить пользу от доказательства некоторых свойств отдельных фрагментов кода. Вместо доказательства, что моя функция всегда правильно сортирует числа, я могу хотя бы доказать, что она не петляет вечно и никогда не выходит за пределы диапазона. Это тоже очень полезная информация. Так, даже самые простые доказательства для программ на C — отличный способ устранить огромную часть неопределённого поведения.

Большинство языков спроектированы или для полной верификации, или вообще её не поддерживают. Проблема в доступности. По этой причине большинство исследований по частичной верификации сосредоточено на нескольких высокоприоритетных языках, таких как C и Java. В первом случае вам не хватает многих хороших функций из более выразительных языков, а во втором случае нужен способ доказать вещи на языке, который враждебен самой концепции. Например, SPARK является ограниченным подмножеством Ada, поэтому вы можете писать критичный код на SPARK и взаимодействовать с менее критичным кодом Ada. Многие работают с ограниченными подмножествами языков. Но большинство этих языков довольно нишевые.

Используемые в продакшне системы типизации — распространённая разновидность: вы можете не знать, что tail всегда возвращает tail, но вы точно знаете, что его тип [a] -> [a]. Чаще определённые виды верификации встраивают в основную структуру языков. Они немного отличаются от SPARK и Frama-C тем, что способны выполнять только частичную проверку. Есть ещё такие примеры как Rust с доказанной безопасностью памяти и Pony с доказательством безопасности по исключениям. Возможно, именно поэтому такие языки, как Rust и Haskell, действительно подходят для использования на практике. И ещё их разрабатывают обычно эксперты по языкам программирования, а не эксперты по формальным методам: между двумя дисциплинами много общего, но они не идентичны.

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

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

Свойства проверить сложно, но вполне понятно, как это сделать. Для пример, возьмём процедуру с грубой спецификацией «если она вызывается, то делает системный вызов для сохранения данных в хранилище и обрабатывает системные ошибки». Нарушаются ли наши гарантии из-за некорректного ввода? Правильно ли сериализуются данные? Теперь сравните систему логов высокого уровня со спецификацией «все сообщения записываются в лог» и ответьте на такие вопросы: Обрабатываем ли мы все возможные способы сбоя системного вызова?

  • Записываются все сообщения или все сообщения, которые поступают в систему? Сообщения записываются один раз или гарантированно один раз?
  • Как отправляются сообщения? Это очередь? Канал доставляет их только один раз? Всё ли в порядке с доставкой?
  • Под записью в лог мы имеем в виду запись навсегда? Можно ли занести сообщение в лог, а потом удалить оттуда? Может ли оно «болтаться» между записанным и незаписанным состояниям, прежде чем будет записано окончательно?
  • Что делать, если сервер взорвётся в середине записи сообщения? Нужно ли журналирование?
  • Есть ли важные свойства носителя? Выходит ли факт «носитель потерял данные» за рамки наших требований или нет?
  • Что насчёт GDPR?
  • и так далее и тому подобное.

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

Языки спецификаций обычно ориентированы на спецификации дизайна, а не спецификации кода, хотя некоторые языки можно использовать для обоих случаев (примечание: процесс сопоставления спецификаций дизайна со спецификациями кода называется уточнением).В дальнейшем я буду называть языки спецификаций языками дизайна (DL), чтобы свести к минимуму путаницу (опять же, это не распространённая терминология; большинство людей используют «язык спецификаций», но я хочу четко разграничить спецификации кода и спецификации дизайна). Так же, как мы используем языки программирования для представления кода, мы используем языки спецификаций для представления проектов.

С тех пор мы видели огромное разнообразие различных языков спецификаций. Вероятно, первым полным DL стал VDM примерно в 1972 году. Грубо говоря, люди изобрели DL как средство достижения цели, а CVL — как саму цель. Пространство DL гораздо более разнообразно и фрагментировано, чем у языков верификации кода (CVL). Вот очень, очень краткий обзор некоторых первых DL: Поскольку на них сильно влияют конкретные проблемные области, в DL реализованы всевозможные идеи и семантика.

Язык

Область моделирования

Средство

Z

бизнес-требования

реляционная алгебра

Promela

сообщения

CSP

SDL

телекоммуникации

блок-схемы

Диаграммы состояний Харела

контроллеры

автоматы

Таблицы принятия решений

решения

таблицы

Поскольку DL обычно создаются для решения конкретных проблем, большинство из них имеют по крайней мере два или три реальных применения. Как правило, результаты очень положительные. Практикующие специалисты говорят, что DL даёт понимание проблем и облегчает поиск решений. Долгое время главным чемпионом был Praxis (теперь Altran), который применял «исправления-по-конструкции» — комбинацию Z-конструкций и кода SPARK — для создания критических систем безопасности. Спецификации экономят время и деньги, потому что вы не обнаружите ошибки дизайна на поздней стадии проекта.

AWS начала находить 35-шаговые критические ошибки, написав спецификации TLA+. Памела Зейв экспериментировала с Alloy и обнаружила фундаментальный баг в Chord, одной из основных распределённых хэш-таблиц. По моему опыту, когда люди пытаются писать спецификации, они очень скоро становятся большими поклонниками этого дела.

Для поклонников самым большим преимуществом является то, что сам процесс написания дизайна заставляет вас понять, что вы пишете. Но поклонники формальных методов и люди со стороны совершенно по-разному оценивают ценность написания спецификаций. Это совершенно не могут понять посторонние. Когда вам нужно формально выразить то, что делает ваша система, то множество неявных ошибок внезапно становятся болезненно очевидными. Если хотите дать кому-то попробовать DL, у человека должен быть способ проверить, что дизайн действительно обладает свойствами, которые он хочет.

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

Проверка моделей

Как и в случае с кодом, мы можем проверить дизайн, написав теоремы. К счастью, у нас есть ещё один трюк: можно использовать программу проверки моделей (model checker). Вместо составления доказательства, что дизайн правильный, мы просто брутфорсим пространство возможных состояний и смотрим, существует ли в нём неправильное состояние. Если ничего не найдём, то всё в порядке (примечание: программы проверки модели также используются для верификации кода, как JMBC, но в верификации дизайна намного чаще используется проверка модели, чем верификация кода).

Во-первых, не нужно писать доказательства, что экономит много времени и усилий. У проверки моделей масса преимуществ. В-третьих, если дизайн сломан, проверка модели даст явный контрпример. Во-вторых, не нужно учиться писать доказательства, поэтому барьер входа намного ниже. Попробуйте найти это самостоятельно. Это гораздо, гораздо упрощает исправление ошибки, особенно если для её воспроизведения нужно 35 шагов.

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

Представьте, что у вас три процесса, каждый из которых состоит из четырёх последовательных шагов, и они могут чередовать шаги любым способом. Другой большой недостаток — взрыв в пространстве состояний (state-space explosion). / (4!)^3 = 34 650 возможных исполнений (поведений). Если они не влияют на поведение друг друга, то получается (4*3)! И проверка моделей должна убедиться, что все они ведут себя хорошо. Если у каждого процесса одно из пяти начальных состояний, то общее число поведений возрастает до 4 300 000. Если они начнут это делать, пространство состояний станет расти ещё быстрее. И это при условии, что они не взаимодействуют друг с другом! Комбинаторный взрыв рассматривается как основная проблема для проверки моделей, и предстоит проделать много работы, чтобы решить эту задачу.

Самая большая проблема для проверки модели — «всего лишь» проблема производительности, а мы очень хорошо решаем проблемы производительности. Но в то же время есть ещё один способ справиться со взрывом пространства состояний: бросить на него больше оборудования. После оптимизации модели и проверки её с небольшими параметрами можно развернуть кластер AWS и запустить его с большими параметрами. Большинство (но не все) проверок моделей легко распараллеливаются.

Ещё больше специалистов по составлению спецификаций запускают проверку моделей, а когда она достигла предела своих возможностей, переключаются на менее интенсивные формы верификации. На практике многие спецификаторы используют проверку моделей, а затем по мере необходимости переходят к программам для доказательства теорем (примечание: имейте в виду, что «много спецификаторов» — это человек десять).

Проблема со спецификациями дизайна

Таким образом, верификация дизайна проще и быстрее, чем верификация кода, и продемонстрировала много впечатляющих успехов. Так почему люди ей не пользуются? Проблема с DV гораздо коварнее. Верификация кода — это техническая проблема, а верификация дизайна — проблема социальная: люди просто не видят смысла.

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

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

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

Но точно такие жалобы есть у каждого сообщества методологии, которое я знаю: сторонники TDD жалуются, что программисты не хотят пробовать TDD, Фанаты Haskell жалуются, что программисты не думают о статической типизации и так далее.

Может быть. Я слышал аргумент, что Agile не приемлет заранее продуманный дизайн, поэтому никто не хочет делать формальную спецификацию. Ещё один аргумент заключается в том, что исторически формальные методы постоянно переоценивались и не выполняли обещанное. Но многие из тех, кого я встречал, отвергают и Agile, и FM. Это тоже возможно, но большинство людей даже не слышали о формальных методах, а уж тем более об их истории.

Просто очень трудно заставить людей волноваться о том, чего они ещё не делают, даже если признают преимущества.

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

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

По крайней мере, это лучшее объяснение, чем обычный аргумент «веб — это же не самолёт». Надеюсь, эта статья чуть лучше объясняет, почему формальные методы так редко используются. Не стесняйтесь кричать, если увидите какие-то очевидные ошибки.

Теги
Показать больше

Похожие статьи

Добавить комментарий

Ваш e-mail не будет опубликован. Обязательные поля помечены *

Кнопка «Наверх»
Закрыть