Использование формальных методов в работе
Оригинал на английском языке - Using Formal Methods At Work.
Несколько человек сказали мне, что им понравилось изучать формальные методы, но они не знают, как начать их использовать на практике. В основном они работают короткими спринтами и не разрабатывают программные системы с нуля. Это говорит о том, что есть некоторая путаница в отношении того, что делает спецификации полезными, и что нужны рекомендации по их применению на практике. Это краткое руководство по использованию формальных спецификаций в работе, доступное для начинающих, которое может быть применимо в разных областях и может принести ценность для бизнеса.
Предположения
Я использую термин “формальные спецификации” для обозначения языков, с помощью которых вы можете выражать высокоуровневые свойства систем, но достаточно формализованных, чтобы вы могли машинно проверить их на соответствие. Сюда входят такие языки, как TLA+, Alloy и Event-B, и не входят такие инструменты как Coq, таблицы решений и Gherkin.
Предполагаем, что вы пишете “типичную” бизнес-систему или инфраструктурную систему, что бы это ни значило. Некоторое количество мелких ошибок допустимо, но крупных ошибок следует избегать. Это грубые эмпирические правила, которые следует учитывать при разработки ваших спецификаций. Разбейте их по мере необходимости.
Спецификации высокоуровневы
Рассмотрим компонент, который получает сообщение и что-то с ним делает. Если есть проблема с самим сообщением (плохо сформированное, неправильно доставленное, что угодно), то мы вместо этого делаем что-то другое. Если проверку ошибок, форматирование и аудит мы можем опустить, то описать мы это можем так:
pred handle_message {
do_good_thing or
do_error_thing
}
Этому соотвутствует “каждое сообщение хорошее”, “каждое сообщение плохое”, “первые десять сообщений плохие, а остальные хорошие” и т. д. Все эти пути допустимы в спецификации, точно так же, как все они могут встречаться в реальной системе. Когда я запускаю проверку модели, то все эти пути проверяются.
Спецификации неполны
Спецификации не обязательно должны описывать общее поведение системы. Если ваша система выполняет A, B и C, обычно гораздо быстрее написать три разные спецификации, каждая из которых предполагает, что два компонента работают правильно. Четвертая спецификация может показать, как взаимодействуют все три, но с меньшими подробностями о каждом компоненте, чем в специализированных спецификациях.
Это не дает вам такой подробной информации, как моделирование всего сразу, но такой подход имеет много преимуществ. Во-первых, каждая специализированная спецификация может быть сосредоточена на том, что вас интересует в этом компоненте. Во-вторых, вы можете использовать каждую специализированную спецификацию без необходимости проектирования всей системы; это полезно на ранних стадиях. В-третьих, такую модель проверить гораздо быстрее. В-четвертых, составить спецификации намного сложнее, чем написать независимые спецификации, и вам часто приходится “ослаблять” спецификацию, чтобы легко осуществить композицию.
Спецификации кратки
Следствие первых двух предположений. Спецификация высокого уровня может быть на порядок меньше фактического кода.
Спецификации неидеальны
Чем больше времени вы потратите на написание спецификации, тем более полной она будет. Но, как и во всем, есть минус. Требуется гораздо больше усилий, чтобы перейти от спецификации 95% системы к 99%, чем перейти от 85% к 95%. Я выбираю максимальный результат при минимальных затратах просто потому, что такой подход наиболее доступен и прагматичен для большинства людей. Спецификация при таком подходе не избавит ваше программное обеспечение от ошибок, но сделает его намного более качественным, чем полное отсутствие спецификаций.
Спецификации - это не код
Большинство языков формальных спецификаций не позволяют выполнять автоматическое уточнение модели: вы не можете легко проверить, соответствует ли ваш код спецификации. В некотором смысле это проблема, но есть также и удивительное преимущество: спецификация существует отдельно от вашего кода и не является его зависимостью. Это значит, что эксперименты со спецификациями, в отличие от экспериментов с новыми языками, не влекут за собой риска возникновения или увеличения технического долга. Также вам не нужно менять код, чтобы писать для него спецификации. Всё это помогает избежать трудностей при экспериментировании с формальными методами. Это сложнее, чем установить новый монитор, но проще, чем изучить Elixir или заставить своих коллег заняться парным программированием.
Спецификации - это не тесты
Существует два типа системных ошибок: ошибки реализации и ошибки проектирования. Тесты хороши для того, чтобы показать, что ваш код соответствует вашим ожиданиям, но очень плохи, чтобы показать, что ваши ожидания соответствуют вашим потребностям. Спецификации наоборот. Вам нужно и то и другое. Спецификации также не являются документацией, инспекцией кода, статическим анализом кода или пост-релизной аналитикой. Это может упростить их выполнение, но не исключает необходимость в них.
Есть случаи, когда спецификации могут избавить от необходимости в тестировании кода, но такие спецификации гораздо сложнее написать и они полезны в более специализированной области.
Подходы
Написание спецификации служит трём основным целям:
- Оно предоставляет чёткую документацию по системным требованиям, поведению и свойствам.
- Оно проясняет ваше понимание системы.
- Оно находит действительно тонкие, опасные ошибки.
(3) является наиболее уникальным преимуществом и, возможно, тем, что обеспечивает наиболее очевидную ценность для бизнеса. Но всё это очень ценно. Самые простые способы начать применять спецификации в основном дают вам (1) и (2). Поскольку люди не так сильно замечают эти преимущества, это заставляет их думать, что им нужно погрузиться в глубокую часть, чтобы получить хоть какую-то пользу от спецификаций.
Следующие проекты расположены в порядке возрастания усилий/навыков. Это приблизительное руководство, а не план урока: не чувствуйте себя обязанным выполнять их все как “упражнения” или что-то в этом роде. Вы можете использовать это, чтобы выяснить, с чего вам удобнее всего начинать и как вам удобнее прогрессировать. Это также не в порядке возрастания полезности. Даже документирование ваших собственных систем может быть очень полезным.
Документирование существующей системы
Возьмём систему, с которой вы работали какое-то время и которую, по вашему мнению, вы хорошо знаете. Напишите высокоуровневую спецификацию архитектуры или некоторых её функций. Не беспокойтесь о согласовании разных спецификаций, просто сделайте несвязные модели различных интересных вам частей. Вам не обязательно искать ошибки в архитектуре; цель состоит в том, чтобы получить практическую практику написания спецификации. Если ваша спецификация показывает поведение, которого вы не видите в существующей системе, обычно это признак того, что вы допустили ошибку при написании спецификации.
Как правило. Также возможно, что вы неправильно поняли какой-то аспект системы. Это полезно знать, но неопределенность (это ошибка перевода или ошибка понимания?) может быть не очень хороша для улучшения ваших навыков моделирования. Вот почему лучше документировать систему, которую хорошо знаете. Это позволяет практиковаться моделировании.
Также есть вероятность, что вы не допустили никаких ошибок, и на самом деле есть небольшая проблема с системой. Это случается гораздо чаще, чем вы ожидаете. Я бы сказал, что если вы только начинаете, то учитывайте такую вероятность, но не делайте это своим первым предположением.
Хотя при этом основное внимание уделяется изучению формальных методов, это всё же дает достаточно ощутимых преимуществ для бизнес-кейса. Во-первых, у вас есть спецификация вашей системы со строго сформулированными предположениями, поведением и требованиями. Я обнаружил, что это отличное дополнение к документации при объяснении чего-либо другим инженерам. Кроме того, если вам позже потребуется изменить систему, то у вас уже есть модель этой системы.
Демонстрация ошибки
Возьмём систему, в которой вы исправили сложную ошибку. Напишите модель, которая соответствует сломанной версии системы, и покажите, что она улавливает ту же ошибку. Это дает вам хорошую практику написания инвариантов. Это также помогает найти инварианты для существующей системы: какое самое слабое свойство нарушает ошибка?
Для этого есть и скрытая причина: это отлично подходит для демонстрации ценности написания спецификаций. Если у вас есть данные о том, как долго присутствовала ошибка и сколько времени потребовалось, чтобы найти ошибку, вы можете показать разницу во времени между “поиском этой ошибки в продакшене” и “поиском этой ошибки в модели”. Разница вполне может быть чем-то вроде “несколько недель” против получаса.
Поиск бага
Возьмите существующую систему с обнаруженной ошибкой и напишите модель с ошибкой. Это отличается от демонстрации ошибки тем, что у вас нет полной информации об ошибке, поскольку вы еще не локализовали и не исправили ее. Цель спецификации - облегчить поиск ошибки. Если вы сможете точно воспроизвести это в модели, она покажет вам серию шагов, ведущих к ошибке. Затем вы можете определить, где в спецификации что-то идет не так, и использовать это для локализации ошибки в самом коде.
Если вы не можете воспроизвести ошибку, это может быть связано с несколькими
распространенными причинами. Во-первых, спецификация может быть слишком
высокого уровня. Возможно, вы абстрагируете обработку ошибок как правильную, но
на самом деле вы пропустили случай ошибки. Во-вторых, ошибка может быть
ошибкой: вы ошиблись в некоторых деталях реализации. Подумайте о том, чтобы
написать merge(f, g) вместо merge(g, f), поместить две строки в неправильном
порядке и т. д. Все эти проблемы легко ускользают от спецификации. Спецификации
лучше воспроизводят ошибки из пробелов в дизайне или когда дизайн имеет
“правильное”, но непреднамеренное поведение.
Иногда вы найдете ошибку из-за проверки модели. Однако во многих случаях спецификация делает ошибку “очевидной”. Гораздо проще увидеть состояние гонки в 10 строках спецификации, чем в 1000 строк кода. Это приводит к распространенному разочарованию новичков формальными спецификациями, которые выявили ошибку до окончания проверки модели. На самом деле это одно из больших преимуществ спецификации: большая часть проверки модели может происходить в вашей голове.
Один пример, над которым я работал: почему не работал аварийный выключатель? После пары дней безрезультатных попыток отследить его, я написал спецификацию и сразу же сказал: “А, точно, аварийная кнопка не позволяла нам добавлять задания в очередь, а не обрабатывать их”. Это очевидно в спецификации и не так очевидно в коде.
Изучение незнакомой системы
Возьмите систему, которую хотите лучше понять, и напишите для неё модель. Ошибка в спецификации с гораздо большей вероятностью означает, что вы что-то неправильно поняли, чем неудачная спецификация, предназначенная для вашей собственной системы. Но написание спецификации сильно поможет ещё до того, как вы её проверите. Вы не можете написать всё что угодно в спецификации: всё, что вы пишете, должно быть точным и строгим. Это позволяет творить чудеса для понимания чего-то.
Кроме того, это хороший способ проверить корректность своих знаний. Вы можете увидеть что происходит, когда вы пропустите спецификацию через средство проверки модели и сравните его с поведением реальной системы. Вы также можете показать модель эксперту в предметной области и посмотреть, соответствует ли она его пониманию системы. Если оно не соответствует, то у вас есть точный способ узнать, где именно расходится ваше представление.
По моему опыту, вы также с большей вероятностью найдете критические ошибки, моделируя незнакомые системы, чем те, с которыми вы знакомы. Понятия не имею почему. Независимо от того, решите ли вы сообщить кому-то об ошибке, помните о том, что нужно быть уважительным и чутким. Точно так же, как спецификации не заменяют тесты, спецификации не заменяют социальные навыки.
Изменение существующей системы
Возьмите систему, модель этой системы и новое требование или желаемое изменение. Покажите, что она не удовлетворяет требованию, а затем модифицируйте модель до тех пор, пока она не будет удовлетворять.
По крайней мере, по моему опыту, это наиболее частое использование формальных методов в проекте. Поскольку спецификация является высокоуровневой, большинство изменений будут отображаться только в нескольких строках модифицированной спецификации. Прежде чем вносить изменения, убедитесь, что внесенные вами изменения действительно делают то, что вы хотите. Это поможет вам понять, что вы делаете. Это также очень помогает в поиске ошибок, показывая, как небольшое изменение в вашей системе распространяется на глобальное нарушение инварианта.
Ещё одно преимущество, которое вы получаете здесь: написание спецификации проверяет соответствие требованиям. Если я говорю “по крайней мере один узел всегда должен быть в сети”, имею ли я в виду “есть по крайней мере один узел, который находится в сети все время” или “в любой момент времени есть по крайней мере один узел в сети”? Намного легче увидеть разницу при написании спецификации, чем когда вы погрузились в написание кода. Иногда клиент сможет уточнить, что он имел в виду, а в редких случаях клиент поймет, что на самом деле не знает, чего хочет.
Разработка новой системы
Создайте новую систему с нуля, используя спецификации. В качестве альтернативы добавьте важную новую функцию в систему, используя спецификации. Это требует наибольшего мастерства как в написании спецификаций, так и в знании того, когда прекратить писать спецификации, но на самом деле это не намного сложнее, чем моделирование существующей системы. Это также имеет самые существенные преимущества, поскольку вы получаете все необходимые знания и проверку моделей с самого начала.
Распространенной ошибкой новичка является попытка слишком подробно смоделировать систему до того, как вы начнете её строить. Помните, что спецификация - это ваш дизайн. Невероятно ценно иметь дизайн, но это не код, и большая часть кода, который вы пишете, не будет отражена в дизайне. Для системы не важны конкретные классы или функции, которые у вас есть, важно только то, какое поведение они производят.
Вы можете заметить одну важную вещь: все они итеративны. Вы не тратите недели и месяцы на написание исчерпывающих спецификаций, прежде чем заняться кодированием. И вы не слепо следуете плану: если реальность вмешивается, вы корректируете спецификацию и смотрите, каковы будут последствия. Спецификация предназначена для того, чтобы усилить вашу способность продумывать дизайн, а не заставлять вас идти по жесткому пути.
Самый большой пробел здесь в том, что это всё индивидуально, а не командно. Промышленные формальные методы это всё ещё очень новая практика, поэтому у нас нет надёжной информации о том, как она вписывается в рабочий процесс более крупной команды. Есть несколько разных компаний, которые внедряют формальные методы более широко, и я рад видеть, как это работает у них.
Есть проекты, в которых исчерпывающая спецификация имеет смысл. Большинство из нас этим не занимается. Есть проекты, в которых спецификации вообще не имеют смысла. Большинство из нас тоже этого не делает. Мы находимся в той точке, где некоторая форма спецификации очень помогает, но подавляющее большинство из нас ее не использует.
Но частью правильного использования чего-то является знание того, когда это применимо. Поэтому, чтобы сделать спецификации полезными, мы также должны знать, когда они не являются таковыми.
Когда не нужно делать спецификации
Вам не нужно делать спецификации, когда оно того не стоит. Конечно, это замкнутый круг, нас больше интересует, почему не стоит писать спецификации. На самом деле у этого вопроса есть два аспекта: когда вообще не писать спецификации, и когда не стоит добавлять более низкоуровневые детали в существующую спецификацию. Оба аспекта подчиняются одним и тем же ограничениям.
Есть некоторые вещи, которые делают спецификации менее полезными. Спецификация может быть полезной, даже если она сохранится, но вы, вероятно, потратите на неё меньше времени и усилий. Кроме того, это связано с моим опытом работы со спецификациями: могут существовать языки, которые подходят для подобных задач.
Низкая стоимость ошибки
Допустим есть ошибка, она очевидна, её легко изолировать и она вызывает мало проблем. Это не означает, что вы не хотите ошибок, это просто означает, что вы можете быстро найти и исправить их. Одним из примеров является пакетное задание, которое просматривает небольшой объем данных и строит отчёт: большинство ошибок, которые может обнаружить спецификация, будут очевидны в рабочей среде, и как только вы их исправите, вы можете легко повторно запустить старые данные. Идеально. Спецификации всё еще могут помочь в этом, но их преимущества корректности менее ценны.
Низкоуровневый код
Не весь код является проекцией какого-то абстрактного дизайна. Иногда основная идея лежит на уровне кода, и в этом случае в спецификации отсутствуют деревья для леса.
Многие манипуляции и сбор данных подобны этому. Возьмём программу, которая обращается к десяти API, извлекает информацию и объединяет её вместе. Там есть дизайн более высокого уровня, с обработкой ошибок, поведением при повторных попытках и всем остальным, но большая часть работы заключается в преобразованиях необработанных данных на уровне реализации. Спецификации дизайна слишком далеки от этого, чтобы помочь; Вы хотите что-то ближе.
И любой вид численных вычислений не подходит. Большинство языков спецификаций могут выражать целые числа, но очень немногие могут на самом деле проверять их на модели. Единственный инструмент, который я видел, который может обрабатывать любые действительные числа, - это PRISM, у которого есть… другие проблемы. Вам не нужно проверять математические операции на уровне архитектуры.
Неоднозначные свойства
Как любят говорить сторонники Agile, лучший способ понять, что нужно людям, - это увидеть, как они взаимодействуют с существующей системой. Но это не обязательно означает, что система должна быть полнофункциональной: часто достаточно прототипа. Требования быстро меняются, и наше понимание того, что нужно на ранних этапах, зачастую минимально. Есть некоторые свойства, которыми система, вероятно, не должна обладать, например, “случайные сбои” или “взрывы”. Но это не обязательные свойства прототипа! Если человек использует систему, чтобы понять, чего он хочет от системы, то менее важно, чтобы система “работала”. Мы собираем данные.
В некотором смысле прототип занимает место спецификации на этом этапе: вместо того, чтобы повторять спецификацию, чтобы найти системные проблемы, вы повторяете прототип, чтобы найти проблемы клиента.
Расширение кода
Этот немного грязнее, чем остальные. Одно из моих предубеждений о программном обеспечении состоит в том, что большинство программ либо пишутся для автоматизации чего-то, чтобы люди не имели к этому никакого отношения, либо дополняют человека, чтобы он мог делать что-то лучше. Грейдон Хоар называет это разницей между пакетной обработкой и интерактивными вычислениями. Границы между ними нечёткие: калькулятор автоматизирует механические вычисления или расширяет ваши возможности для выполнения вычислений? На самом деле мало того и другого. Но я по-прежнему считаю эту модель полезной.
По моему опыту, спецификации гораздо полезнее для автоматизации, чем для дополнения. В автоматизации человек может запустить её, но не обязательно что-то делать потом, поэтому важнее, чтобы она удовлетворяла инвариантам. В расширенном коде постоянно присутствует человек, который может настраивать систему и вносить самокоррекцию.
Заключение
Хорошо, вы дочитали до этого места, пора подытожить. Формальные методы — невероятно мощный инструмент. Самым большим препятствием для их использования, на мой взгляд, является образование. Формальные методы требуют другого мышления, отличного от кодирования, и иногда у людей возникают проблемы с интуицией. Существует также неявно предполагаемый набор математических навыков, которые легко освоить, но трудно осознать, что вам нужно их освоить. Я написал книгу “Practical TLA+, Planning Driven Development”, чтобы помочь людям в этом, но ничто не сравнится с опытным учителем.