На Software Engineering Stack Exchange я увидел такой вопрос: «Что мешает широкому внедрению формальных методов?» Вопрос был закрыт как предвзятый, а большинство ответов представляли собой комментарии типа «Слишком дорого!!!» или «Сайт — это не самолёт!!!» В каком-то смысле это верно, но мало что объясняет. Я написал эту статью, чтобы дать более широкую историческую картину формальных методов (FM), почему они на самом деле не используются и что мы делаем для исправления ситуации.
Прежде чем начать, нужно сформулировать некоторые условия. На самом деле существует не так много формальных методов: всего несколько крошечных групп. Это означает, что разные группы по-разному применяют термины. В широком смысле есть две группы формальных методов: формальная спецификация изучает запись точных, однозначных спецификаций, а формальная проверка — методы доказательства. Сюда входят и код, и абстрактные системы. Мало того, что мы используем разные термины для кода и систем, мы часто используем разные инструменты для их верификации. Чтобы ещё больше всё запутать, если кто-то говорит, что создаёт формальную спецификацию, обычно это означает и верификацию дизайна. А если кто-то говорит, что делает формальную верификацию, обычно это относится к верификации кода.
Для ясности разделим проверку на верификацию кода (CV) и верификацию дизайна (DV) и таким же образом разделим спецификации на CS и DS. Такие термины обычно не используются в широком сообществе FM. Начнем с CS и CV, затем перейдём к DS и DV.
Кроме того, возможна частичная верификация, где проверяется только подмножество спецификации, или полная верификация. Это может быть разница между доказательствами утверждений «система никогда не выходит из строя и не принимает неправильный пароль» или «система никогда не выходит из строя и блокирует учётную запись, если трижды ввести неправильный пароль». В основном, будем предполагать, что мы делаем полную проверку.
Также следует уточнить тип программного обеспечения, которое мы формализуем. Большинство людей неявно выделяют высоконадёжные программы, такие как медицинские устройства и самолёты. Люди предполагают, что для них формальные методы широко используются, а для остального не нужны. Это слишком оптимистичный взгляд: в большинстве высоконадёжного ПО не используются формальные методы. Вместо этого мы сосредоточимся на «обычном» софте.
Наконец, дисклеймер: я не профессиональный историк, и хотя пытался тщательно проверить информацию, в статье могут быть ошибки. Кроме того, я специализируюсь на формальной спецификации (DS и DV), поэтому больше вероятность ошибки там, где я говорю о верификации кода. Если увидите, пишите мне, я исправлю (и ещё: я зарабатываю на проведении семинаров по TLA+ и Alloy, поэтому очень предвзято отношусь к этим языкам; я пытаюсь быть максимально объективным, но сами понимаете: предвзятость — это предвзятость).
Формальное программирование
Получение спецификации
Прежде чем доказать корректность кода, нужно получить эталон истины. Это означает некую спецификацию, что должен делать код. Мы должны точно знать, что результат соответствует спецификации. Недостаточно сказать, что список «отсортирован»: мы не знаем, что сортируем, какие критерии используем и даже что мы подразумеваем под «сортировкой». Вместо этого можно сказать: «Список целых чисел l отсортирован в порядке возрастания для любых двух индексов i и j, если i < j, то l[i] <= l[j]».
Спецификации кода делятся на три основных вида:
- Первый — написание независимых от кода операторов. Напишем нашу функцию сортировки, а в отдельном файле напишем теорему «это возвращает сортированные списки». Это самая старая форма спецификации, но так по-прежнему работают Isabelle и ACL2 (ML изобрели специально для помощи в написании таких спецификаций).
- Второй внедряет спецификации в код в виде пред- и постусловий, утверждений и инвариантов. К функции можно добавить постусловие, что «возвращаемое значение является отсортированным списком». Спецификации на основе утверждений первоначально формализовали как логику Хоара. Они впервые появились в языке программирования Euclid в начале 1970-х годов (неясно, кто первым их начал использовать: Euclid или SPV, но, насколько я знаю, Euclid раньше представили общественности). Этот стиль также называют контрактным программированием — самая популярная форма верификации в современной индустрии (здесь контракты используются как спецификации кода).
- Наконец, есть системы типов. По соответствию Карри — Ховарда любую математическую теорему или доказательство можно закодировать как зависимый тип. Мы определим тип «отсортированные списки» и объявим для функции тип
[Int] -> Sorted [Int].
На Let's Prove Leftpad можно посмотреть, как это выглядит. HOL4 и Isabelle — хорошие примеры спецификаций «независимой теоремы», SPARK и Dafny — спецификаций «вложенного утверждения», а Coq и Agda — «зависимого типа».
Если присмотреться, то эти три формы спецификации кода сопоставляются с тремя основными областями автоматической проверки корректности: тестами, контрактами и типами. Это не совпадение. Корректность — это широкий диапазон, а формальная верификация — одна из его крайностей. По мере уменьшения строгости (и усилий) верификации мы получаем более простые и узкие проверки, будь то ограничение исследуемого пространства состояний, использование более слабых типов или принудительную проверку во время выполнения. Тогда любое средство полной спецификации превращается в средство частичной спецификации, и наоборот: многие считают Cleanroom техникой формальной верификации, где код-ревью выходит далеко за рамки человеческих возможностей.
Какие спецификации правильные?
Верификация проверяет, что код соответствует спецификации. Возникает вопрос: откуда мы знаем, что у нас правильная спецификация? Поиск правильной спецификации — одна из самых больших проблем в формальных методах. Это также одно из главных возражений против них. Но скептики подразумевают здесь не совсем то, что имеют в виду специалисты по формальным методам.
Когда посторонние спрашивают «Как ты получишь верные спецификации?», то обычно думают о валидации, то есть спецификациях, которые не соответствуют требованиям клиента. Если вы формально докажете, что ваш код сортирует список, а клиент на самом деле хочет Uber для супов (tm), вы просто потратили кучу времени. Мол, только быстрые итерации и короткие циклы обратной связи способны подтвердить ваши требования.
Это правда, что верификация кода не валидирует его. Но с этим аргументом есть две проблемы. Первая заключается в том, что этап применения формальных методов просто переносится, но не исчезает полностью. После всех этих быстрых итераций, вероятно, вы уже имеете представление, чего хочет клиент. И тогда начинаете верификацию кода. Во-вторых, хотя мы не знаем, чего именно хочет клиент, но можем предположить, чего он точно не хочет. Например, чтобы программное обеспечение случайно падало. Им не нужны дыры в безопасности. С этим все согласны: в конце концов, никто не говорит, что нужно пропустить модульные тесты во время итераций. Так что хотя бы убедитесь, что ваша система контроля версий не удаляет случайные данные пользователя (примечание: не думайте, что я озлоблен или что-то в этом роде).
Проблема с поиском правильной спецификации более фундаментальна: мы часто не знаем, что туда записать. Мы думаем о наших требованиях в человеческих, а не математических терминах. Если я говорю: «Программа должна отличать деревья от птиц», то о чём идёт речь? Я могу объяснить человеку, показав кучу фотографий деревьев и птиц, но это лишь конкретные примеры, а не описание идеи. На самом деле, чтобы перевести это в формальную спецификацию, нужно формализовать человеческие концепции, а это серьезная проблема.
Не поймите меня неправильно. Здесь можно определить соответствующие спецификации, и эксперты делают это всё время. Но написание соответствующих спецификаций — навык, который нужно развивать, также как навыки программирования. Вот почему многие из последних успехов верификации кода объясняются чётким отображением того, что мы хотим, в то, что мы можем выразить. Например, CompCert — формально верифицированный компилятор C. Спецификация для него: «Не допускать ошибок компиляции».
Но всё это не имеет отношения к верифицакии. Когда у вас есть спецификация, всё равно нужно доказать, что код ей соответствует.
Доказательство спецификации
Первое в истории средство верификации кода — это метод в стиле Дейкстры «подумайте о том, почему это правда», который в основном предназначен для ALGOL. Например, я могу следующим образом «доказать» правильность сортировки методом вставки:
- Базовый вариант: если в пустой список добавить один элемент, это будет единственный элемент, поэтому он будет отсортирован.
- Если у нас есть отсортированный список с k элементами и добавить один элемент, то мы вставляем элемент так, чтобы он был после всех меньших чисел и перед всеми большими числами. Это означает, что список по-прежнему отсортирован.
- По индукции, сортировка методом вставки отсортирует весь список.
Очевидно, что в реальности доказательство будет выглядеть более строго, но это общая идея. Дейкстра и другие использовали такой стиль, чтобы доказать правильность множества алгоритмов, включая многие основы параллелизма. Это также стиль, с которым связаны слова Кнута: «Остерегайтесь ошибок в этом коде; я лишь доказал, что он правильный, но не запускал его». Можно легко испортить математическое доказательство так, что никто не заметит. По некоторым оценкам, примерно в 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-сообществу, потому что внезапно сделал тривиальными многие простые доказательства и позволил подступиться к очень сложным проблемам. Таким образом, люди могли работать на более выразительных языках, поскольку теперь проблемы выразительных заявлений стали решаться. Невероятный прогресс очевиден в проекте IronFleet: используя лучшие SMT-решатели и передовой язык верификации, Microsoft смогла написать 5000 строк проверенного кода Dafny всего за 3,7 человеко-лет! Это невероятно быстрый темп: целых четыре целых строчки в день (примечание: предыдущий рекорд принадлежал seL4, разработчики которого писали по две строчки в день на С.
Доказательства трудны.
Зачем это нужно?
Самое время отступить назад и спросить: «В чём смысл?» Мы пытаемся доказать, что какая-то программа соответствует какой-то спецификации. Корректность — это диапазон. Есть две части верификации: насколько объективно «правильна» ваша программа и насколько тщательно вы проверили правильность. Очевидно, что чем больше проверено, тем лучше, но проверка стоит времени и денег. Если у нас есть несколько ограничений (производительность, время выхода на рынок, стоимость и т. д.), полная проверка корректности не обязательно является оптимальным вариантом. Тогда возникает вопрос, какая минимальная проверка нам нужна и чего это стоит. В большинстве случаев вам достаточно, например, 90% или 95% или 99% корректности. Может, стоит потратить время на улучшение интерфейса, а не на проверку оставшегося 1%?
Тогда вопрос: «Действительно ли проверка 90/95/99% значительно дешевле, чем 100%?» Ответ «да». Вполне комфортно говорить, что кодовая база, которую мы хорошо протестировали и хорошо типизировали, в основном корректна кроме нескольких исправлений в продакшне, и мы даже пишем больше четырёх строчек кода в день. Фактически, подавляющее большинство сбоев в работе распределённых систем можно было бы предотвратить чуть более полным тестированием. И это просто расширение тестов, не говоря уже о фаззинге, тестировании на основе свойств или тестировании модели. Вы можете получить действительно выдающийся результат с этими простыми трюками без необходимости добиваться полного доказательства.
Что, если типизация и тесты не обеспечивают достаточной верификации? Всё равно гораздо легче перейти от 90% до 99%, чем от 99% до 100%. Как упоминалось ранее, Cleanroom — это практика разработчиков, включающая всестороннюю документацию, тщательный анализ потока и обширный код-ревью. Ни доказательств, ни формальной проверки, ни даже модульного тестирования. Но правильно организованный Cleanroom уменьшает плотность дефектов до менее чем 1 бага на 1000 строк кода в продакшне (примечание: цифры из исследования Стэвли в работе Toward Zero-Defect Programming> но лучше всегда относитесь скептически и проверяйте первоисточники). Программирование Cleanroom не замедляет темп разработки, и уж точно идёт быстрее, чем 4 строчки в день. И сам по себе Cleanroom — лишь один из многих методов разработки высоконадёжного ПО, которые находится посредине между обычной разработкой и верификацией кода. Вам не нужна полная верификация, чтобы написать хороший софт или даже почти идеальный. Есть случаи, когда она необходима, но для большинства отраслей это пустая трата денег.
Однако это не означает, что формальные методы в целом неэкономичны. Многие вышеупомянутые высоконадёжные методы основаны на написании спецификаций кода, которые вы формально не доказываете. Что касается верификации, в отрасли с выгодой используют два общих способа. Во-первых, верификация дизайна вместо кода, что мы рассмотрим позже. Во-вторых, частичная верификация кода, которую мы рассмотрим сейчас.
Частичная верификация кода
Для повседневных задач слишком дорого делать полную проверку. Как насчёт частичной? Ведь можно получить пользу от доказательства некоторых свойств отдельных фрагментов кода. Вместо доказательства, что моя функция всегда правильно сортирует числа, я могу хотя бы доказать, что она не петляет вечно и никогда не выходит за пределы диапазона. Это тоже очень полезная информация. Так, даже самые простые доказательства для программ на C — отличный способ устранить огромную часть неопределённого поведения.
Проблема в доступности. Большинство языков спроектированы или для полной верификации, или вообще её не поддерживают. В первом случае вам не хватает многих хороших функций из более выразительных языков, а во втором случае нужен способ доказать вещи на языке, который враждебен самой концепции. По этой причине большинство исследований по частичной верификации сосредоточено на нескольких высокоприоритетных языках, таких как C и Java. Многие работают с ограниченными подмножествами языков. Например, SPARK является ограниченным подмножеством Ada, поэтому вы можете писать критичный код на SPARK и взаимодействовать с менее критичным кодом Ada. Но большинство этих языков довольно нишевые.
Чаще определённые виды верификации встраивают в основную структуру языков. Используемые в продакшне системы типизации — распространённая разновидность: вы можете не знать, что tail всегда возвращает tail, но вы точно знаете, что его тип [a] -> [a]. Есть ещё такие примеры как Rust с доказанной безопасностью памяти и Pony с доказательством безопасности по исключениям. Они немного отличаются от SPARK и Frama-C тем, что способны выполнять только частичную проверку. И ещё их разрабатывают обычно эксперты по языкам программирования, а не эксперты по формальным методам: между двумя дисциплинами много общего, но они не идентичны. Возможно, именно поэтому такие языки, как Rust и Haskell, действительно подходят для использования на практике.
Спецификация дизайна
До сих пор мы говорили только о верификации кода. Однако у формальных методов есть ещё одна сторона, которая более абстрактна и верифицирует сам дизайн, архитектуру проекта. Это настолько глубокий анализ, что является синонимом формальной спецификации: если кто-то говорит, что выполняет формальную спецификацию, скорее всего, это означает, что он определяет и верифицирует дизайн.
Как мы уже говорили, доказать все строчки кода очень, очень сложно. Но многие проблемы в продакшне возникают не из-за кода, а из-за взаимодействия компонентов системы. Если отмахнуться от деталей реализации, например, принять как данность, что система способна распознавать птиц, то нам будет проще анализировать, как деревья и птицы в качестве модулей высокого уровня вписываются в общий дизайн. В таком масштабе становится намного проще описать вещи, которые вы не смогли бы реализовать, например, среду выполнения, человеческие взаимодействия или беспощадный поток времени. В этом масштабе мы формализуем свои намерения с помощью общей системы, а не строк кода. Это гораздо ближе к человеческому уровню, где проекты и требования могут быть гораздо более неоднозначными, чем на уровне кода.
Для пример, возьмём процедуру с грубой спецификацией «если она вызывается, то делает системный вызов для сохранения данных в хранилище и обрабатывает системные ошибки». Свойства проверить сложно, но вполне понятно, как это сделать. Правильно ли сериализуются данные? Нарушаются ли наши гарантии из-за некорректного ввода? Обрабатываем ли мы все возможные способы сбоя системного вызова? Теперь сравните систему логов высокого уровня со спецификацией «все сообщения записываются в лог» и ответьте на такие вопросы:
- Записываются все сообщения или все сообщения, которые поступают в систему? Сообщения записываются один раз или гарантированно один раз?
- Как отправляются сообщения? Это очередь? Канал доставляет их только один раз? Всё ли в порядке с доставкой?
- Под записью в лог мы имеем в виду запись навсегда? Можно ли занести сообщение в лог, а потом удалить оттуда? Может ли оно «болтаться» между записанным и незаписанным состояниям, прежде чем будет записано окончательно?
- Что делать, если сервер взорвётся в середине записи сообщения? Нужно ли журналирование?
- Есть ли важные свойства носителя? Выходит ли факт «носитель потерял данные» за рамки наших требований или нет?
- Что насчёт GDPR?
- и так далее и тому подобное.
Без формального дизайна сложнее выразить действительно нужные требования для системы. Если вы не можете их выразить, то понятия не имеете, действительно ли дизайн соответствует требованиям или просто выглядит похоже на них, но может привести к непредсказуемым последствиям. Более формально выражая намерения и дизайн, мы можем легко проверить, что на самом деле разрабатываем то, что нужно.
Так же, как мы используем языки программирования для представления кода, мы используем языки спецификаций для представления проектов. Языки спецификаций обычно ориентированы на спецификации дизайна, а не спецификации кода, хотя некоторые языки можно использовать для обоих случаев (примечание: процесс сопоставления спецификаций дизайна со спецификациями кода называется уточнением).В дальнейшем я буду называть языки спецификаций языками дизайна (DL), чтобы свести к минимуму путаницу (опять же, это не распространённая терминология; большинство людей используют «язык спецификаций», но я хочу четко разграничить спецификации кода и спецификации дизайна).
Вероятно, первым полным DL стал VDM примерно в 1972 году. С тех пор мы видели огромное разнообразие различных языков спецификаций. Пространство DL гораздо более разнообразно и фрагментировано, чем у языков верификации кода (CVL). Грубо говоря, люди изобрели DL как средство достижения цели, а CVL — как саму цель. Поскольку на них сильно влияют конкретные проблемные области, в DL реализованы всевозможные идеи и семантика. Вот очень, очень краткий обзор некоторых первых DL:
| Язык | Область моделирования | Средство |
|---|---|---|
| Z | бизнес-требования | реляционная алгебра |
| Promela | сообщения | CSP |
| SDL | телекоммуникации | блок-схемы |
| Диаграммы состояний Харела | контроллеры | автоматы |
| Таблицы принятия решений | решения | таблицы |
Поскольку DL обычно создаются для решения конкретных проблем, большинство из них имеют по крайней мере два или три реальных применения. Как правило, результаты очень положительные. Практикующие специалисты говорят, что DL даёт понимание проблем и облегчает поиск решений. Долгое время главным чемпионом был Praxis (теперь Altran), который применял «исправления-по-конструкции» — комбинацию Z-конструкций и кода SPARK — для создания критических систем безопасности. Спецификации экономят время и деньги, потому что вы не обнаружите ошибки дизайна на поздней стадии проекта.
Памела Зейв экспериментировала с Alloy и обнаружила фундаментальный баг в Chord, одной из основных распределённых хэш-таблиц. AWS начала находить 35-шаговые критические ошибки, написав спецификации TLA+. По моему опыту, когда люди пытаются писать спецификации, они очень скоро становятся большими поклонниками этого дела.
Но поклонники формальных методов и люди со стороны совершенно по-разному оценивают ценность написания спецификаций. Для поклонников самым большим преимуществом является то, что сам процесс написания дизайна заставляет вас понять, что вы пишете. Когда вам нужно формально выразить то, что делает ваша система, то множество неявных ошибок внезапно становятся болезненно очевидными. Это совершенно не могут понять посторонние. Если хотите дать кому-то попробовать DL, у человека должен быть способ проверить, что дизайн действительно обладает свойствами, которые он хочет.
К счастью, это также чрезвычайно важно для многих спецификаторов, поэтому верификация дизайна — большая область исследований.
Проверка моделей
Как и в случае с кодом, мы можем проверить дизайн, написав теоремы. К счастью, у нас есть ещё один трюк: можно использовать программу проверки моделей (model checker). Вместо составления доказательства, что дизайн правильный, мы просто брутфорсим пространство возможных состояний и смотрим, существует ли в нём неправильное состояние. Если ничего не найдём, то всё в порядке (примечание: программы проверки модели также используются для верификации кода, как JMBC, но в верификации дизайна намного чаще используется проверка модели, чем верификация кода).
У проверки моделей масса преимуществ. Во-первых, не нужно писать доказательства, что экономит много времени и усилий. Во-вторых, не нужно учиться писать доказательства, поэтому барьер входа намного ниже. В-третьих, если дизайн сломан, проверка модели даст явный контрпример. Это гораздо, гораздо упрощает исправление ошибки, особенно если для её воспроизведения нужно 35 шагов. Попробуйте найти это самостоятельно.
Есть и пара недостатков. Во-первых, эти инструменты не такие мощные. В частности, вы можете столкнуться с беспредельной (unbounded) моделью, у которой бесконечное количество разных состояний. Например, вы определяете обработчик очереди сообщений: он нормально работает со списком из десяти сообщений. Но если нужно поверить его на любом списке… ну, их бесконечное количество, поэтому в модели бесконечное количество состояний. У большинства инструментов для проверки моделей есть различные приёмы для подобных ситуаций, такие как определение классов эквивалентности или симметрии, но каждый случай отличается.
Другой большой недостаток — взрыв в пространстве состояний (state-space explosion). Представьте, что у вас три процесса, каждый из которых состоит из четырёх последовательных шагов, и они могут чередовать шаги любым способом. Если они не влияют на поведение друг друга, то получается (4*3)! / (4!)^3 = 34 650 возможных исполнений (поведений). Если у каждого процесса одно из пяти начальных состояний, то общее число поведений возрастает до 4 300 000. И проверка моделей должна убедиться, что все они ведут себя хорошо. И это при условии, что они не взаимодействуют друг с другом! Если они начнут это делать, пространство состояний станет расти ещё быстрее. Комбинаторный взрыв рассматривается как основная проблема для проверки моделей, и предстоит проделать много работы, чтобы решить эту задачу.
Но в то же время есть ещё один способ справиться со взрывом пространства состояний: бросить на него больше оборудования. Самая большая проблема для проверки модели — «всего лишь» проблема производительности, а мы очень хорошо решаем проблемы производительности. Большинство (но не все) проверок моделей легко распараллеливаются. После оптимизации модели и проверки её с небольшими параметрами можно развернуть кластер AWS и запустить его с большими параметрами.
На практике многие спецификаторы используют проверку моделей, а затем по мере необходимости переходят к программам для доказательства теорем (примечание: имейте в виду, что «много спецификаторов» — это человек десять). Ещё больше специалистов по составлению спецификаций запускают проверку моделей, а когда она достигла предела своих возможностей, переключаются на менее интенсивные формы верификации.
Проблема со спецификациями дизайна
Таким образом, верификация дизайна проще и быстрее, чем верификация кода, и продемонстрировала много впечатляющих успехов. Так почему люди ей не пользуются? Проблема с DV гораздо коварнее. Верификация кода — это техническая проблема, а верификация дизайна — проблема социальная: люди просто не видят смысла.
Во многом это следствие того, что дизайн — это не код. В большинстве DL не существует автоматического способа создания кода, а также способа взять существующий код и проверить его на соответствие дизайну (примечание: генерация кода из спецификаций называется синтезом; для ориентировки см. работы Нади Поликарповой; доказательство, что код соответствует спецификации (или спецификации соответствует другой спецификации) называется уточнением: по обоим направлениям идут активные исследования).
Программисты склонны не доверять артефактам программного обеспечения, которые не являются кодом или принудительно не синхронизированы с кодом. По этой же причине часто игнорируются документация, комментарии, диаграммы, вики и сообщения в коммитах.
Похоже, программисты просто не верят, что от спецификаций есть какая-то польза. По моему опыту, они предполагают, что текущих инструментов (псевдокод, диаграммы, TDD) более чем достаточно для правильного проектирования. Я не знаю, насколько распространённым является это мнение и не могу его объяснить ничем, кроме общего консерватизма.
Но точно такие жалобы есть у каждого сообщества методологии, которое я знаю: сторонники TDD жалуются, что программисты не хотят пробовать TDD, Фанаты Haskell жалуются, что программисты не думают о статической типизации и так далее.
Я слышал аргумент, что Agile не приемлет заранее продуманный дизайн, поэтому никто не хочет делать формальную спецификацию. Может быть. Но многие из тех, кого я встречал, отвергают и Agile, и FM. Ещё один аргумент заключается в том, что исторически формальные методы постоянно переоценивались и не выполняли обещанное. Это тоже возможно, но большинство людей даже не слышали о формальных методах, а уж тем более об их истории.
Просто очень трудно заставить людей волноваться о том, чего они ещё не делают, даже если признают преимущества.
Резюме
Верификация кода — трудная задача. В это вовлекается всё больше людей, хотя программы для доказательства теорем и SMT-решатели становятся всё более сложными. Но всё-таки в обозримом будущем, наверное, это останется уделом специалистов.
Верификация дизайна намного проще, но для её использования требуется преодолеть культурный барьер. Думаю, ситуацию можно изменить. Двадцать лет назад автоматизированное тестирование и код-ревью были довольно экзотическими и нишевыми темами, но в конечном итоге стали мейнстримом. Опять же, контрактное программирование были нишевым и остаётся таковым.
Надеюсь, эта статья чуть лучше объясняет, почему формальные методы так редко используются. По крайней мере, это лучшее объяснение, чем обычный аргумент «веб — это же не самолёт». Не стесняйтесь кричать, если увидите какие-то очевидные ошибки.
Автор: m1rko
