В последнее время попадаются статьи на хабре, обосновывающие пользу спеков и моделей. Много слов сказано про новое ПО, которое удешевит инженерный подход. Но все примеры которые я нахожу связаны с довольно узким спектром задач. В большинстве проектов в IT и алгоритмы то никакие не используются, не считая библиотечных.
Могу посоветовать посмотреть блог Hillel Wayne, по поводу того какие в каких задачах может быть применёны model-checkers/model-finders. Там много простых примеров из разных областей. А его книга Practical TLA+ начинается с самого что ни на есть примера именно из бизнес-логики: пересылка денег между счетами.
Можете сказать, насколько реально и целесообразно на данный момент использование данного подхода, скажем в обычном клиент — серверном решении (мобилка + сервер, например). Например, клиент запросил сервис по доставке еды — имеет в этом случае писать спеки и создавать модели?
На вскидку, где я вижу применение моделей:
Промоделировать логику работы пользователя с системой на общем уровне, с целью найти неоптимальные последовательности действий пользователя с точки зрения важности востребованности функции для пользователя и сложности её реализации в протоколе работы пользователя с системой (грубо говоря, чтобы система следовала принципу наименьшего удивления пользователя).
Промоделировать сущности в системе и их взаимосвязь, с целью исключить какие-либо неправильные конфигурации в системе.
Промоделировать протоколы взаимодействия модулей в системе, чтобы посмотреть, нет ли каких-нибудь неочевидных/невалидных состояний (как пример, из-за сбоя в подтверждении запроса от одного модуля к другому, система зациклилась и начала пользователю складывать в цикле блюда в корзину из-за ретраев).
Это всё делается весьма быстро и малозатратно при определённом уровне навыков, но при этом может существенно повысить качество системы и user experience.
Или, скажем, чуть более сложный заказ: клиент хочет разработать систему умного дома, имеет ли это смысл в этом случае?
Тут примерно то же самое, что и в предыдущем пункте: самое быстрое и простое — это промоделировтаь логику работы пользователя с системой, с целью недопущения ситуаций, когда для включения лампочки нужно системе дать 5 команд.
Более глубокие уровни — это моделирование взаимодействия железок в системе умного дома, чтобы исключить всякие неприятные ситуации для пользователя из-за каких-нибудь дедлоков и пр. в протоколах и логике.
Если да, то можно ли увидеть пример?
Для более-менее толкового примера нужно чуть погрузиться в специфику умного дома, что потребует времени. Саму модель для наиболее важных частей системы после этого сделать относительно несложно.
Насчёт модели умного дома можно продолжить в личке, если мне получится выкроить время чтобы погрузиться в специфику этой области на достаточном уровне, может ещё одну статью по этому поводу напишу с примером близком к реальности.
Создание математической модели для алгоритма это одно, у тебя есть входные параметры, их область применения, это все очень похоже на математику и ее теоремы. А вот с бизнес логикой, где много висящих хвостов, ad hoc параметров все выглядит иначе.
Принципиальной разницы нет. Опять же рекомендую в блоге Hillel Wayne посмотреть примеры из разных областей.
Моделирование подходит для любых областей, где есть система с пространством состояний и дискретные переходы между ними (в общем случае недетерминированные).
Поиск моделей подходит для задач, которые можно выразить в виде некоторых объектов и отношений между ними, ну и плюс логика.
Важно иметь некоторый опыт и навыки работы с тулами и опыт по абстракции и декомпозиции частей системы, чтобы потом на абстрактном уровне проанализировать их взаимодействие.
В общем случае — да, проблема останова нам гарантирует отсутствие универсального алгоритма проверки свойств системы. Но современные средства позволяют просматривать огромные пространства состояний за разумное время. Тот же самый Alloy, работая через SAT-солверы, проверяет огромные пространства состояний в поисках примеров/контр-примеров.
Даже explicit model-checkers, типа TLA+/TLC, могут проверять вполне хорошие пространства состояний для практического применения. А если ещё взять TLAPS, который позволяет некоторые формулы TLA+ доказывать строго математически (индуктивно) с использованием SAT-солверов, то получается можно проверять свойства систем с весьма приличным размером.
Относительно покрытия — тут моё мнение таково: хорошее покрытие явно лучше его отсутствия, но оно недостаточно во многих задачах. Например, современное ПО активно становится параллельным и асинхронным и тут статичное покрытие уже мало о чём говорит. Вы можете тестами добиться 100% покрытия кода, но параллельная/распределённая/асинхронная прога легко будет сбоить дедлоками/live-locks и пр.
Кроме того, 100% покрытие даже однопоточной проги не гарантирует её корректности, если в основе лежит некорректный алгоритм.
Так как 100% покрытие не может гарантировать сохранение контрактов и инвариантов в коде (этого можно добиться только перейдя к формальной верификации).
Тести и покрытие это хорошо, но этого часто бывает недостаточно даже для однопоточного кода.
Правда подход внутренних DSL (как в примере с baysick) мне не сильно нравится (похожее можно получить с помощью GADT, обобщённых алгебраических типов).
Больше нравится подход в Ocaml: https://ocamlverse.github.io/content/ppx.html. Там есть специальные точки расширения и плагины к компилятору, которые работают над AST. Можно гибче управлять синтаксисом (так как плагины работают над AST до компилятора) и четко видно, где используется DSL.
По поводу контрактов, мне очень нравится подход в Ada/SPARK (https://www.adacore.com/resources). Там можно контракты как верифицировать, так и вынести в рантайм, и это довольно гибко можно настраивать. GNATProve+ GNATTest возволяют гибко двигать границу между протестированным кодом и отверифицированным.
Формальная спека позволяет убедиться, что ваш код в совокупности корректен и не приводит в запрещенные состояния
Я бы уточнил: формальные спеки нужны в первую очередь для проверки алгоритмов, которые лягут в основу кода.
Закрыть формально путь от формальных спек к коду можно (чтобы гарантировать соответствие кода спекам), но это уже довольно сложно и дорого в общем случае.
Спеки в первую очередь позволяют не допустить серьёзных косяков в архитектуре, протоколах взаимодействия и тому подобных вещей.
Хорошо закрывает путь от формальных спек к результирующему коду подход Event-B и тулы типа AtelierB. Но там спеки не настолько высокоуровневые, как Alloy или TLA+ и заточены в основном на описании FSM'ок и их постепенного уточнения (с формальным доказательством корректности уточнения) вплоть до результирующей кодогенерации в Ada или C.
По пунктам контр-аргументировать будет долго, поэтому только самые некорректные прокомментирую:
model-checkers не используют даже старые дядьки с опытом в 20 лет и больше. Просто потому, что любая современная IDE имеет встроенные проверки на race conditions, потенциально возможные исключения и тп и тд.
Во-первых, не используют, так как многие просто не знают о них и не умеют пользоваться.
Во-вторых, стат-анализаторы, хоть и сделали большой шаг вперёд, до сих пор не могут (да и в принципе не смогут) находить широкий класс ошибок, например, в распределённом ПО (да и в параллельном тоже, детекции на гонки/дедлоки и пр — в самом зачаточном состоянии).
Я бы не рекомендовал читать Лампорта просто потому, что литература устаревшая и специфичная. На сколько я знаю, тот-же TLA больше не используется.
Ну какая разница, как называется инструмент и как выглядят его команды, если он именно что занимается стандартным подходом, определяемым названием «верификация программ»? Да, инструмент использует не весь аппарат верификации, ну и что? Да, вы сами пишите скрипты верификации, но суть-то от этого почему изменилась? Вы показали ручной вариант верификации, но алгоритм «модель-проверка» никуда от этого не делся.
Знаете, мне сложно дискутировать на таком уровне. Разговор в таком ключе мне представляется довольно беспредметным и неконструктивным.
Программа/алгоритм/модель и пр — это всё существенно разные понятия, и смешивать их в одну кучу — совсем не правильно.
Верификация программ, проверка моделей, вероятностная проверка моделей, поиск моделей и др — это всё существенно разные методы и инструменты, которые имеют разные (возможно, где-то немного пересекающиеся) области применения.
Если честно, то model-checkers/model-finders — это не совсем про соф (даже совсем не про софт), а про любые системы, которые описываются формализмами, на которых базируется тот или иной инструмент. Например, TLA+ используется для проверки корректности не только софта, но и железа (когерентность кэшей, например).
Alloy можно использовать для исследования всевозможных структур, например, конфигурации топологий машин в сети и тд.
Если есть желание дискутировать в конструктивном русле с нормально применяемой терминологией, без смешения и подмен, то всегда с удовольствием, но в текущий момент в данной ветке дискуссии никакой пользы ни для кого я не вижу, уж извините.
Но давайте вспомним, что включает спецификация? 7 состояний и десяток переходов. Всего пара десятков элементов. Всего!
Многие спецификации реально важных алгоритмов (Chord, Paxos и тд) тоже не сильно большие.
В реальности сложные задачи оперируют сотнями, а то и тысячами элементов. Простейший случай — связываем текстовое поле с БД. Одно единственное текстовое поле. Начнём с БД — нужна собственно база (где-то уже установленная), нужна связь с ней, нужны логины/пароли, нужна таблица значений, нужен селект конкретного значения, нужно чтение результатов селекта, нужно положить прочитанное в поле, нужно прочитать из поля в нужный момент, запихнуть в апдейт (который нужно написать), правильно выполнить апдейт, показать юзеру некий фидбэк. Вот такой самый минимальный минимум. Ради одного поля. Без логики. Только лишь тупое копирование.
Зачастую нет смысла делать такие детальные спеки. Выше где-то в комментариях, я уже писал о важном навыке — грамотно проводить уровни абстракции.
Зачастую действительно важные и критичные свойства системы можно проверить на весьма абстрактных (и соответственно небольших) спеках.
Зачем делать детальную спеку БД, записей, сетевых соединений и пр, если цель — проверить корректность алгоритма аутентификации пользователя?
Это один из вопросов, которые должны решать разработчики для грамотного применения формальных методов — понимать где и на каком уровне абстракции их применять.
В целом призыв «давайте наконец будем думать» выше уже нашёл подходящий ответ — думать дорого.
Вот я как раз и преследую цель данной статьёй — показать, что эта фраза и этот стереотип немного устарели. Думать сейчас стало намного дешевле с современной инструментальной поддержкой.
Хотя и без комментариев давно было ясно, что доказывание свойств программы — совсем не панацея.
Методов и инструментов широкий спектр. Доказывание свойств программы — это отдельная ветвь формальных методов и самая трудоёмкая.
В статье речь идёт не о формальной верификации программ. А о применении инструментов класса model-finders для исследования прототипа архитектуры.
Как некий предварительный шаг в сторону инструмента, который сделает за разработчика большую часть работы, такой подход уместен. В неких узких и очень дорогих нишах такой подход так же может быть применён. Но всё остальное (99.99%) — не из этой оперы. И это — главное, что стоило донести в статье.
Если честно, складывается ощущение, что статью вы только просмотрели по заголовкам. Ибо я про верификацию программ только вскользь упоминал. Основная часть статьи — это применение Alloy для исследования свойств архитектуры решения из области организации микросервисной системы.
В неких узких и очень дорогих нишах такой подход так же может быть применён. Но всё остальное (99.99%) — не из этой оперы. И это — главное, что стоило донести в статье.
Давайте сначала вы всё-таки более внимательно посмотрите статью, а потом уже думаю можно будет обсудить её более детально и предметно.
Так как именно такие стереотипы (как вышепроцитированное утверждение) я и пытаюсь немного развеять.
Я уже частично написал в комментариях ответы на эти вопросы, но повторюсь ещё раз:
У любых методов, и формальные тут не исключение, своя область применения и критерии применимости.
Нужно ко всему подходить разумно и формальные спеки использовать именно там, где они дадут выигрыш.
Для того, чтобы понимать где и какие формальные методы можно применять, нужно немного с ними ознакомиться, на что и направленна данная статья (ну и будущие статьи)
Далее, ответы на приведённые аргументы:
Юзеры не знают, чего они хотят — мы должны сделать продукт и предложить им, а они уже заценят.
Во-первых, я уже упоминал, что есть хорошие методы и инструменты для работы с требованиями, которые могут помочь в работе даже с быстро-меняющимися требованиями.
Во-вторых, вряд ли требования у пользователей меняются настолько кардинально, что нельзя даже выделить и абстрагировать ядро функционала, нужного пользователю.
В-третьих, многие вещи с пользователями можно обсуждать на основе моделей и результатов моделирования (например, логику работы UI в виде состояний недетерминированных FSM'ок, нужно только выбрать подходящее, понятное для пользователя графическое представление). Это может оказаться существенно быстрее, чем писать и выкидывать прототипы.
Заказчик не знает, сколько времени и денег он готов вложить в продукт, поскольку не понятно, насколько он «зайдёт»
Ну тут могу только повториться: нужно хорошо понимать где и какие методы и инструменты применять.
И если у вас стартап по написанию игрушки для андроид на деньги венчурного фонда, то тут да, формальные методы и спеки могут быть излишни.
Программисты не знают, насколько сложно (и возможно ли вообще) будет реализовать часть фич
А вот тут формальные спеки, на мой взгляд, зачастую могут помочь с более точной оценкой, так как вероятность ошибок, которые могут повлечь большие объёмы работы — архитектурных и подобных им, становится меньше.
Ну во-первых, спеки позволяют быстро проверить какие-то идеи и зачастую при меньших затратах, чем написание тестов и прототипов.
Во-вторых устаревание спек сопоставимо с устареванием тестов при изменении функционала/архитектуры и пр. Во всяком случае, на мой взгляд.
В-третьих, моделирование спек даёт такое покрытие, которое никакими тестами не достичь.
В-четвёртых, в распределённых (и параллельных) системах зачастую такое огромное пространство состояний, что любые тесты тут просто бессильны.
Ну и в-пятых, TDD и спеки совсем не являются антагонистами.
Напротив, формальные спеки очень хорошо сочетаются с любыми тестами, так как на основе спек мы можем делать направленные тесты, которые бы максимально учитывали краевые случаи в системе.
Видимо мне так и не удалось раскрыть основной посыл статьи: современные инструменты делают возможным применение формальных методов при небольших затратах на широком спектре практических задач.
И, если вы посмотрите материал по ссылкам в статье (особенно в блоге Hillel Wayne), вы увидите, что применять формальные методы можно довольно легко и в довольно многих областях разработки ПО.
Вопрос только в том, чтобы грамотно видеть, где применение каких инструментов принесёт наибольший эффект.
Ну и естественно, нужно небольшое знакомство с этими методами и инструментами (на что, в основном и направлена статья)
Да и не только фейсбук. Сейчас многие крупные компании понимают, что софт, который позволил им взлететь, не позволяет лететь дальше и выше и обращаются к серьёзным методам и инструментам. В статье только малая часть айсберга по таким примерам в заключении приведена.
Мотивировать инженера можно двумя путями — либо показав, что это круто и крутые чуваки так делают, либо спустив разнарядку сверху.
Мне кажется путей мотивации всё-таки чуть больше. Например, что меня серьёзно мотивирует в формальных методах — это последующая экономия времени на отладку (отлаживать многопоточные приложения с плаващими логическими багами — это то ещё "удовольствие") и возможность, в случае model-checkers/model-finders, быстро проверять свои идеи.
Сейчас делаем интерактивные диаграммы с использованием Graphviz с web assembly напрямую
Спасибо за идею! Обязательно посмотрю подробнее. Для анимации взаимодействующих FSM'ок (интерфейсы/протоколы) возможно самое оно.
Да, сейчас время коротких итераций и быстрой разработки. Важна скорость адаптации бизнеса и ПО, в частности, к постоянно меняющимся условиям.
Но, осмелюсь утверждать, это не только не отрицает инженерный подход, но в некоторых случаях синергизм инженерного подхода и итеративной скоростной разработки может быть очень ощутимым.
Например, model-checkers/model-finders могут быть очень хорошим первичным фильтром для идей по изменению архитектуры, что позволяет серьёзно сэкономить время и силы на дальнейшей отладке и поддержке (да и просто писанины кода меньше, чем в случае прототипирования, тестирования, отката изменений и пр.).
Если у вас есть формальная отлаженная спека ПО (например Alloy и/или TLA+), то на ней можно быстро тестировать реализуемость нового функционала, который серьёзно может затронуть архитектуру ПО и соответственно результатам моделирования корректировать вносимые изменения, что позволяет в серьёзной степени исключить в дальнейшем длительную отладку для поиска редкого критичного бага, который проявился только у потребителей ПО под боевой нагрузкой, переписывание огромного объема кода, чтобы скорректировать такие баги (и как правило, это переписывание — просто обкладывание костылями, что множит проблему) и тд.
TLA+/Alloy и тд спеки очень хорошо разрабатываются итеративно и иерархически, что хорошо сочетается с agile подходом. И работать со спеками не сложнее чем работать с обычными исходниками.
У молодого специалиста время всегда в дефиците. Нужно и что-то поизучать и погулять и пиво попить :)
А современные фреймворки, языки, NoSQL БД и пр. плодятся как грибы после дождя, ты ещё не успел до конца освоиться с Ruby/Rails, тут выходит более модный Django/Python, все начинают обсуждать его и тд. (я не силён в вебе, поэтому пример может быть несколько неправильным)
Всё это отвлекает внимание, требует время на изучение и пр.
И в результате остаются без внимания фундаментальные вещи. Как например, умение правильно и грамотно проводить уровни абстракции, там где нужно, переходить к специализации решения, умение анализировать идеи и алгоритмы на применимость в решении какой-либо задачи и тд.
думать и анализировать, пока что, для разработчика — главный навык
С этим-то я как раз не спорю совсем. Я лишь говорю о том, что сейчас много инструментов, способов и методов, которые могут существенно помочь в анализе.
Но этим инструментам, методам и пр. совсем не уделяется должного внимания.
И в частности из-за увлечения быстроменяющимися современными фреймворками, прикладными технологиями, языками и пр.
Новые технологии это модно, это круто, книги по ним выходят с огромной скоростью и почти сразу устаревают.
Кому из молодёжи будет интересно на этом фоне сесть и начать вдумчиво читать "Specifying Systems" Лампорта?
Более того, многие даже не знают, что можно свой свежепридуманный алгоритм или ещё какую-нибудь идею быстро проверить на model-checkers/model-finders.
И цель этой статьи немного рассказать о том, что есть интересные инструменты, которые помогают разрабатывать и анализировать архитектуру, алгоритмы и пр.
без способностей решать какие-то задачи никого не брали
Решать задачи зачастую бывает недостаточно. Иногда нужно решать и гарантировать определённые свойства решения, вот о способах гарантировать определённые свойства решения и идёт речь в статье.
Проблема в том, что хорошие компании часто теряют клиентов из-за тех, кто выбирает дешевле и быстрее, а выбирают их менеджеры, которые не видят разницы между сениором и джуниором, видят только цифры, так и появляются компании индусов, которым и требования не нужны, и сроки минимальные, после них никакой документации не остается и никакие архитектурные решения не применяются. Но это не из-за погони за фреймворком, а потому что так дешевле и быстрее.
К сожалению да, менеджмент играет свою отрицательную роль в низком качестве современного софта. И что самое смешное, в итоге получается и не быстрее и не дешевле. А потом боинги падают, у тойот залипает газ и тд.
Что вы думаете про промежуточные варианты (типа Design-by-Contract + DSL)?
В некоторых случаях весьма хорошее решение. Когда кодогенератор для контрактов и DSL поддерживает высококвалифицированный спец, который может гарантировать с высокой степенью корректность кодогенерации, а остальные разработчики пользуются этим — вполне рабочее и хорошее решение.
порог входа высокий и разработчику без магистерской степени объяснить тот же TLA+ очень затруднительно
Вот это дискуссионный вопрос. Мне кажется тут больше от мотивации разработчика зависит, чем от его степени магистра/бакалавра и пр. Освоить TLA+, на мой вгляд, не сложнее чем асинхронное программирование. То есть, если разработчик мотивирован изучить TLA+, то он его изучит. Особенно если применять на уровне PlusCal не спускаясь на более низкий уровень — то с этим вполне по силам справиться даже средним разработчикам.
В итоге для критических вещей мы написали DSL компилятор на базе Scala, который генерирует гарантированно (ну, когда автор с командой не налажали) корректный код для структур данных и интерфейсов сервисов (с проверками целостности, инвариантами, трансформациями между представлениями и прочим) на нескольких языках. А программеры живут под DbC и доказывают друг другу корректность устно проверяя контракты на ревью.
Получилось по-моему не плохо. С одной стороны, пришлось пожертвовать универсальностью и строгостью, но с другой стороны удалось выйти за пределы "башни из слоновой кости" в поле, к "ремесленникам".
Нормальный подход. Единственное, что тут нужно серьёзное внимание уделять корректности кодогенерации из DSL. Ну и поддерживать самостоятельно эти тулы для DSL.
Я бы попробовал найти и адаптировать уже существующие тулы из этой области (что-нибудь а-ля http://smc.sourceforge.net/), наверняка есть близкие вашим задачам. Это потом позволит экономить на поддержке тулов.
"картинки! Оно умеет клевые доки и картинки!11"
PlantUML, Graphviz/Dot, Tex/Tikz? :)
Хорошо мотивирует изучать TLA+ вот эта книжка (выше уже приводил ссылку): OpenCOM RTOS
Там народ благодаря спекам на TLA+ смог архитектурно соптимизировать RTOS так, что по сравнению с предшествующим вариантом у них получилось в 10 раз! меньше кода.
Формальная верификация, во всяком случае как я её понимаю (строгое доказательство свойств, а-ля логика Хоара для верификации кода, зависимые типы и пр), это всё-таки вещь весьма трудоёмкая, даже с современными ATP и пр.
А вот model-checker/model-finders вполне себе доступная даже для повседневного применения обычными программистами. Конечно есть определённая кривая обучения, но просто несравнимая с кривой у хардкорных формальных методов.
Хотя и хардкор я тоже планировал рассмотреть в будущих статьях (есть идея попытаться кратко расписать формальную верификацию реализации TLSF аллокатора памяти в SPARK/Ada)
Основная проблема даже не водопад vs agile (моделирование и даже некоторые методы верификации нормально совмещаются с agile), а в том, что в погоне за новомодными методами, языками, фреймворками и тд. утрачивается самое важное качество разработчика — способность думать и анализировать. Хотя сейчас есть очень хорошая инструментальная поддержка для анализа архитектурных решений, алгоритмов и пр., что позволяет проводить серьёзный анализ решений в разработке с относительно небольшими трудозатратами.
Пожалуйста! Рад что статья оказалась интересной.
Могу посоветовать посмотреть блог Hillel Wayne, по поводу того какие в каких задачах может быть применёны model-checkers/model-finders. Там много простых примеров из разных областей. А его книга Practical TLA+ начинается с самого что ни на есть примера именно из бизнес-логики: пересылка денег между счетами.
На вскидку, где я вижу применение моделей:
Промоделировать логику работы пользователя с системой на общем уровне, с целью найти неоптимальные последовательности действий пользователя с точки зрения важности востребованности функции для пользователя и сложности её реализации в протоколе работы пользователя с системой (грубо говоря, чтобы система следовала принципу наименьшего удивления пользователя).
Промоделировать сущности в системе и их взаимосвязь, с целью исключить какие-либо неправильные конфигурации в системе.
Промоделировать протоколы взаимодействия модулей в системе, чтобы посмотреть, нет ли каких-нибудь неочевидных/невалидных состояний (как пример, из-за сбоя в подтверждении запроса от одного модуля к другому, система зациклилась и начала пользователю складывать в цикле блюда в корзину из-за ретраев).
Это всё делается весьма быстро и малозатратно при определённом уровне навыков, но при этом может существенно повысить качество системы и user experience.
Тут примерно то же самое, что и в предыдущем пункте: самое быстрое и простое — это промоделировтаь логику работы пользователя с системой, с целью недопущения ситуаций, когда для включения лампочки нужно системе дать 5 команд.
Более глубокие уровни — это моделирование взаимодействия железок в системе умного дома, чтобы исключить всякие неприятные ситуации для пользователя из-за каких-нибудь дедлоков и пр. в протоколах и логике.
Для более-менее толкового примера нужно чуть погрузиться в специфику умного дома, что потребует времени. Саму модель для наиболее важных частей системы после этого сделать относительно несложно.
Насчёт модели умного дома можно продолжить в личке, если мне получится выкроить время чтобы погрузиться в специфику этой области на достаточном уровне, может ещё одну статью по этому поводу напишу с примером близком к реальности.
Принципиальной разницы нет. Опять же рекомендую в блоге Hillel Wayne посмотреть примеры из разных областей.
Моделирование подходит для любых областей, где есть система с пространством состояний и дискретные переходы между ними (в общем случае недетерминированные).
Поиск моделей подходит для задач, которые можно выразить в виде некоторых объектов и отношений между ними, ну и плюс логика.
Важно иметь некоторый опыт и навыки работы с тулами и опыт по абстракции и декомпозиции частей системы, чтобы потом на абстрактном уровне проанализировать их взаимодействие.
В общем случае — да, проблема останова нам гарантирует отсутствие универсального алгоритма проверки свойств системы. Но современные средства позволяют просматривать огромные пространства состояний за разумное время. Тот же самый Alloy, работая через SAT-солверы, проверяет огромные пространства состояний в поисках примеров/контр-примеров.
Даже explicit model-checkers, типа TLA+/TLC, могут проверять вполне хорошие пространства состояний для практического применения. А если ещё взять TLAPS, который позволяет некоторые формулы TLA+ доказывать строго математически (индуктивно) с использованием SAT-солверов, то получается можно проверять свойства систем с весьма приличным размером.
Относительно покрытия — тут моё мнение таково: хорошее покрытие явно лучше его отсутствия, но оно недостаточно во многих задачах. Например, современное ПО активно становится параллельным и асинхронным и тут статичное покрытие уже мало о чём говорит. Вы можете тестами добиться 100% покрытия кода, но параллельная/распределённая/асинхронная прога легко будет сбоить дедлоками/live-locks и пр.
Кроме того, 100% покрытие даже однопоточной проги не гарантирует её корректности, если в основе лежит некорректный алгоритм.
Как пример — история с timsort (http://www.envisage-project.eu/proving-android-java-and-python-sorting-algorithm-is-broken-and-how-to-fix-it/).
Так как 100% покрытие не может гарантировать сохранение контрактов и инвариантов в коде (этого можно добиться только перейдя к формальной верификации).
Тести и покрытие это хорошо, но этого часто бывает недостаточно даже для однопоточного кода.
Интересные ссылки.
Правда подход внутренних DSL (как в примере с baysick) мне не сильно нравится (похожее можно получить с помощью GADT, обобщённых алгебраических типов).
Больше нравится подход в Ocaml: https://ocamlverse.github.io/content/ppx.html. Там есть специальные точки расширения и плагины к компилятору, которые работают над AST. Можно гибче управлять синтаксисом (так как плагины работают над AST до компилятора) и четко видно, где используется DSL.
Дополню немного по системам типов: новичкам могу рекомендовать Пирса: https://www.ozon.ru/context/detail/id/7410082/ (в англоязычной среде её называют brick-book :) )
По поводу контрактов, мне очень нравится подход в Ada/SPARK (https://www.adacore.com/resources). Там можно контракты как верифицировать, так и вынести в рантайм, и это довольно гибко можно настраивать. GNATProve+ GNATTest возволяют гибко двигать границу между протестированным кодом и отверифицированным.
Я бы уточнил: формальные спеки нужны в первую очередь для проверки алгоритмов, которые лягут в основу кода.
Закрыть формально путь от формальных спек к коду можно (чтобы гарантировать соответствие кода спекам), но это уже довольно сложно и дорого в общем случае.
Спеки в первую очередь позволяют не допустить серьёзных косяков в архитектуре, протоколах взаимодействия и тому подобных вещей.
Хорошо закрывает путь от формальных спек к результирующему коду подход Event-B и тулы типа AtelierB. Но там спеки не настолько высокоуровневые, как Alloy или TLA+ и заточены в основном на описании FSM'ок и их постепенного уточнения (с формальным доказательством корректности уточнения) вплоть до результирующей кодогенерации в Ada или C.
По пунктам контр-аргументировать будет долго, поэтому только самые некорректные прокомментирую:
Во-первых, не используют, так как многие просто не знают о них и не умеют пользоваться.
Во-вторых, стат-анализаторы, хоть и сделали большой шаг вперёд, до сих пор не могут (да и в принципе не смогут) находить широкий класс ошибок, например, в распределённом ПО (да и в параллельном тоже, детекции на гонки/дедлоки и пр — в самом зачаточном состоянии).
Весьма ложное утверждение. Ссылки, которые это опровергают, я уже приводил в статье (в заключении посмотрите их).
Вот например небольшой список по ссылке: https://lamport.azurewebsites.net/tla/industrial-use.html
Как вы там можете увидеть многие публикации по ссылкам весьма свежие.
Вот один из свежих примеров применения TLA+ :https://github.com/elastic/elasticsearch/issues/31976#ISSUECOMMENT-404722753
Вот тут детальный анализ проблемы в наглядном виде: https://users.ece.cmu.edu/~koopman/pubs/koopman14_toyota_ua_slides.pdf
Там не просто "коврик" был. Весьма интересный материал по ссылке, рекомендую.
Знаете, мне сложно дискутировать на таком уровне. Разговор в таком ключе мне представляется довольно беспредметным и неконструктивным.
Программа/алгоритм/модель и пр — это всё существенно разные понятия, и смешивать их в одну кучу — совсем не правильно.
Верификация программ, проверка моделей, вероятностная проверка моделей, поиск моделей и др — это всё существенно разные методы и инструменты, которые имеют разные (возможно, где-то немного пересекающиеся) области применения.
Если честно, то model-checkers/model-finders — это не совсем про соф (даже совсем не про софт), а про любые системы, которые описываются формализмами, на которых базируется тот или иной инструмент. Например, TLA+ используется для проверки корректности не только софта, но и железа (когерентность кэшей, например).
Alloy можно использовать для исследования всевозможных структур, например, конфигурации топологий машин в сети и тд.
Если есть желание дискутировать в конструктивном русле с нормально применяемой терминологией, без смешения и подмен, то всегда с удовольствием, но в текущий момент в данной ветке дискуссии никакой пользы ни для кого я не вижу, уж извините.
Многие спецификации реально важных алгоритмов (Chord, Paxos и тд) тоже не сильно большие.
Зачастую нет смысла делать такие детальные спеки. Выше где-то в комментариях, я уже писал о важном навыке — грамотно проводить уровни абстракции.
Зачастую действительно важные и критичные свойства системы можно проверить на весьма абстрактных (и соответственно небольших) спеках.
Зачем делать детальную спеку БД, записей, сетевых соединений и пр, если цель — проверить корректность алгоритма аутентификации пользователя?
Это один из вопросов, которые должны решать разработчики для грамотного применения формальных методов — понимать где и на каком уровне абстракции их применять.
Вот я как раз и преследую цель данной статьёй — показать, что эта фраза и этот стереотип немного устарели. Думать сейчас стало намного дешевле с современной инструментальной поддержкой.
Методов и инструментов широкий спектр. Доказывание свойств программы — это отдельная ветвь формальных методов и самая трудоёмкая.
В статье речь идёт не о формальной верификации программ. А о применении инструментов класса model-finders для исследования прототипа архитектуры.
Если честно, складывается ощущение, что статью вы только просмотрели по заголовкам. Ибо я про верификацию программ только вскользь упоминал. Основная часть статьи — это применение Alloy для исследования свойств архитектуры решения из области организации микросервисной системы.
Давайте сначала вы всё-таки более внимательно посмотрите статью, а потом уже думаю можно будет обсудить её более детально и предметно.
Так как именно такие стереотипы (как вышепроцитированное утверждение) я и пытаюсь немного развеять.
Я уже частично написал в комментариях ответы на эти вопросы, но повторюсь ещё раз:
У любых методов, и формальные тут не исключение, своя область применения и критерии применимости.
Нужно ко всему подходить разумно и формальные спеки использовать именно там, где они дадут выигрыш.
Для того, чтобы понимать где и какие формальные методы можно применять, нужно немного с ними ознакомиться, на что и направленна данная статья (ну и будущие статьи)
Далее, ответы на приведённые аргументы:
Во-первых, я уже упоминал, что есть хорошие методы и инструменты для работы с требованиями, которые могут помочь в работе даже с быстро-меняющимися требованиями.
Во-вторых, вряд ли требования у пользователей меняются настолько кардинально, что нельзя даже выделить и абстрагировать ядро функционала, нужного пользователю.
В-третьих, многие вещи с пользователями можно обсуждать на основе моделей и результатов моделирования (например, логику работы UI в виде состояний недетерминированных FSM'ок, нужно только выбрать подходящее, понятное для пользователя графическое представление). Это может оказаться существенно быстрее, чем писать и выкидывать прототипы.
Ну тут могу только повториться: нужно хорошо понимать где и какие методы и инструменты применять.
И если у вас стартап по написанию игрушки для андроид на деньги венчурного фонда, то тут да, формальные методы и спеки могут быть излишни.
А вот тут формальные спеки, на мой взгляд, зачастую могут помочь с более точной оценкой, так как вероятность ошибок, которые могут повлечь большие объёмы работы — архитектурных и подобных им, становится меньше.
Ну во-первых, спеки позволяют быстро проверить какие-то идеи и зачастую при меньших затратах, чем написание тестов и прототипов.
Во-вторых устаревание спек сопоставимо с устареванием тестов при изменении функционала/архитектуры и пр. Во всяком случае, на мой взгляд.
В-третьих, моделирование спек даёт такое покрытие, которое никакими тестами не достичь.
В-четвёртых, в распределённых (и параллельных) системах зачастую такое огромное пространство состояний, что любые тесты тут просто бессильны.
Ну и в-пятых, TDD и спеки совсем не являются антагонистами.
Напротив, формальные спеки очень хорошо сочетаются с любыми тестами, так как на основе спек мы можем делать направленные тесты, которые бы максимально учитывали краевые случаи в системе.
Видимо мне так и не удалось раскрыть основной посыл статьи: современные инструменты делают возможным применение формальных методов при небольших затратах на широком спектре практических задач.
И, если вы посмотрите материал по ссылкам в статье (особенно в блоге Hillel Wayne), вы увидите, что применять формальные методы можно довольно легко и в довольно многих областях разработки ПО.
Вопрос только в том, чтобы грамотно видеть, где применение каких инструментов принесёт наибольший эффект.
Ну и естественно, нужно небольшое знакомство с этими методами и инструментами (на что, в основном и направлена статья)
Про контракты + DSL + кодогенерацию?
Статей на самом деле по этой теме хватает, но если уважаемый borv напишет свою статью на эту тему, будет крайне интересно ознакомиться с его опытом.
Так как подход действительно рабочий и зачастую даёт очень хороший эффект (в плане качества ПО по отношению к затратам на разработку).
Да и не только фейсбук. Сейчас многие крупные компании понимают, что софт, который позволил им взлететь, не позволяет лететь дальше и выше и обращаются к серьёзным методам и инструментам. В статье только малая часть айсберга по таким примерам в заключении приведена.
Мне кажется путей мотивации всё-таки чуть больше. Например, что меня серьёзно мотивирует в формальных методах — это последующая экономия времени на отладку (отлаживать многопоточные приложения с плаващими логическими багами — это то ещё "удовольствие") и возможность, в случае model-checkers/model-finders, быстро проверять свои идеи.
Спасибо за идею! Обязательно посмотрю подробнее. Для анимации взаимодействующих FSM'ок (интерфейсы/протоколы) возможно самое оно.
Да, сейчас время коротких итераций и быстрой разработки. Важна скорость адаптации бизнеса и ПО, в частности, к постоянно меняющимся условиям.
Но, осмелюсь утверждать, это не только не отрицает инженерный подход, но в некоторых случаях синергизм инженерного подхода и итеративной скоростной разработки может быть очень ощутимым.
Например, model-checkers/model-finders могут быть очень хорошим первичным фильтром для идей по изменению архитектуры, что позволяет серьёзно сэкономить время и силы на дальнейшей отладке и поддержке (да и просто писанины кода меньше, чем в случае прототипирования, тестирования, отката изменений и пр.).
Если у вас есть формальная отлаженная спека ПО (например Alloy и/или TLA+), то на ней можно быстро тестировать реализуемость нового функционала, который серьёзно может затронуть архитектуру ПО и соответственно результатам моделирования корректировать вносимые изменения, что позволяет в серьёзной степени исключить в дальнейшем длительную отладку для поиска редкого критичного бага, который проявился только у потребителей ПО под боевой нагрузкой, переписывание огромного объема кода, чтобы скорректировать такие баги (и как правило, это переписывание — просто обкладывание костылями, что множит проблему) и тд.
TLA+/Alloy и тд спеки очень хорошо разрабатываются итеративно и иерархически, что хорошо сочетается с agile подходом. И работать со спеками не сложнее чем работать с обычными исходниками.
У молодого специалиста время всегда в дефиците. Нужно и что-то поизучать и погулять и пиво попить :)
А современные фреймворки, языки, NoSQL БД и пр. плодятся как грибы после дождя, ты ещё не успел до конца освоиться с Ruby/Rails, тут выходит более модный Django/Python, все начинают обсуждать его и тд. (я не силён в вебе, поэтому пример может быть несколько неправильным)
Всё это отвлекает внимание, требует время на изучение и пр.
И в результате остаются без внимания фундаментальные вещи. Как например, умение правильно и грамотно проводить уровни абстракции, там где нужно, переходить к специализации решения, умение анализировать идеи и алгоритмы на применимость в решении какой-либо задачи и тд.
С этим-то я как раз не спорю совсем. Я лишь говорю о том, что сейчас много инструментов, способов и методов, которые могут существенно помочь в анализе.
Но этим инструментам, методам и пр. совсем не уделяется должного внимания.
И в частности из-за увлечения быстроменяющимися современными фреймворками, прикладными технологиями, языками и пр.
Новые технологии это модно, это круто, книги по ним выходят с огромной скоростью и почти сразу устаревают.
Кому из молодёжи будет интересно на этом фоне сесть и начать вдумчиво читать "Specifying Systems" Лампорта?
Более того, многие даже не знают, что можно свой свежепридуманный алгоритм или ещё какую-нибудь идею быстро проверить на model-checkers/model-finders.
И цель этой статьи немного рассказать о том, что есть интересные инструменты, которые помогают разрабатывать и анализировать архитектуру, алгоритмы и пр.
Решать задачи зачастую бывает недостаточно. Иногда нужно решать и гарантировать определённые свойства решения, вот о способах гарантировать определённые свойства решения и идёт речь в статье.
К сожалению да, менеджмент играет свою отрицательную роль в низком качестве современного софта. И что самое смешное, в итоге получается и не быстрее и не дешевле. А потом боинги падают, у тойот залипает газ и тд.
В некоторых случаях весьма хорошее решение. Когда кодогенератор для контрактов и DSL поддерживает высококвалифицированный спец, который может гарантировать с высокой степенью корректность кодогенерации, а остальные разработчики пользуются этим — вполне рабочее и хорошее решение.
Вот это дискуссионный вопрос. Мне кажется тут больше от мотивации разработчика зависит, чем от его степени магистра/бакалавра и пр. Освоить TLA+, на мой вгляд, не сложнее чем асинхронное программирование. То есть, если разработчик мотивирован изучить TLA+, то он его изучит. Особенно если применять на уровне PlusCal не спускаясь на более низкий уровень — то с этим вполне по силам справиться даже средним разработчикам.
Нормальный подход. Единственное, что тут нужно серьёзное внимание уделять корректности кодогенерации из DSL. Ну и поддерживать самостоятельно эти тулы для DSL.
Я бы попробовал найти и адаптировать уже существующие тулы из этой области (что-нибудь а-ля http://smc.sourceforge.net/), наверняка есть близкие вашим задачам. Это потом позволит экономить на поддержке тулов.
PlantUML, Graphviz/Dot, Tex/Tikz? :)
Хорошо мотивирует изучать TLA+ вот эта книжка (выше уже приводил ссылку): OpenCOM RTOS
Там народ благодаря спекам на TLA+ смог архитектурно соптимизировать RTOS так, что по сравнению с предшествующим вариантом у них получилось в 10 раз! меньше кода.
Неплохая книга, но Карпов для новичков будет намного понятнее и интереснее.
У Камкина материал слишком сжат и уже нужен хороший уровень матподготовки.
А если нужна хорошая обзорная книга по формальным методам, как ликбез, то мне понравилась вот эта: Understanding Formal Methods
А вот model-checker/model-finders вполне себе доступная даже для повседневного применения обычными программистами. Конечно есть определённая кривая обучения, но просто несравнимая с кривой у хардкорных формальных методов.
Хотя и хардкор я тоже планировал рассмотреть в будущих статьях (есть идея попытаться кратко расписать формальную верификацию реализации TLSF аллокатора памяти в SPARK/Ada)