Comments 135
При том, что такой подход выглядит многообещающе, сколько ресурсов (человеков) он потребляет? Более того, если называть это "инженерным" подходом против "ремесленного", то сколько широкоиспользуемого ПО было написано таким образом? СУБД, операционные системы общего назначения, веб-браузеры, веб-сервера, графические/текстовые редакторы?
В целом такой подход подразумевает, что цена пропущенного бага такова, что "никаких денег не жалко" на его предотвращение.
Мы точно хотим, чтобы стержни опустились в реактор, даже если на эти 3000 строк уйдёт год работы десятка программистов.
Но точно ли мы хотим год работы десятка программистов на безупречную работу фильтра "комикс" в графическом редакторе?
Тут же дело не в инструментах, а в полноте требований. Никакой инструмент не поможет разработать хорошие требования быстрее, чем требуется для осознания всех особенностей предметной области. А дальше там вопрос бюджета (денег, времени).
Одна из существенных проблем современной индустрии ПО, что разработка начинается намного раньше даже нормального осмысления требований, не говоря уже про полноту.
В результате — забиваем гвозди микроскопами, пытаемся ломом починить микросхемы и пр. Получаем в результате больших плохоподдерживаемых монстров из сильносвязанного спагетти-кода и пр.
Хотя весьма хорошо развивается область Requirements Management, есть хорошая литература по проблематике анализа и разработки требований (например, уже упомянутая в статье «Problem Frames») и тд. То есть, есть методики, инструменты и пр. для того, чтобы и к разработке требований подходить профессионально и серьёзно.
Причем современные инструменты позволяют серьёзно уменьшить затраты усилий на хорошую проработку требований. С требованиями сейчас тоже можно работать итеративно в стиле agile.
Очень интересный пример, когда сначала проанализировали требования, затем написали спеки и потом только стали кодить: OpenCOM RTOS. В итоге объем кода, по сравнению с предшествующим вариантом ПО, уменьшился на порядок (в 10 раз, как пишут в книге). Что было удивительно даже для самих авторов проекта, они даже не предполагали настолько сильный эффект.
Ну тут всем не угодишь :)
Некоторые говорят, что мало написал про внутреннюю кухню и математику стоящую за Alloy.
Вам показалось сложным пояснение про ограничения Alloy.
На самом деле, показанная ситуация с ограничением логики Alloy на практике нечасто встречается.
И этим инструментом (Alloy) можно вполне успешно и эффективно пользоваться даже не зная, что такое "сколемизация". Просто зная, что некоторые подкванторные выражения он не может анализировать и нужно либо их переформулировать в более простом виде, либо изменить условия (ослабить, например, как в примере в статье)
Просто зная, что некоторые подкванторные выражения он не может анализировать и нужно либо их переформулировать в более простом виде, либо изменить условияЭто очень демотивирует – мало того, что я должен написать корректную спецификацию, так еще тратить время на то, чтобы удовлетворить требования используемого инструмента.
Ну, фундаментально все инструменты имеют ограничения.
И вообще, многие задачи в области computer science неразрешимы.
Тут нужно просто понимать, какие классы задач какими способами и какими инструментами решать.
Alloy, даже со всеми своими ограничениями, для своего класса задач (моделирование структур и операций над ними, как пример подкласса) очень хороший инструмент.
Если Alloy не хватает (упёрлись в ограничения логики первого порядка), можно взять Higher-Order Alloy (https://aleksandarmilicevic.github.io/hola/). Там возможна квантификация по высшим структурам.
И для того, чтобы на примерах показать какие классы задач какими инструментами и как решаются и был задуман мной этот цикл статей.
В целом, сейчас моделирование вполне доступно для широкого применения даже в повседневной работе. Например, когда встаёт вопрос по оптимизациям логики работы с базой данных многих потребителей, как сократить количество блокировок и безопасно часть работы сделать асинхронной и тд.
Рекомендую посмотреть примеры в блоге Hillel Wayne, там видно, что моделирование можно легко и малозатратно применять даже для моделирования логики UI (в статье есть ссылка на это).
Одна из целей данной статьи — показать, что моделирование (поиск и проверка моделей) сейчас стало весьма дешёвым и удобным в использовании и его вполне можно применять в весьма широком классе задач.
Естественно, нужно разумно подходить ко всем используемым инструментам и хорошо понимать, где и какие инструменты стоит использовать. Но для этого нужно минимальное знакомство с инструментами, на что и направлена данная (и последующие) статья.
В следующих статьях (надеюсь, что будет возможность продолжить цикл статей в нормальном темпе) я планирую вернуться к вопросам применимости разных методов для разных задач, там более подробно будут рассмотрены классы задач и применимость различных методов для этих классов, соотношение усилий применения методов и полученного результата с реальными примерами из промышленности.
Данная статья эти вопросы оставила в стороне, так как в основном такие вопросы для разработчиков существенно менее интересны, чем технические подробности и примеры применения.
Так что с нетерпением жду второй статьи!
Уже в процессе. :)
Там будет прямо из реальной практики пример применения TLA+.
Должно неплохо получиться: с одной стороны реальное применение на реальной задаче (ошибка в алгоритме, которая не ловилась на тестах, но было интуитивное ощущение, что она там есть, и она там действительно была :) ), с другой — небольшая модель, которая будет понятна всем даже без всяких "сколемизаций" :)
Правда процесс не быстрый :( Сейчас основной работы много :(
К сожалению это вам не новый язык/фреймворк — сходу не вскочишь, нужно приличное количество сосредоточенной работы (поэтому пример я пролистал, ибо работа), по хорошему самое время ботанить такие вещи было во время учёбы, но увы.
Спасибо за Alloy. Уже пробовал TLA+ на учебных задачах, классная вещь.
Ещё было бы прикольно иметь фреймворк, который генерил бы шаблон под спеку по UML диаграмме, чтобы можно было бы изящно встроить model-checker'ы в пайплайн разработки, но не знаю есть ли уже такое
Либо по LTL и др. формулам из модели генерить проверяющий автомат, который бы работал по трассе событий из ПО и анализировал бы эту трассу на корректность.
Это позволило бы быстро ловить ошибки в логике ПО, где эта логика расходится с моделью.
И, кажется на первый взгляд, это вполне можно применять даже в продакшн-коде (зависит от величины модели и её детализации), когда рядом с боевым кодом всегда бежит проверяющий автомат и сразу сигнализирует, если вдруг что пошло не так (например, может приостановить боевой экземпляр ПО, запустить gdb attach, закрыть машину от нагрузки и позвать службу поддержки для решения проблемы).
Таким образом можно будет ловить проблемы на очень ранних стадиях, до того, как эффект от проблемы стал существенным (например, до того как положили в БД некорректные данные).
У молодого специалиста время всегда в дефиците. Нужно и что-то поизучать и погулять и пиво попить :)
А современные фреймворки, языки, NoSQL БД и пр. плодятся как грибы после дождя, ты ещё не успел до конца освоиться с Ruby/Rails, тут выходит более модный Django/Python, все начинают обсуждать его и тд. (я не силён в вебе, поэтому пример может быть несколько неправильным)
Всё это отвлекает внимание, требует время на изучение и пр.
И в результате остаются без внимания фундаментальные вещи. Как например, умение правильно и грамотно проводить уровни абстракции, там где нужно, переходить к специализации решения, умение анализировать идеи и алгоритмы на применимость в решении какой-либо задачи и тд.
думать и анализировать, пока что, для разработчика — главный навык
С этим-то я как раз не спорю совсем. Я лишь говорю о том, что сейчас много инструментов, способов и методов, которые могут существенно помочь в анализе.
Но этим инструментам, методам и пр. совсем не уделяется должного внимания.
И в частности из-за увлечения быстроменяющимися современными фреймворками, прикладными технологиями, языками и пр.
Новые технологии это модно, это круто, книги по ним выходят с огромной скоростью и почти сразу устаревают.
Кому из молодёжи будет интересно на этом фоне сесть и начать вдумчиво читать "Specifying Systems" Лампорта?
Более того, многие даже не знают, что можно свой свежепридуманный алгоритм или ещё какую-нибудь идею быстро проверить на model-checkers/model-finders.
И цель этой статьи немного рассказать о том, что есть интересные инструменты, которые помогают разрабатывать и анализировать архитектуру, алгоритмы и пр.
без способностей решать какие-то задачи никого не брали
Решать задачи зачастую бывает недостаточно. Иногда нужно решать и гарантировать определённые свойства решения, вот о способах гарантировать определённые свойства решения и идёт речь в статье.
Проблема в том, что хорошие компании часто теряют клиентов из-за тех, кто выбирает дешевле и быстрее, а выбирают их менеджеры, которые не видят разницы между сениором и джуниором, видят только цифры, так и появляются компании индусов, которым и требования не нужны, и сроки минимальные, после них никакой документации не остается и никакие архитектурные решения не применяются. Но это не из-за погони за фреймворком, а потому что так дешевле и быстрее.
К сожалению да, менеджмент играет свою отрицательную роль в низком качестве современного софта. И что самое смешное, в итоге получается и не быстрее и не дешевле. А потом боинги падают, у тойот залипает газ и тд.
У тойоты залипал газ из-за отсутствия интеграционного тестирования(коврик не давал педали газа отжаться).
По пунктам контр-аргументировать будет долго, поэтому только самые некорректные прокомментирую:
model-checkers не используют даже старые дядьки с опытом в 20 лет и больше. Просто потому, что любая современная IDE имеет встроенные проверки на race conditions, потенциально возможные исключения и тп и тд.
Во-первых, не используют, так как многие просто не знают о них и не умеют пользоваться.
Во-вторых, стат-анализаторы, хоть и сделали большой шаг вперёд, до сих пор не могут (да и в принципе не смогут) находить широкий класс ошибок, например, в распределённом ПО (да и в параллельном тоже, детекции на гонки/дедлоки и пр — в самом зачаточном состоянии).
Я бы не рекомендовал читать Лампорта просто потому, что литература устаревшая и специфичная. На сколько я знаю, тот-же TLA больше не используется.
Весьма ложное утверждение. Ссылки, которые это опровергают, я уже приводил в статье (в заключении посмотрите их).
Вот например небольшой список по ссылке: 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 могут быть очень хорошим первичным фильтром для идей по изменению архитектуры, что позволяет серьёзно сэкономить время и силы на дальнейшей отладке и поддержке (да и просто писанины кода меньше, чем в случае прототипирования, тестирования, отката изменений и пр.).
Если у вас есть формальная отлаженная спека ПО (например Alloy и/или TLA+), то на ней можно быстро тестировать реализуемость нового функционала, который серьёзно может затронуть архитектуру ПО и соответственно результатам моделирования корректировать вносимые изменения, что позволяет в серьёзной степени исключить в дальнейшем длительную отладку для поиска редкого критичного бага, который проявился только у потребителей ПО под боевой нагрузкой, переписывание огромного объема кода, чтобы скорректировать такие баги (и как правило, это переписывание — просто обкладывание костылями, что множит проблему) и тд.
TLA+/Alloy и тд спеки очень хорошо разрабатываются итеративно и иерархически, что хорошо сочетается с agile подходом. И работать со спеками не сложнее чем работать с обычными исходниками.
Юрий Карпов. MODEL CHECKING. Верификация параллельных и распределённых программных систем
Вы советуете книгу, которую нигде не найти :(
Спасибо за статью.
Да не за что.
Рад, что статья понравилась.
Вы советуете книгу, которую нигде не найти :(
К сожалению да, бумажный вариант думаю уже тяжело будет найти (хотя ещё относительно недавно видел его в продаже).
Но есть возможность электронного варианта: www.ozon.ru/context/detail/id/32561151
И ссылка на полноэкранный пред-просмотр у гугла: books.google.ru/books?id=xpui56eRsHgC&lpg=PP1&pg=PR3#v=onepage&q&f=false
А вот model-checker/model-finders вполне себе доступная даже для повседневного применения обычными программистами. Конечно есть определённая кривая обучения, но просто несравнимая с кривой у хардкорных формальных методов.
Хотя и хардкор я тоже планировал рассмотреть в будущих статьях (есть идея попытаться кратко расписать формальную верификацию реализации TLSF аллокатора памяти в SPARK/Ada)
Помню вроде у potan во френдах в фейсбуке был человек который сделал пособие по формальной верификации.
Эта — Камкин А.С. Введение в формальные методы верификации программ: учебное пособие?
Неплохая книга, но Карпов для новичков будет намного понятнее и интереснее.
У Камкина материал слишком сжат и уже нужен хороший уровень матподготовки.
А если нужна хорошая обзорная книга по формальным методам, как ликбез, то мне понравилась вот эта: Understanding Formal Methods
Что вы думаете про промежуточные варианты (типа Design-by-Contract + DSL)?
Мы смотрели в сторону формальных проверок, но пришли к выводу что они для нас запредельно дороги, потому что порог входа высокий и разработчику без магистерской степени объяснить тот же TLA+ очень затруднительно. Продать формальные методы команде тоже оказалось не просто. Критика была в духе: "код писать все равно надо", "это избыточность", "зачем писать спеку в странном псевдокоде", "лучше тратить время на ревью или тесты" и т.д. Это не говоря уже о том, что все эти инструменты допускают математически корректные, но семантически неадекватные (с точки зрения предметной области) модели. Последнее расстраивало архитекторов ("вот я написал абсолютную чушь, а TLA+ всем доволен", "мне теперь что, программировать на ТеХ-е?!", "к вашему птичьему языку надо еще страницу наратива на простом английском, потому что строгость есть, а семантики нет").
В итоге для критических вещей мы написали DSL компилятор на базе Scala, который генерирует гарантированно (ну, когда автор с командой не налажали) корректный код для структур данных и интерфейсов сервисов (с проверками целостности, инвариантами, трансформациями между представлениями и прочим) на нескольких языках. А программеры живут под DbC и доказывают друг другу корректность устно проверяя контракты на ревью.
Получилось по-моему не плохо. С одной стороны, пришлось пожертвовать универсальностью и строгостью, но с другой стороны удалось выйти за пределы "башни из слоновой кости" в поле, к "ремесленникам".
Продать это команде оказалось проще ("круто, я не должен писать тупой код и тесты к нему", "ура-валидация!", "картинки! Оно умеет клевые доки и картинки!11"). К тому же у нас теперь есть бюджет на развитие методов верификации, потому что использование генерации уже себя окупило много раз. В вашей терминологии это что-то вроде "мануфактуры", я полагаю ;-)
Что вы думаете про промежуточные варианты (типа 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 раз! меньше кода.
Спасибо!
Вот это дискуссионный вопрос. Мне кажется тут больше от мотивации разработчика зависит, чем от его степени магистра/бакалавра и пр
Вы правы, мне стоило бы написать подробнее. Вероятнее тут наша территориальная специфика (Кэмбридж). Мотивировать инженера можно двумя путями — либо показав, что это круто и крутые чуваки так делают, либо спустив разнарядку сверху. Первое, как я писал выше, у нас не зашло. Второе у нас плохо прокатывает в силу культурных особенностей. Американские инженеры очень пассивно-агрессивные. Магистры скорее всего как минимум натаскались на линейной алгебре и хотя бы раз видели либо теорию категорий, либо мат. логику, либо еще что-то, поэтому с интересом (или хотя бы уважением) относятся к формальным методам. Местные бакалавры часто и с алгеброй-то знакомы шапочно и в большинстве встают в защитную позу сразу как видят греческую букву. Так что феномен, на мой взгляд, присутствует, просто объясняется тем, что те, у кого аллергия на формальные вещи, часто не идут на магистра в CS.
нужно серьёзное внимание уделять корректности кодогенерации
Это да. Мы постепенно эволюционируем в этом направлении, и, кстати, количество поддерживаемого кода внутри компилятора постепенно снижается, по мере перехода не "правильные" методы.
что-нибудь а-ля http://smc.sourceforge.net/
Спасибо, посмотрел. Немного не в нашу сторону. Вывести корректный алгоритмический код у нас особых проблем не вызывает (пока). После того, как мы переехали на представление в виде графов, большая часть задач "сделать из того это" сводится к обходу графов и поиску по ним. Опять же с оговоркой, что мы прикладники.
PlantUML, Graphviz/Dot, Tex/Tikz? :)
Дык мы через них и генерируем. Сначала был PlantUML, потом пришлось от него отказаться (баги + на статических диаграммах далеко не уедешь). Сейчас делаем интерактивные диаграммы с использованием Graphviz с web assembly напрямую.
Хорошо мотивирует изучать TLA+ вот эта книжка...
Спасибо за наводку!
Мотивировать инженера можно двумя путями — либо показав, что это круто и крутые чуваки так делают, либо спустив разнарядку сверху.
Мне кажется путей мотивации всё-таки чуть больше. Например, что меня серьёзно мотивирует в формальных методах — это последующая экономия времени на отладку (отлаживать многопоточные приложения с плаващими логическими багами — это то ещё "удовольствие") и возможность, в случае model-checkers/model-finders, быстро проверять свои идеи.
Сейчас делаем интерактивные диаграммы с использованием Graphviz с web assembly напрямую
Спасибо за идею! Обязательно посмотрю подробнее. Для анимации взаимодействующих FSM'ок (интерфейсы/протоколы) возможно самое оно.
Про контракты + DSL + кодогенерацию?
Статей на самом деле по этой теме хватает, но если уважаемый borv напишет свою статью на эту тему, будет крайне интересно ознакомиться с его опытом.
Так как подход действительно рабочий и зачастую даёт очень хороший эффект (в плане качества ПО по отношению к затратам на разработку).
Хмм. Как минимум я давно хотел перевести нашу методичку по DbC для Хабра...
С материалами по DSL все сложно, на самом деле. Наше приключение с ним началось с пинка от CTO, что во многом определило вектор дальнейшего развития. Так сказать по баллистической кривой. Насколько далеко мы ушли от велосипеда сказать трудно. Пожалуйста не забывайте что мы прикладники ;-)
Про DSL что могу вспомнить сходу:
Есть несколько хороших статей про то, как запилить DSL на Scala. В основном вариации на тему этого.
С формализмом я ничего напрямую применимого не нашел, ходил NorthEastern University на кафедру PRL, поил пивом людей со смежными интересами. Про интерпретаторы написано очень много чего. А вот про статические структуры не очень. Предлагают брать классические работы по системам типов и выводить оттуда.
Есть очень смешная поделка baysick которая демонстрирует некоторые приемы комбинаторного DSL. Практической пользы в последнем — никакой, разумеется. Никто так интерпретатор Бейсика писать не будет. А вот всякие декларативные системы правил так пишутся на ура.
Про DbC — наша методичка начинается с отсыла к Бертрану Мейеру, так что наверное я бы начинал с него. Так же статья на вики, если хочется уж совсем на пальцах. Эйфель мы, конечно, не используем. У нас DbC адаптирован под Java и Scala.
Интересные ссылки.
Правда подход внутренних 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 возволяют гибко двигать границу между протестированным кодом и отверифицированным.
Со внутренними DSL — это из области "чем богаты, тем и рады". Если уж сильно приспичило, в той же Scala можно использовать макросы (та же идея — манипуляция AST в соответствующей фазе компиляции). А если совсем по-взрослому, то можно сделать плагин для компилятора. Или подождать пока уважаемые люди (Евгений Бурмако и компания) наконец определятся с поддержкой мета-программирования. Обещали завезти к 2020 в Scala 3.
В общем мы пытались, но потом решили отказаться. Работа с AST (в Scala) пока имеет два серьезных косяка, поэтому мы стараемся ее избегать:
- во-первых IDE ничего не знает про ваши изощрения с деревьями. Поэтому либо трансформация тривиальная (трансформированное дерево после компиляции соответствует типу из контекста. т.н. blackbox), либо отрубает практически все вещи которые любят разработчики — от подсветки синтаксиса до подсказок и рефакторинга (т.н. whitebox). Даже на среднем проекте (сейчас у нас все DSL определения занимают порядка 105K строк) это уже очень грустно. Встроенные DSL выражения таки являются корректными выражениями на "основном" языке, поэтому с ними такой проблемы нет.
- стоимость разработки новой фичи сильно растет, потому что надо заниматься разбором и трансформацией этих самых AST. Ну и верификацией всего этого кода, что тоже стоит дорого. Доказывать-то приходится трансформацию всего поля AST. А в Scala 2 деревья ого-го, и ко всему прочему с атрибутами и мутируемые. Короче вообще адъ и Израиль. Если немножко раскорячиться можно добиться того, что выражения DSL являются выполнимым и возвращают практически то, что нам надо, даже с грубой типизацией. Т.е. нам на этапе компиляции надо просто выполнить выражение и "допроверить" корректность. Мы так затащили подмножество SQL-92 внутрь нашего языка для поддержки маппинга таблиц и ETL ;-).
Про книжку Пирса совсем забыл. Огромное спасибо что напомнили!
во-первых IDE ничего не знает про ваши изощрения с деревьями.
Это да, при нетривиальном внешнем DSL все прелести IDE теряются :(
Ну, либо как вариант, сразу делать плагин к IDE хотя бы для подсветки синтаксиса (правда тут сразу возникает тесная привязка к конкретным IDE).
стоимость разработки новой фичи сильно растет, потому что надо заниматься разбором и трансформацией этих самых AST. Ну и верификацией всего этого кода, что тоже стоит дорого. Доказывать-то приходится трансформацию всего поля AST. А в Scala 2 деревья ого-го, и ко всему прочему с атрибутами и мутируемые. Короче вообще адъ и Израиль.
Со Scala я мало знаком (практически не знаком), но в Ocaml с этим не так страшно. Есть инструменты и либы, которые существенно облегчают задачу написания AST трансформеров. Ну и плюс к этому тайп-чекинг всё-равно потом делается, и совсем уж ерунду компилятор не пропустит. Если часть семантики закрыть на GADT + эмуляция поведенческих типов (это будет от пользователя спрятано и появится лишь в результирующем AST), то можно до какой-то степени быть уверенным и в семантической корректности кодогенерации.
Мы так затащили подмножество SQL-92 внутрь нашего языка для поддержки маппинга таблиц и ETL ;-).
Хорошо, когда синтаксис DSL вкладывается в синтаксис целевого языка :)
Одним из самых крутых языков (на мой взгляд) в этом смысле был CommonLisp с его reader macro, когда файл начинается как CommonLisp, а заканчивается как Pascal, после нескольких reader macro :)
Если часть семантики закрыть на GADT + эмуляция поведенческих типов (это будет от пользователя спрятано и появится лишь в результирующем AST), то можно до какой-то степени быть уверенным и в семантической корректности кодогенерации.
Мне кажется это очень близко к тому, что мы пытаемся делать. Да, хороших утилит много. Скажем так, если семантика DSL не сильно ушла от исходного языка, по сути все что мы делаем — это красивый синтаксис + проверки. Тут все ложится на стандартные средства и корректность доказать дешево. Грусть приходит с трансформацией выражений, особенно когда тип результата тоже выводится в процессе.
Боевой пример: схема + условный GraphQL на входе и строго-типизированный результат на выходе. Баги в этой штуке наиболее опасные и приводят к тому, что компилятор превращается в бредогенератор. Код на выходе практически всегда компилится (мы ж все вывели автоматом!) и проходит все статические проверки (у нас ведь отличный транслятор в Java!), полностью документирован (генератор документации тоже не подкачал!), но делает какую-то фигню (упс...).
Боевой пример: схема + условный GraphQL на входе и строго-типизированный результат на выходе. Баги в этой штуке наиболее опасные и приводят к тому, что компилятор превращается в бредогенератор. Код на выходе практически всегда компилится (мы ж все вывели автоматом!) и проходит все статические проверки (у нас ведь отличный транслятор в Java!), полностью документирован (генератор документации тоже не подкачал!), но делает какую-то фигню (упс...).
Про GraphQL не слышал, интересная вещь, посмотрю. Спасибо за наводку.
А что касается синтаксически правильных и правильно типизированных программ, которые делают какую-то фигню — тут уже начинается область семантики и проверки семантической корректности.
Весьма интересная область сама по себе.
Частично семантику можно переложить на типы (особенно сложные системы типов, GADT + эмуляция поведенческих типов, как уже упоминал, или пойти в хардкор: зависимые типы (но это уже весьма сложные дебри чего-то типа Coq, Agda, Idris и пр.))
Как идея: трансляция DSL в Coq, семантика определена заранее в либах Coq (ну не знаю, там например ввиде операционной семантики с малым шагом (автоматические тактики тогда хорошо работают) для предметной области), далее проверка выхлопа кодогенератора DSL->Coq в Coq'е полуавтоматическими тактиками, кодогенерация из Coq в целевой язык (сейчас, по-моему, поддерживает Haskell, Ocaml, scheme).
Но это весьма трудозатратный способ, и полностью автоматическую проверку семантической корректности сделать не получится в общем случае, там может требоваться и ручная работа. Хотя, если семантика простая и написать хорошие тактики, то можно практически всегда автоматически проверять.
Но это так, просто мысли вслух.
Что касается зависимых типов и ATP типа Coq и пр, то у меня весьма скромный опыт работы с ними, так что тут вряд ли чем-то серьёзно смогу помочь.
Ещё как идея: это попробовать использовать SAT/SMT солверы. DSL + контракты -> в формат для SMT и запуск SMT для поиска нарушений контрактов (контрпримеров). Подход а-ля Frama-C + why3 + WP plugin, или ADA/Spark + GNATProve.
В общем, когда начинаются задачи на проверку нетривиальной семантики, начинается самое интересное :)
Куча новых слов, спасибо. Буду изучать.
Ага, взаимно :) Тоже узнал много новых интересных слов :)
По поводу Coq и определения семантики, вспомнил про статью, которая мне очень понравилась, когда я ещё был RTL-инженером: https://arxiv.org/pdf/1301.4779v1.pdf
Она, конечно про верифицированный синтез железа из спец DSL, но подходы с софтовой верификацией очень близки.
Если есть интерес к хардкорной верификации, то могу рекомендовать: https://softwarefoundations.cis.upenn.edu/index.html
Там как раз про семантику софта и верификацию много информации.
Сейчас разработка серьёзного ПО уже немыслима без грамотного инженерного подхода. Facebook, Google, Microsoft, Amazon уделяют много внимания и сил разработке надёжных систем и ПО.
Ага, только для разработки таким методом — надо иметь бюджеты как у Gooogle и Amazon.
Или времени столько, сколько у NASA, когда никто не гонит за быстрый выпуск релизов.
В целом штука занятная, но практической пользы в обычном IT — примерно столько, сколько от интеграла в анекдоте про интеграл.
практической пользы в обычном IT
Проблема в том, что не бывает «обычного» IT. Все IT разное и в каждом случае можно и нужно использовать свои подходы. В определенных случаях (например, как в Яндексе) это все вполне применимо.
Видимо мне так и не удалось раскрыть основной посыл статьи: современные инструменты делают возможным применение формальных методов при небольших затратах на широком спектре практических задач.
И, если вы посмотрите материал по ссылкам в статье (особенно в блоге Hillel Wayne), вы увидите, что применять формальные методы можно довольно легко и в довольно многих областях разработки ПО.
Вопрос только в том, чтобы грамотно видеть, где применение каких инструментов принесёт наибольший эффект.
Ну и естественно, нужно небольшое знакомство с этими методами и инструментами (на что, в основном и направлена статья)
Чем формальные спеки лучше TDD, кроме того, что они хуже и быстро устаревают?
Ну тесты и спеки пока пишут люди. И там и там уровень детализации и покрытия требованиями даже близко к 100% не приближаются. Причем даже в формальных спецификациях слишком много подразумевается и мало декларируется. Даже из простейших примеров статьи это понятно. А ведь там по сути хелловорд специфицируется.
Насчет "неизвестно насколько" я бы поспорил. Анализ покрытия вполне себе точная метрика.
В общем случае — да, проблема останова нам гарантирует отсутствие универсального алгоритма проверки свойств системы. Но современные средства позволяют просматривать огромные пространства состояний за разумное время. Тот же самый 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% покрытие не может гарантировать сохранение контрактов и инвариантов в коде (этого можно добиться только перейдя к формальной верификации).
Тести и покрытие это хорошо, но этого часто бывает недостаточно даже для однопоточного кода.
Ну во-первых, спеки позволяют быстро проверить какие-то идеи и зачастую при меньших затратах, чем написание тестов и прототипов.
Во-вторых устаревание спек сопоставимо с устареванием тестов при изменении функционала/архитектуры и пр. Во всяком случае, на мой взгляд.
В-третьих, моделирование спек даёт такое покрытие, которое никакими тестами не достичь.
В-четвёртых, в распределённых (и параллельных) системах зачастую такое огромное пространство состояний, что любые тесты тут просто бессильны.
Ну и в-пятых, TDD и спеки совсем не являются антагонистами.
Напротив, формальные спеки очень хорошо сочетаются с любыми тестами, так как на основе спек мы можем делать направленные тесты, которые бы максимально учитывали краевые случаи в системе.
На самом деле идей много.
Начиная от того, что предикаты из спек перекладываются на assert'ы в коде и в тестах + (если используете property-based testing) по модели можно шейпить пространство состояний, проверяемое тестами (делать тесты более специфичными и направленными) и заканчивая методами, которые через итеративный процесс позволяют от абстрактных спек перейти к коду через последовательность уточняющих шагов со строгим доказательством сохранения более абстрактных в уточнённых (например, b-method и AtelierB, как инструмент для него).
Ещё можно использовать DSL, специально спроектированные для конкретных задач, которые позволят и модели получить и провести кодогенерацию из одного источника.
Арсенал на самом деле довольно большой, в каждой конкретной задаче, исходя из требуемой степени надёжности соответствия кода спекам, можно подобрать удобный подход и инструментарий.
Это два ортогональных подхода.
Формальная спека позволяет убедиться, что ваш код в совокупности корректен и не приводит в запрещенные состояния. Гарантий что он будет решать поставленную бизнес задачу вообще говоря нет (мы гарантируем что процесс заказа пиццы завершится семантически корректным заказом и что его жизненный цикл соответствует спецификации, а имеет ли этот процесс какой-то смысл мы сказать не можем).
TDD проверяет выполнимость отдельных кейсов. Гарантии в совокупной корректности нет (мы можем показать что заказ пиццы три сыра за 10.99 в условиях успешной оплаты сработал как ожидалось, но сделать из этого вывод что он сработает во всех остальных случаях не можем).
Формальная спека позволяет убедиться, что ваш код в совокупности корректен и не приводит в запрещенные состояния
Я бы уточнил: формальные спеки нужны в первую очередь для проверки алгоритмов, которые лягут в основу кода.
Закрыть формально путь от формальных спек к коду можно (чтобы гарантировать соответствие кода спекам), но это уже довольно сложно и дорого в общем случае.
Спеки в первую очередь позволяют не допустить серьёзных косяков в архитектуре, протоколах взаимодействия и тому подобных вещей.
Хорошо закрывает путь от формальных спек к результирующему коду подход Event-B и тулы типа AtelierB. Но там спеки не настолько высокоуровневые, как Alloy или TLA+ и заточены в основном на описании FSM'ок и их постепенного уточнения (с формальным доказательством корректности уточнения) вплоть до результирующей кодогенерации в Ada или C.
Только не абстрактная с проверкой «расчетов на графах»)
Такие абстрактные рассуждения большинство разработчиков просто не понимают, к сожалению.
А максимально приземленная. Например с рабочим кодом на Spring Boot и расчетами корректности алгоритма заказа пицы на Alloy. С разжевыванием «на пальцах» что с чем связано (как связано то, что пишется на Alloy с реальным рабочим кодом) и для чего это все делается в итоге. Т.е. в конце должен быть видимый эффект какой-то от возни с Alloy.
Тогда люди потянутся и будут рассматривать подробнее изложенное вами в статье.
А пока, к сожалению, большинство просто не понимает о чем речь и зачем все эти приседания на непонятном языке.
Я был бы очень рад ошибиться, но думаю большинство разработчиков просто не воспринимают фразы в духе
Тут мы проанализируем основные свойства, которыми должны обладать вычислительные графы, чтобы на основе графов можно было делать работоспособные системы.как что-то реальное, относящееся к их текущей работе. У них ведь ресты, интерфейсы, сервисы, дао, паттерны, а не вот эти вот ваши «вычислительные графы».
Надеюсь я понятно донес свой посыл)
Нужна новая статья, с подробным разбором создания вебсервиса, например тот же заказ пицы с оплатой, с применением подходов из статьи.
Да, это было бы хорошо.
Только я в основном бэкенд-разработчик, а до этого был системным программистом (а-ля уровня гипервизоров), а ещё раньше вообще логику для микрух и FPGA разрабатывал, поэтому чтобы мне сделать хороший пример со связкой ещё рабочего фронтэнд кода придётся потратить весьма приличное время просто на погружение во фронтэнд разработку.
Именно поэтому я и упомянул в статье блог Hillel Wayne и в частности его статью о применении Alloy при разработке UI. Чтобы люди, которым ближе фронтэнд смогли посмотреть пример и для фронтэнда.
Т.е. в конце должен быть видимый эффект какой-то от возни с Alloy.
Тема графов для микросервисов, начало которой приведено в данной статье, получила продолжение в реальности (как личный проект) и у меня сейчас есть уже наброски работающего прототипа. Возможно, в дальнейшем я и опубликую что-нибудь из продолжения работы относительно графов.
А пока, к сожалению, большинство просто не понимает о чем речь и зачем все эти приседания на непонятном языке.
Тут всё зависит от того, кому какая тематика ближе.
Для кого-то пример на основе фронтэндных задач будет тёмным лесом.
Но в целом да, фронтендеров больше (ну мне так кажется) и лучше было бы понятный пример из этой области.
Но, увы, от области фронтэнда я далёк. Могу только рекомендовать посмотреть блог Hillel Wayne.
Если будет достаточное множество желающих, возможно даже что-то из его блога я и переведу, дополнительно ещё разъяснив непонятные и тонкие моменты.
(если есть интерес к определённым темам, можно мне личку писать, я потом обобщу и в новых статьях постараюсь учесть интересы большинства)
У них ведь ресты, интерфейсы, сервисы, дао, паттерны, а не вот эти вот ваши «вычислительные графы».
А у меня на работе "вычислительные графы" и микросервисы :) Зависит от того, где
кто работает.
Надеюсь я понятно донес свой посыл)
В целом да. Во многом согласен с посылом.
Только, как мне кажется, у фронтендеров запрос на формальные методы и корректное ПО существенно меньше, чем у людей middle и back-end. Чисто ввиду того, что ошибки в бэкенде, на мой взгляд, дороже и сложнее в отладке (плюсовый многопоточный асинхронный код отлаживать намного менее приятно, чем JS для браузера).
придётся потратить весьма приличное время просто на погружение во фронтэнд разработку.
Rest сервис это не про фронт вообще) Во всем, что я описал, 146% бэкенда.
Rest сервис это не про фронт вообще) Во всем, что я описал, 146% бэкенда.
Да, у меня всё ещё немного смещено восприятие, так как бэкенд-разработчик я относительно недавно. После системного программирования, рест тоже больше ассоциируется с фронтом. :)
Бэкенд больше ассоциируется с какой-нибудь плюсовой многопоточкой, что-то похожее на вот такие вещи: https://github.com/vasil-sd/rendezvous-protocol
В общем, пока ещё я не силён в современной фронтэнд и бэкенд веб и мобильной разработке и могу в терминологии и классификациях технологий и фреймфорков что-то и путать (например, про Spring Boot в первый раз прочитал). :(
Хотя можно обойтись и серверной частью с каким-нибудь REST на базе OpenAPI.
enaml — интересная вещь, спасибо за ссылку!
Что касается более массового, то тут есть пара моментов:
Мне пока не понятно точно, кто в какой области работает из тех, что обратили внимание на статью. То есть, нет понимания того, что было бы интересно большинству
Чтобы грамотно написать пример близкий к реальности из какой-либо области, нужно до какой-то степени знать эту область и понимать её специфику.
В общем я пока в размышлениях относительно того, чтобы такого написать более массового и близкого к реальности.
Есть идея следующую статью посвятить решению одной небольшой реальной задачи из области бизнес-логики и баз данных с использованием TLA+.
Там была проблема, которая тестами практически не ловится, но было интуитивное понимание того, что определённый код может работать некорректно.
Сделали модель и на модели явно нашли ошибку в алгоритме работы.
Теперь нужно убедиться, что модель отражает код (направленный тест по трассе ошибки из модели) и если так, то думать, как исправить алгоритм или как сделать аккуратные костыли (работу которых тоже нужно будет проверить на модели).
Там получается как раз: и модель небольшая, самое оно для учебной, и задача реальная.
У меня есть не очень пока проработанная идея минималистичного децентрализованного мессенджера, но это всё-таки специфичная задача.
У меня есть не очень пока проработанная идея минималистичного децентрализованного мессенджера, но это всё-таки специфичная задача.
А что в основе планируется? DHT? Kedemlia?
Только текстовые сообщения, может чат-группы (но частично децентрализованные — хостяться у того кто создал, иначе слишком много коннектов нужно всем держать)
Вобщем для тех кто хочет иметь реально безопасный мессенджер (который реально могут проверить на закладки практически все) и реально независящий от каких-то коммерческих компаний (для тех кто устал менять мессенжеры и иметь их миллион не зная какой лучше в итоге будет).
Интересные идеи по ссылке.
Насчёт DHT — лично мне очень понравилась Kademlia, показалась наиболее понятной и простой в реализации (ну и судя по количеству проектов на её вариациях, видимо у многих такое же мнение).
Но пока сомнительно, что найду в обозримом будущем на это время, приоритет за другими вещами, кстати, там есть раздел и на тему других моих идей про ИТ, про всякое децентрализованное голосование, именно из-за них меня интересуют темы всякой верификации.
Если делать инструмент децентрализованной демократии, то его важность столь высока, что без формальной верификации не обойтись.
- Юзеры не знают, чего они хотят — мы должны сделать продукт и предложить им, а они уже заценят.
- Заказчик не знает, сколько времени и денег он готов вложить в продукт, поскольку не понятно, насколько он «зайдёт»
- Программисты не знают, насколько сложно (и возможно ли вообще) будет реализовать часть фич
В итоге лишь малая часть фич может быть специфицирована, остальные реализовываются по ходу дела исходя из пересечения множеств «оказалось затребовано пользователями» и «оказалось возможно реализовать». Но сами эти множества очень динамичны и вообще не существуют до выпуска первой версии продукта.
Я уже частично написал в комментариях ответы на эти вопросы, но повторюсь ещё раз:
У любых методов, и формальные тут не исключение, своя область применения и критерии применимости.
Нужно ко всему подходить разумно и формальные спеки использовать именно там, где они дадут выигрыш.
Для того, чтобы понимать где и какие формальные методы можно применять, нужно немного с ними ознакомиться, на что и направленна данная статья (ну и будущие статьи)
Далее, ответы на приведённые аргументы:
Юзеры не знают, чего они хотят — мы должны сделать продукт и предложить им, а они уже заценят.
Во-первых, я уже упоминал, что есть хорошие методы и инструменты для работы с требованиями, которые могут помочь в работе даже с быстро-меняющимися требованиями.
Во-вторых, вряд ли требования у пользователей меняются настолько кардинально, что нельзя даже выделить и абстрагировать ядро функционала, нужного пользователю.
В-третьих, многие вещи с пользователями можно обсуждать на основе моделей и результатов моделирования (например, логику работы UI в виде состояний недетерминированных FSM'ок, нужно только выбрать подходящее, понятное для пользователя графическое представление). Это может оказаться существенно быстрее, чем писать и выкидывать прототипы.
Заказчик не знает, сколько времени и денег он готов вложить в продукт, поскольку не понятно, насколько он «зайдёт»
Ну тут могу только повториться: нужно хорошо понимать где и какие методы и инструменты применять.
И если у вас стартап по написанию игрушки для андроид на деньги венчурного фонда, то тут да, формальные методы и спеки могут быть излишни.
Программисты не знают, насколько сложно (и возможно ли вообще) будет реализовать часть фич
А вот тут формальные спеки, на мой взгляд, зачастую могут помочь с более точной оценкой, так как вероятность ошибок, которые могут повлечь большие объёмы работы — архитектурных и подобных им, становится меньше.
выдавливание инженерного подхода из ИТ приносит хорошие деньги
Это весьма спорное утверждение, хорошие деньги в краткосрочной перспективе приносит найм дешёвых низкоквалифицированных разработчиков, да и то не во всех областях. А вот в долгосрочной перспективе это дорогой и зачастую смертельный для бизнеса подход.
Крупные игроки это уже поняли и сейчас опять восстанавливают серьёзный подход к разработке, но уже на другом уровне, стараются по-прежнему экономить на массовом разработчике, но при этом активно развивают инструменты в рамках групп высококвалифицированных разаработчиков, которые (инструменты) бы позволили снизить требования квалификации к большинству разработчиков (reason, Go, typescript, множество тулов стат. анализа кода и тд.)
Ну и активно используют инженерные методы разработки для наиболее чувствительных частей системы (в конце статьи много ссылок на это).
То есть, определённое понимание есть у некоторых крупных игроков на ранке ПО по поводу того, что нужно иногда софт разрабатывать с серьёзным подходом.
Мотивация думать, развиваться, создавать и творить сведена, можно сказать, к нулю.
Ну тут тоже не всё так однозначно плохо. Например, многие менеджеры (даже топы из весьма крупных компаний) активно изучали/изучают опыт Semco (могу рекомендовать книги Рекардо Семлера "Маверик" и "Выходные всю неделю").
Надеюсь его опыт будет потихоньку перениматься в корпорациях, так как он показал на практике, насколько можно эффективно мотивировать людей, на развитие и работу.
Потом получается: ты его просишь пересмотреть модель в его же коде с учетом изменения бизнеса, а он не помнит что и для чего вообще делал, не то что что-то предложить, т.к. смещены приоритеты и ценности и ему это неинтересно. А ты его уволить не можешь, т.к. менеджменту он выгоден, как дешевый ресурс.
Ну тут проблема менеджмента. Обычно проекты, где менеджеры допускают такой подход к разработке (а особенно, если в результате код на выходе получается не поддерживаемый и не сопровождаемых, то есть с плохим bus-factor), долго не живут.
2, 3. Как раз спеки позволяют сделать дстаточно адекватные оценки.
Но давайте вспомним, что включает спецификация? 7 состояний и десяток переходов. Всего пара десятков элементов. Всего!
В реальности сложные задачи оперируют сотнями, а то и тысячами элементов. Простейший случай — связываем текстовое поле с БД. Одно единственное текстовое поле. Начнём с БД — нужна собственно база (где-то уже установленная), нужна связь с ней, нужны логины/пароли, нужна таблица значений, нужен селект конкретного значения, нужно чтение результатов селекта, нужно положить прочитанное в поле, нужно прочитать из поля в нужный момент, запихнуть в апдейт (который нужно написать), правильно выполнить апдейт, показать юзеру некий фидбэк. Вот такой самый минимальный минимум. Ради одного поля. Без логики. Только лишь тупое копирование.
В целом призыв «давайте наконец будем думать» выше уже нашёл подходящий ответ — думать дорого. Хотя и без комментариев давно было ясно, что доказывание свойств программы — совсем не панацея. Да, некоторые программы (точнее их крохотные части) действительно доказывают, но сколь велика пропасть между этими крохами и всем остальным миром!
Поэтому призыв стоит подавать хотя бы с указанием на его очень и очень узкую область применения. В реально массовом софте что-то подобное будет воспринято лишь в одном случае — когда не будет нужды думать. Вы не заметили противоречия? Призыв «подумать» может быть реализован лишь если есть возможность не думать.
Как некий предварительный шаг в сторону инструмента, который сделает за разработчика большую часть работы, такой подход уместен. В неких узких и очень дорогих нишах такой подход так же может быть применён. Но всё остальное (99.99%) — не из этой оперы. И это — главное, что стоило донести в статье.
Но давайте вспомним, что включает спецификация? 7 состояний и десяток переходов. Всего пара десятков элементов. Всего!
Многие спецификации реально важных алгоритмов (Chord, Paxos и тд) тоже не сильно большие.
В реальности сложные задачи оперируют сотнями, а то и тысячами элементов. Простейший случай — связываем текстовое поле с БД. Одно единственное текстовое поле. Начнём с БД — нужна собственно база (где-то уже установленная), нужна связь с ней, нужны логины/пароли, нужна таблица значений, нужен селект конкретного значения, нужно чтение результатов селекта, нужно положить прочитанное в поле, нужно прочитать из поля в нужный момент, запихнуть в апдейт (который нужно написать), правильно выполнить апдейт, показать юзеру некий фидбэк. Вот такой самый минимальный минимум. Ради одного поля. Без логики. Только лишь тупое копирование.
Зачастую нет смысла делать такие детальные спеки. Выше где-то в комментариях, я уже писал о важном навыке — грамотно проводить уровни абстракции.
Зачастую действительно важные и критичные свойства системы можно проверить на весьма абстрактных (и соответственно небольших) спеках.
Зачем делать детальную спеку БД, записей, сетевых соединений и пр, если цель — проверить корректность алгоритма аутентификации пользователя?
Это один из вопросов, которые должны решать разработчики для грамотного применения формальных методов — понимать где и на каком уровне абстракции их применять.
В целом призыв «давайте наконец будем думать» выше уже нашёл подходящий ответ — думать дорого.
Вот я как раз и преследую цель данной статьёй — показать, что эта фраза и этот стереотип немного устарели. Думать сейчас стало намного дешевле с современной инструментальной поддержкой.
Хотя и без комментариев давно было ясно, что доказывание свойств программы — совсем не панацея.
Методов и инструментов широкий спектр. Доказывание свойств программы — это отдельная ветвь формальных методов и самая трудоёмкая.
В статье речь идёт не о формальной верификации программ. А о применении инструментов класса model-finders для исследования прототипа архитектуры.
Как некий предварительный шаг в сторону инструмента, который сделает за разработчика большую часть работы, такой подход уместен. В неких узких и очень дорогих нишах такой подход так же может быть применён. Но всё остальное (99.99%) — не из этой оперы. И это — главное, что стоило донести в статье.
Если честно, складывается ощущение, что статью вы только просмотрели по заголовкам. Ибо я про верификацию программ только вскользь упоминал. Основная часть статьи — это применение Alloy для исследования свойств архитектуры решения из области организации микросервисной системы.
В неких узких и очень дорогих нишах такой подход так же может быть применён. Но всё остальное (99.99%) — не из этой оперы. И это — главное, что стоило донести в статье.
Давайте сначала вы всё-таки более внимательно посмотрите статью, а потом уже думаю можно будет обсудить её более детально и предметно.
Так как именно такие стереотипы (как вышепроцитированное утверждение) я и пытаюсь немного развеять.
Сложный UI критичен весь. Юзеры должны работать не отвлекаясь на косяки программистов, но в какой-нибудь социальной сети мы встретим под сотню всяких формочек, приспособленных под ту или иную ситуацию, и каждая форма должна корректно взаимодействовать с пользователем. Иначе — негативное восприятие соц.сети и уход пользователей. И вот в такой ситуации — сколько времени потребуется вам лично для вникания во все эти сотни формочек, построения моделей, верификации и т.д.? Просто прикиньте, а потом просто будьте честными сами с собой. А после верификации программисты добавят массу ошибок реализации. Так есть ли вообще хоть какая-то выгода?
>> В статье речь идёт не о формальной верификации программ. А о применении инструментов класса model-finders для исследования прототипа архитектуры.
Ну скажем честно — model-finders ничего не находят. То есть вы сами создаёте (находите) модель, и только потом запускаете некие выборочные алгоритмы верификации. Это во первых. И во вторых — в статье как раз и идёт речь о верификации программ. Просто вы используете слово «алгоритм» для обозначения чего-то маленького, вроде бы доступного по цене, но при этом область верификации программ всего лишь декларирует цель максимум в виде полной программы, когда в реальности занимается именно узкими и маленькими алгоритмами, в точности как у вас в примере.
>> Основная часть статьи — это применение Alloy для исследования свойств архитектуры решения из области организации микросервисной системы.
Ну какая разница, как называется инструмент и как выглядят его команды, если он именно что занимается стандартным подходом, определяемым названием «верификация программ»? Да, инструмент использует не весь аппарат верификации, ну и что? Да, вы сами пишите скрипты верификации, но суть-то от этого почему изменилась? Вы показали ручной вариант верификации, но алгоритм «модель-проверка» никуда от этого не делся.
Ну какая разница, как называется инструмент и как выглядят его команды, если он именно что занимается стандартным подходом, определяемым названием «верификация программ»? Да, инструмент использует не весь аппарат верификации, ну и что? Да, вы сами пишите скрипты верификации, но суть-то от этого почему изменилась? Вы показали ручной вариант верификации, но алгоритм «модель-проверка» никуда от этого не делся.
Знаете, мне сложно дискутировать на таком уровне. Разговор в таком ключе мне представляется довольно беспредметным и неконструктивным.
Программа/алгоритм/модель и пр — это всё существенно разные понятия, и смешивать их в одну кучу — совсем не правильно.
Верификация программ, проверка моделей, вероятностная проверка моделей, поиск моделей и др — это всё существенно разные методы и инструменты, которые имеют разные (возможно, где-то немного пересекающиеся) области применения.
Если честно, то model-checkers/model-finders — это не совсем про соф (даже совсем не про софт), а про любые системы, которые описываются формализмами, на которых базируется тот или иной инструмент. Например, TLA+ используется для проверки корректности не только софта, но и железа (когерентность кэшей, например).
Alloy можно использовать для исследования всевозможных структур, например, конфигурации топологий машин в сети и тд.
Если есть желание дискутировать в конструктивном русле с нормально применяемой терминологией, без смешения и подмен, то всегда с удовольствием, но в текущий момент в данной ветке дискуссии никакой пользы ни для кого я не вижу, уж извините.
Как вам будет угодно. Но всё, что вы описали, на 100% относится к верификации программ. Только инструменты самодельные да плохо автоматизированные. В нормальных же инструментах код доказанной программы генерируется автоматически, а уровень используемых абстракций заметно выше, нежели простейший автомат. Ну и естественно, алгоритмы работы железных модулей там прекрасно доказываются.
Есть "пример успеха": Hyper-V был формально верифирован для Microsoft.
Как это вписывается в вашу "картину мира"?
( А "сотни формочек" генерировались в Clarion из схемы БД ( .dct ) ещё в 90х.
И если сейчас это стало трудоёмкой задачей, то где прогресс средств разработки? )
Как я и писал выше — 99.99% софта не создают и не будут создавать в ближайшем будущем по такой технологии.
>> А «сотни формочек» генерировались в Clarion из схемы БД
Вы, видимо, просто не видели эти формочки в социальных сетях. Поглядите, расширите кругозор. Ну и можете попробовать сгенерировать хоть одну с помощью Clarion — будет очень поучительно.
В реально массовом софте
Решим задачу в стиле отдела кадров Google:
на первом месте 4 миллиарда Android OS, поделим на 3, пусть на 5 или 16, получим примерно долю Windows с включённым Hyper-V ( см. "device guard"). И не забудем прибавить мощности Azure.
Т.о. пример верифицированного массового ПО найден.
В нормальных же инструментах код доказанной программы генерируется автоматически
Не затруднит чуть подробнее? URL или менее общую терминологию ( для поиска ) ?
после верификации программисты добавят массу ошибок реализации
При генерации из создаваемых программистом в RAD среде Clarion "связке" .app + .dct файлов исходного кода ничто не мешает генерировать и пред- и постусловия, инварианты циклов и т.п.
( Т.е. большой объём кода, если он более менее типичный — не препятствие )
Вы, видимо, просто не видели эти формочки в социальных сетях
Скажем так: если и видел, то не оценил в чём их сложность: в количестве полей? в нестандартных элементах?
( Если последнее, то у C. есть и конкуренты: например, французская разработка. )
Т.к. если в логике обработки, то инженерный подход, как раз, будет не лишним.
Ну если ваша цель — победа, то вы, безусловно, победитель.
>> чуть подробнее?
Гуглите isabelle theorem prover. От него по встретившимся терминам найдёте массу аналогов.
>> большой объём кода, если он более менее типичный — не препятствие
Так вы уже сгенерировали свой фэйсбук или только теоретически доказываете, что вам это раз плюнуть?
>> если в логике обработки, то инженерный подход, как раз, будет не лишним.
И снова здравствуйте! Ждём следующей встречи после генерации аналога фэйсбука с применением инженерного подхода. Вы завоюете мир в один миг, стоит только всё правильно сгенерировать и инженерно подойти.
Гуглите isabelle theorem prover. От него по встретившимся терминам найдёте массу аналогов.
Рад, что вы знакомы с ATP. Но это только небольшая часть инструментария для инженерного подхода.
И применение ATP:
- Очень дорогое, требующее высокой квалификации
- Подходит только для весьма узких задач (докажите мне пожалуйста корректность алгоритма Paxos с помощью Isabelle/HOL)
- Требует частого ручного вмешательства пользователя в ходе доказательства свойств ПО (ну да, после этого кодогенерация автоматом, хотя и то, только для определённого подмножества целевого языка и как правило ещё и с хаками системы типов этого целевого языка (здравствуй obj.magic в Ocaml и аналоги в Хаскеле), либо генерация в бестиповый ЯП, типа scheme)
Ну вот, а вы давеча говорили, что инструмент, мол, стал доступнее…
>> докажите мне пожалуйста корректность алгоритма Paxos с помощью Isabelle/HOL
А вы на автоматах с помощью указанных в статье инструментов это сможете? В смысле асинхронный обмен в них вообще поддерживается?
А вообще по асинхронности и доказательству теорем в сети много данных, например такие или такие.
И да, даже если некое частное решение всё же можно сделать на ваших инструментах, то всё равно это бесконечно малая часть от реальной потребности. Ну хоть с этим-то вы согласны?
Ну вот, а вы давеча говорили, что инструмент, мол, стал доступнее…
Вы специально троллите? Или просто настолько невнимательно читаете?
Писал в статье я про класс инструментов, которые весьма существенно отличаются от ATP. Приравнивать Isabelle/HOL к Alloy — это показывает полную неосведомлённость в вопросе.
И в первую очередь про инструменты классов model-checkers/model-finders я говорил, что они стали намного удобнее и доступнее.
А вы на автоматах с помощью указанных в статье инструментов это сможете? В смысле асинхронный обмен в них вообще поддерживается?
Paxos:
TLA+: https://github.com/bringhurst/tlaplus/tree/master/examples/Paxos
Isabelle/HOL: https://www.isa-afp.org/browser_info/current/AFP/DiskPaxos/outline.pdf
Сравните сложность. Думаю разница явно видна. И доказательство в Isabelle/HOL появилось спустя много лет TLA+ модели. И, что самое забавное, базируется именно на TLA+ модели.
И да, даже если некое частное решение всё же можно сделать на ваших инструментах, то всё равно это бесконечно малая часть от реальной потребности. Ну хоть с этим-то вы согласны?
С чем согласен? С вашими утверждениями, которые непонятно на чём основаны с учётом того, что вы вообще не вникаете в ответы на ваши комментарии и не читали статью (есть веские основания это полагать)?
Перечитайте свой предпоследний ответ. Там ясно написано — всё сложно и методов много. Собственно об этом я с самого начала и говорил, но вы упирались, а потом (в предпоследнем ответе) всё же согласились. Хотя да, теперь вы опять отказались, поскольку, оказывается не вы мне невнятно объяснили, но это я вас с самого начала плохо понимал и вообще даже статью не читал.
Собственно по статье (по пользе от неё). Вы там пишете про конкретику, по совершенно ненужный синтаксис и тому подобные детали, но не описываете сущность применяемого подхода. Такой стиль, понятно, принят во многих статьях, но это не значит, что он правильный. Этот стиль позволяет провести совсем ничего не понимающего пользователя по примитивным шагам, после которых пользователь, возможно, хоть чуть-чуть ощутит смысл всего сказанного. При этом «хоть чуть-чуть» чаще всего выражается в простейшей способности запустить рекламируемое чудо. То есть все шаги, обычно, просто показывают в деталях, как банально запустить игрушку, ну и попробовать поиграться. Вот и вы всё подали в таком же стиле, хотя по вашей же ссылке на статью некоего американца (как-то относящегося к рекламируемым вами инструментам) он довольно внятно и коротко объясняет — я делал сайтик, потом взглянул на него с точки зрения конечных автоматов, потом построил модель автомата и проверил возможные переходы состояний, после чего получил результат, позволивший существенно улучшить сайтик (некоторые страницы были очень далеко, что-то ещё там было нелогично). Ну и после его пояснения я просто пролистал дальше ваш текст, потому что искал суть, а вы всё какие-то синтаксические детали на меня изливали.
Вот взгляните даже на элементарное введение вами ваших инструментов — вы просто даёте некий англицизм и больше ничего не говорите! Ни-че-го! Типа все и так знают, что за прекрасную игрушку им сейчас покажут. Но это же бред! Вы знакомите людей с новой для них технологией, и начинаете сразу с запутывания. Вместо пояснений о природе инструментов, вы просто даёте название и далее, примерно как в мифах про богов, рассказываете про какие-то магические свойства персонажей. При этом — как это всё работает, вы не поясняете. Ну и зачем мне такая статья? Мне что, рекламы в интернете мало, что бы ещё и ваш рекламный текст самостоятельно дешифровывать и выводить из него те тайны, про которые вы не захотели рассказать?
Общие принципы я вам выше показал, вы мне в ответ начали про «я не читал статью». То есть с принципами вы не спорите, с ними согласны, но тогда зачем мне всё остальное? Если принципы я понял правильно, то уж инструмент выбрать я смогу, и при этом мне совершенно не обязательно опираться на некие примеры синтаксиса, приведённые вами. Мне не синтаксис нужен, мне нужна целостная картина применения инструмента, с упором на сокращение затрат на том или ином этапе разработки. И вот этого у вас просто нет (ну кроме заявлений про «инженерный подход творит чудеса»).
Там ясно написано — всё сложно и методов много. Собственно об этом я с самого начала и говорил, но вы упирались, а потом (в предпоследнем ответе) всё же согласились.
По поводу высокой сложности, я имел ввиду ATP, к которым вы почему-то стараетесь всё свести. А model-checkers/model-finders это как раз относительно легко и при небольшой сноровке можно широко применять.
Собственно по статье (по пользе от неё). Вы там пишете про конкретику, по совершенно ненужный синтаксис и тому подобные детали, но не описываете сущность применяемого подхода.
Это да, изначально статья планировалась существенно больше, но тогда охват аудитории был бы ниже. Я же в самом начале написал, что эта статья для привлечения внимания, причём, чтобы большинству разработчиков было интересно, в статье максимум конкретики и примеров, чтобы можно было самим поиграться.
Если бы я начал расписывать SAT/SMT солверы + Kodkod + детальное изложение реляционной логики первого порядка с операторами транзитивного замыкания и join + особенности трансляции всего этого в код задач для SAT/SMT солверов + особенности работы kodkod — кто бы это всё стал читать? 1-2 человека?
И от расписывания внутренностей специально в этой статье старался держаться подальше, ибо хотел показать разработчикам как выглядит именно пример применения Alloy, а не расписать, что у него внутри, как к нему писать плагины, как вызывать kodkod и какие особенности трансляции атомов из kodkod в формулы для SAT солверов.
он довольно внятно и коротко объясняет — я делал сайтик, потом взглянул на него с точки зрения конечных автоматов, потом построил модель автомата и проверил возможные переходы состояний, после чего получил результат, позволивший существенно улучшить сайтик (некоторые страницы были очень далеко, что-то ещё там было нелогично)
Во-первых, я специально дал ссылку для тех, кто захочет подробнее посмотреть на примеры близкие к реальности применения формальных методов.
Во-вторых, он хоть и взял модельный пример из реальной работы, но для статьи его очень сильно упростил.
В-третьих, в статье он делает сильный акцент на какой-то сторонний ресурс для моделирования формочек, а именно про применение самого Alloy у него в той статье очень мало.
Я же решил акцент сместить на применение самого инструмента, именно для того, чтобы лучше показать как с ним работать.
Вместо пояснений о природе инструментов, вы просто даёте название и далее, примерно как в мифах про богов, рассказываете про какие-то магические свойства персонажей. При этом — как это всё работает, вы не поясняете. Ну и зачем мне такая статья?
Цель статьи я обозначил прямо в самом начале: привлечь внимание разработчиков к инструментам определённого толка, которые могли бы им помочь в их работе.
Для тех, кто захочет изучить предмет статьи подробнее, дано много ссылок на разные материалы по теме.
Кроме того, планируются ещё статьи, возможно с более глубоким погружением в детали технологий.
То есть с принципами вы не спорите, с ними согласны, но тогда зачем мне всё остальное?
С какими принципами? Чтобы с чем-то спорить или соглашаться это должно стать предметом дискуссии и быть чётко выраженным.
На текущий момент я вижу непонятную критику того, что я якобы не объяснил, как всё работает, хотя цель статьи была заявлена в самом начале и там ничего про объяснение принципов работы не было.
Мне не синтаксис нужен, мне нужна целостная картина применения инструмента, с упором на сокращение затрат на том или ином этапе разработки. И вот этого у вас просто нет (ну кроме заявлений про «инженерный подход творит чудеса»).
Я бы и сам не против написать детальную статью со всеми ньюансами (в том числе и подкапотными технологиями в основе инструментов) и детальным примером применения с отсылками к промышленному опыту. Но сколько людей смогут прочитать такую статью и осилить? Огромное количество людей изобилие в подобной статье внутренних деталей того же самого Alloy просто отпугнёт. И вместо того, чтобы показать пользу, лёгкость применения и удобство формальных инструментов, я просто всех распугаю и поддержу миф, что нормальная разработка ПО и систем это суперсложно, супердорого и пр.
PS: Ещё раз отдельно для вас: детали внутренностей Alloy можете посмотреть тут, тут, тут, тут ну и по инету много других публикаций.
Все эти инструменты сводятся к перебору вариантов, полученных на основе некоторых ограничений. Хотя название для каждого инструмента может уводить в сторону неких привычных подходов, вроде конечных автоматов. Но независимо от способа описания модели (задания ограничений), мы всё равно имеем простой перебор вариантов. Если вдаваться в математику и доказывать что-то про исследуемый перебор, то получим весьма отдалённые друг от друга направления, которые даже занимающиеся ими математики не всегда охватывают полноценно. Поэтому мне сдаётся, что вы несколько застряли в рамках какого-то одного направления, а другие для вас кажутся не вполне понятными, ну и поэтому вы стараетесь их отделить друг от друга. Но на самом деле вы отделяете известные вам подходы к построению переборных задач от мало изученных.
Я сам тоже глубоко во все направления не вникал, но суть, которую я всё же уловил, подсказывает мне, что во всех случаях модель задаёт ограничения, а далее лишь модифицируются алгоритмы обхода вариантов, укладывающихся в ограничения. Поэтому я и говорю, что подход-то всего один — задаём ограничения и перебираем варианты. И те же theorem provers тоже при некоторой сноровке применять легко, просто потому, что там тот же самый принцип.
В примере про сайт был применён подход на основе конечных автоматов, то есть ограничения задавались автоматом, а алгоритм обхода затачивался на перебор состояний. В theorem provers используется более сложная модель (хотя есть и такие, где моделью является чистая логика первого порядка), но это всего лишь способ задать ограничения для алгоритма. А после задания ограничений имеем всё тот же перебор — на основе модели алгоритм перебирает допустимые варианты. Общая логика такая — сгенерировать вариант, проверить на соответствие модели (ограничениям), если всё соответствует — получен вариант решения. И это всё, как вы сами видите, можно объяснить простыми словами, аудитория для которых может быть очень широкой. Вот в примерно таком стиле я и хотел бы видеть действительно достойную статью. Ну а математику можно просто пропускать, как вы сами это делали в институте, когда вам давали лишь инженерные основы, то есть рабочий математический инструмент, а доказательство его работоспособности вам в учебниках не показывали, поскольку это превратило бы вас из инженера в математика.
>> Если бы я начал расписывать SAT/SMT солверы + Kodkod + детальное изложение реляционной логики первого порядка с операторами транзитивного замыкания и join + особенности трансляции всего этого в код задач для SAT/SMT солверов + особенности работы kodkod — кто бы это всё стал читать? 1-2 человека?
Вот поэтому я выше и показал примерно, как могли бы выглядеть именно инженерные рассуждения, то есть оставленные без доказательств в некой полезной статье, но опирающиеся на серьёзную работу математиков, которую желающие изучат самостоятельно.
>> Цель статьи я обозначил прямо в самом начале: привлечь внимание разработчиков к инструментам определённого толка
Так проблема в том, что без понимания принципов работы, мало кто заинтересуется. Для них это будет просто некая магия, которую совершенно непонятно, как применять.
Тот же SAT-solver штука очень простая — есть формула и надо подобрать такие значения переменных, что бы формула давала значение true. Ну куда проще? Тривиально же! И почему этого нельзя пояснить в статье?
Точно так же часть ваших инструментов поясняется простейшим расшифровыванием сути — они формируют логическую формулу на основе ограничений, а потом ищут перебором варианты значений переменных в формуле. При этом собственно переход от модели к логической формуле в каждом случае точно так же весьма прост, но поскольку самих моделей напридумано на данный момент множество, пояснять все, конечно же, долго, да и не реально, поскольку мы многих просто не знаем. Но хотя бы переход от модели к логической формуле конкретно для вашего инструмента вы могли бы показать? Ведь вам понятен (надеюсь) инструмент, вы даже утверждаете, что понятна стоящая за ним математика, так почему нельзя по простому показать это банальное отображение модели на формулу с последующим указанием на суть перебора значений для полученной формулы?
о хотя бы переход от модели к логической формуле конкретно для вашего инструмента вы могли бы показать? Ведь вам понятен (надеюсь) инструмент, вы даже утверждаете, что понятна стоящая за ним математика, так почему нельзя по простому показать это банальное отображение модели на формулу с последующим указанием на суть перебора значений для полученной формулы?
Цель была другая совсем. Хотел привести именно пример использования инструмента, а не расписывать внутренности и математику.
Когда машину показывают среднестатистическому покупателю, ему же рассказывают про то как её клёво использовать, как она быстро ездит и как удобно ею рулить, а не про принципы двигателей внутреннего сгорания и как программировать микроконтроллеры в управляющей электронике, правильно?
Так же и эта статья призвана показать использование инструмента, а не математику и эвристики SAT-солверов (кстати, SAT только на первый взгляд простые, а на самом деле там огромное количество ньюансов, начиная от эвристик по выбору порядка переменных при построении BDD на основе формулы до эвристик по оптимизации формулы и тд.), то в ней и не уделялось внимание подкапотному пространству.
Если увижу, что многим людям интереснее про математику и внутренности тулов, то может напишу статьи и про это.
Можете сказать, насколько реально и целесообразно на данный момент использование данного подхода, скажем в обычном клиент — серверном решении (мобилка + сервер, например). Например, клиент запросил сервис по доставке еды — имеет в этом случае писать спеки и создавать модели?
Или, скажем, чуть более сложный заказ: клиент хочет разработать систему умного дома, имеет ли это смысл в этом случае? Если да, то можно ли увидеть пример?
Создание математической модели для алгоритма это одно, у тебя есть входные параметры, их область применения, это все очень похоже на математику и ее теоремы. А вот с бизнес логикой, где много висящих хвостов, ad hoc параметров все выглядит иначе.
Спасибо за статью!
Пожалуйста! Рад что статья оказалась интересной.
В последнее время попадаются статьи на хабре, обосновывающие пользу спеков и моделей. Много слов сказано про новое ПО, которое удешевит инженерный подход. Но все примеры которые я нахожу связаны с довольно узким спектром задач. В большинстве проектов в IT и алгоритмы то никакие не используются, не считая библиотечных.
Могу посоветовать посмотреть блог Hillel Wayne, по поводу того какие в каких задачах может быть применёны model-checkers/model-finders. Там много простых примеров из разных областей. А его книга Practical TLA+ начинается с самого что ни на есть примера именно из бизнес-логики: пересылка денег между счетами.
Можете сказать, насколько реально и целесообразно на данный момент использование данного подхода, скажем в обычном клиент — серверном решении (мобилка + сервер, например). Например, клиент запросил сервис по доставке еды — имеет в этом случае писать спеки и создавать модели?
На вскидку, где я вижу применение моделей:
Промоделировать логику работы пользователя с системой на общем уровне, с целью найти неоптимальные последовательности действий пользователя с точки зрения важности востребованности функции для пользователя и сложности её реализации в протоколе работы пользователя с системой (грубо говоря, чтобы система следовала принципу наименьшего удивления пользователя).
Промоделировать сущности в системе и их взаимосвязь, с целью исключить какие-либо неправильные конфигурации в системе.
Промоделировать протоколы взаимодействия модулей в системе, чтобы посмотреть, нет ли каких-нибудь неочевидных/невалидных состояний (как пример, из-за сбоя в подтверждении запроса от одного модуля к другому, система зациклилась и начала пользователю складывать в цикле блюда в корзину из-за ретраев).
Это всё делается весьма быстро и малозатратно при определённом уровне навыков, но при этом может существенно повысить качество системы и user experience.
Или, скажем, чуть более сложный заказ: клиент хочет разработать систему умного дома, имеет ли это смысл в этом случае?
Тут примерно то же самое, что и в предыдущем пункте: самое быстрое и простое — это промоделировтаь логику работы пользователя с системой, с целью недопущения ситуаций, когда для включения лампочки нужно системе дать 5 команд.
Более глубокие уровни — это моделирование взаимодействия железок в системе умного дома, чтобы исключить всякие неприятные ситуации для пользователя из-за каких-нибудь дедлоков и пр. в протоколах и логике.
Если да, то можно ли увидеть пример?
Для более-менее толкового примера нужно чуть погрузиться в специфику умного дома, что потребует времени. Саму модель для наиболее важных частей системы после этого сделать относительно несложно.
Насчёт модели умного дома можно продолжить в личке, если мне получится выкроить время чтобы погрузиться в специфику этой области на достаточном уровне, может ещё одну статью по этому поводу напишу с примером близком к реальности.
Создание математической модели для алгоритма это одно, у тебя есть входные параметры, их область применения, это все очень похоже на математику и ее теоремы. А вот с бизнес логикой, где много висящих хвостов, ad hoc параметров все выглядит иначе.
Принципиальной разницы нет. Опять же рекомендую в блоге Hillel Wayne посмотреть примеры из разных областей.
Моделирование подходит для любых областей, где есть система с пространством состояний и дискретные переходы между ними (в общем случае недетерминированные).
Поиск моделей подходит для задач, которые можно выразить в виде некоторых объектов и отношений между ними, ну и плюс логика.
Важно иметь некоторый опыт и навыки работы с тулами и опыт по абстракции и декомпозиции частей системы, чтобы потом на абстрактном уровне проанализировать их взаимодействие.
Это первая моя статья из цикла, призванного привлечь внимание разработчиков и менеджеров к инженерному подходу к разработке ПО. В последнее время он незаслуженно обойдён вниманием, несмотря на революционные изменения в подходе и инструментах поддержки.
Моя мотивация для погружения в тему — это то, что мне импонирует подобный подход к задачам. Пока что мне не удалось вызвать интерес к этому ни у одного из коллег (объяснял, кидал ссылки на статьи). Типичный ответ — напишем примерные требования максимум, тесты напишем, разве мало? Планирую погрузиться в данную тему (через приведенную вами литературу и сторонние ресурсы) и все проверить на личном опыте, только так думаю смогу получить сторонников)).
Тут я думаю можно провести аналогию с университетским курсом: у студента конечно есть исчерпывающая информация в Фихтенгольце, но все хотят тоненькую методичку с конкретными первыми шагами, он их посмотрит, решит задачки, а там может и Фихтенгольца откроет.
Например, что мне выбрать TLA+ или Alloy? А где будет храниться спецификация? Прямо в проекте или отдельно? Спецификацию пишут на функцию, класс или в отдельных случаях лишь на модуль (если функции и классы малы и понятны)? Было бы здорово, если бы вы помогли сделать первые шаги, как это делают современные курсы по обучению. Это вызовет интерес и далее человеку будет гораздо проще двигаться.
П.С. Разрабатываемый умный дом базируется на open source технологии z-wave и проприетарном контроллере. Сейчас находится на стадии когда команду придавил обрушивающийся сверху фунционал, который был создан в лучшем стиле ремесленной разработки. У меня есть данные по проекту, было бы интересно посмотреть, как можно было бы ускорить разработку, если применять инженерный подход.
Немного прокомментирую по пунктам:
Пока что мне не удалось вызвать интерес к этому ни у одного из коллег (объяснял, кидал ссылки на статьи). Типичный ответ — напишем примерные требования максимум, тесты напишем, разве мало?
Да, к сожалению разработчики и менеджеры не понимают, что грамотное применение формальных методов может серьёзно помочь с точки зрения уменьшения затрат на разработку, отладку и поддержку (уменьшением вероятности серьёзных архитектурных багов). Ну и вероятность сдать проект в срок тоже может быть увеличена.
Поэтому и задумал я написать цикл статей, где бы в простой форме можно было показать как применять тот или иной метод и инструмент.
Лично я понял полезность TLA+, когда занимался отладкой рандеву для многопоточного кода. Отлаживать нетривиальную синхронизацию в многопоточке — это сущий ад. На TLA+ нашёл ошибку в алгоритме (он хоть и базировался на Лэмпортовском, но был динамическим по количеству участников рандеву), ну и соответственно правил реализацию. Ошибка была на 63 шаге модели при поиске в ширину. То есть на тестах найти и отладить такое — нереально.
Например, что мне выбрать TLA+ или Alloy?
Тут имеет смысл посмотреть на промышленный опыт применения этих тулов. Например у амазона есть сравнение Alloy vs. TLA+ для их задач: https://lamport.azurewebsites.net/tla/formal-methods-amazon.pdf
А в целом примерно так: Alloy для моделирования структур, топологий и конфигураций и небольшой операционной семантики над ними (то есть, когда структура бедна форматами данных, функциями и пр., но богата связями/отношениями между объектами с большим количеством логики поверх этих отношений), а TLA+ когда много динамики с богатыми структурами данных (множества, записи, функции и пр).
Грубо говоря: статика (топология, конфигурации) — это Alloy, а динамика (протоколы, FSM и тд) — это TLA+. Хотя до какой-то степени они взаимозаменяемы. Например, я нормально моделировал FSM и в Alloy.
А где будет храниться спецификация? Прямо в проекте или отдельно?
Если рассматриваем спеку в формальном смысле (текст на TLA+/Alloy), то тут зависит от уровня абстракции: абстрактные спеки ближе к диз-докам и высокоуровневой докуменатации проекта, детальные спеки уже ближе к коду (либо даже в код в комментарии и настроить систему CI, чтобы она в одном из шагов вырезала спеки из исходников и прогоняла их проверку в тулах моделирования).
Ещё есть небольшой плюс: Alloy позволяет получать диаграммы конфигураций системы в виде картинок, что позволяет их потом использовать в доках, и для TLA+ тоже есть модуль анимации трасс: https://github.com/will62794/tlaplus_animation. Это позволяет при небольшой сноровке из моделей получать сопровождающие картинки для документации. Например, в текущей статье все диаграммы взяты из Alloy (с небольшими правками).
Спецификацию пишут на функцию, класс или в отдельных случаях лишь на модуль (если функции и классы малы и понятны)?
Тут всё зависит от потребности. Где-то достаточно высокоуровневых спек, на абстрактном архитектурном уровне, где-то нужны более детальные.
Хорошо процесс применения спек описан в OpenCom RTOS
В общем где, как и на каком уровне детализации применять спеки зависит от конкретного проекта и конкретных потребностей. Понимание этого приходит по мере изучения методов и примеров их применения в промышленности.
Часто можно спеки применять ретроспективно, например, чтобы промоделировать подозрительные части системы, в корректности которых есть сомнения (в распределённых системах на тестах далеко не всё можно найти).
Было бы здорово, если бы вы помогли сделать первые шаги, как это делают современные курсы по обучению. Это вызовет интерес и далее человеку будет гораздо проще двигаться.
Тут не совсем понял. На какие-либо курсы у меня точно не хватит ни сил, ни времени.
Пока постараюсь только цикл статей обзорных с небольшими примерами сделать.
Советую посмотреть блог Hillel Wayne (уже многократно тут на него ссылался), у него много простых примеров применения формальных спек и моделирования.
Относительно TLA+ могу рекомендовать его же книгу Practical TLA+. Относительно простое введение в использование TLA+ с простыми примерами. Для начала — самое оно.
У меня есть данные по проекту, было бы интересно посмотреть, как можно было бы ускорить разработку, если применять инженерный подход.
С этим, наверное, лучше в личку. Может, после обсуждения получится на интересную статью материал сделать (при согласовании того, какие детали допустимо выносить на публикацию).
Рад, что вам понравилась эта книга!
Это реально хорошая книга для первого знакомства с TLA+. Её смело можно рекомендовать всем разработчикам.
Думаю многим дальше PlusCal и не потребуется погружаться в ньюансы TLA+.
Но если вдруг нужно будет чуть больше low-level деталей могу рекомендовать виде-курс самого Лэмпорта: http://lamport.azurewebsites.net/video/videos.html
Затем его книгу "Specifying Systems": https://lamport.azurewebsites.net/tla/book-02-08-08.pdf
И ещё у Рона Преслера можно почитать цикл статей: https://pron.github.io/posts/tlaplus_part1
Вообще у Рона можно всё читать, он хорошо и доходчиво объясняет многие сложные вещи. Но это если есть сильный интерес к Computer Science.
Ещё у Hillel Wayne и Ron Pressler есть довольно много видео с выступлений на различных конференциях, можно на YouTube поискать.
В вашей статье, по приведённой ссылке, основной упор делается на верификацию программ и верифицированное ПО (тот же пример с seL4). Ну и плюс упоминаются языки с алгебраическими системами типов и спец-железо под эти языки и тд.
Это хорошо, что такие мысли возникают (надеюсь, у всё большего количества разработчиков), но тут нужно хорошо себе представлять область применения разных технологий, методов и инструментов. И что формальные методы включая формальную верификацию программ — это только одно из условий корректного ПО (необходимое, но не достаточное)
Например:
Невозможно создать очень выразительный язык, чтобы свойства программ на нём легко доказывались. Тут антагонизм — либо ограничиваем выразительность языка, чтобы класс верифицируемых программ был шире, либо жертвуем верифицированностью в угоду большей выразительности. Хорошая статья на эту тему (и смежные темы) у Ron Pressler: Why Writing Correct Software Is Hard
Очень рекомендую всего Рона Преслера, там все материалы отличные.
Задача формулирования свойств для проверки/верификации сама по себе довольно сложная и интересная. И тут, к сожалению, не так уж и много автоматизируется. Всё гипотезы для проверки, контракты, все LTL формулы и пр. должен формулировать разработчик (автоматически там не так много можно сформулировать и почти всё оно будет тривиальным), основываясь на требованиях к ПО.
И тут мы переходим к след. пункту:
Постановка задач и разработка требований — тоже сама по себе довольно сложная задача и мало-автоматизируемая.
Программы (на любых языках, хоть C, хоть Haskell) — это всего-лишь зафиксированные в тексте алгоритмы поведения системы (частей системы, при декомпозиции). И вопрос разработки корректных (для решения какой-либо прикладной задачи) алгоритмов — это тоже нетривиальная и слабоавтоматизируемая задача.
Много базовых алгоритмов (сортировки, поиска и пр) уже разработано, какая-то часть даже формально верифицирована на соответствующие свойства (то что алгоритм qsort действительно сортирует и пр.), но любой практический софт, базируясь на этих "кирпичиках" реализует свой нетривиальный алгоритм, корректность которого — это ещё вопрос.
И много-много других моментов, которые влияют на корректность ПО по отношению к решаемым этим ПО задачам.
Что самое интересное, что Рон Пресслер(в той статье по ссылке в комментарии) хорошо показывает, что языки на сложность задачи верификации свойств программ влияют слабо, ибо там сложность растёт от самих свойств. И декомпозиция программ не помогает в уменьшении сложности верификации, так как сумма верифицированных частей не равна автоматом верифицированному целому, это целое нужно отдельно верифицировать и сложность явно больше простой суммы сложностей верификации отдельных частей.
То есть задача верификации в общем случает от языков слабо зависит. Если язык тьюринг полный. Можно, конечно, урезать полноту языков, но тогда мы будем сильно сужать область решаемых задач в рамках этих языков.
Чисто интуитивно кажется, что доказывать корректность Rust кода должно быть проще чем сишного.
Чисто интуитивно кажется, что доказывать корректность Rust кода должно быть проще чем сишного.
Как показывает Ron Pressler, фундаментальной разницы в общем случае нет.
У него основная идея — это для определённых классов задач (только нужно сначала ввести продуманную таксономию) разработать DSL'и и спец-средства для проверки кода на этих DSL. За счёт специализации по областям применения и разумного ограничения на DSL'и, можно класс формально верифицированного ПО значительно увеличить.
Важный момент это возможность прогресса — допустим мы сделали формально верифицированную софтину, а потом, со временем нашли баг в требованиях, исправили их, исправили софтину и снова верифицировали их, в отличии от обычной разработки мы в значительно большей степени уверены, что улучшили наше решение т.к. знаем что правки не внесли багов.
сформулировать корректные требования значительно проще чем корректно реализовать их
В целом кажется так, но думаю иногда может быть и наоборот.
Но в целом задача формулирования требований весьма нетривиальная — нужно понять какие инварианты и предикаты в системе позволяют ей достигать нужных нам характеристик, а это весьма творческий процесс.
Важный момент это возможность прогресса — допустим мы сделали формально верифицированную софтину, а потом, со временем нашли баг в требованиях, исправили их, исправили софтину и снова верифицировали их, в отличии от обычной разработки мы в значительно большей степени уверены, что улучшили наше решение т.к. знаем что правки не внесли багов.
Именно такой подход мне импонирует больше всего, ибо позволяет сдержать экспоненциальный рост костылей в софте по мере изменения функционала и починке багов.
Но, я предполагаю, что делая свободные верифицированные компоненты вроде того же seL4 мы в какой-то момент можем оказаться в мире где есть верифицированная операционная система пригодная для всего (может кроме домашнего использования).
Ведь ровно также получилось со свободным софтом — шаг за шагом делались отдельные компоненты и однажда оказалось, что GNU/Linux это полноценная и универсальная операционная система.
Но, я предполагаю, что делая свободные верифицированные компоненты вроде того же seL4 мы в какой-то момент можем оказаться в мире где есть верифицированная операционная система пригодная для всего (может кроме домашнего использования).
Хотелось бы в это верить, но тот же самый seL4 накладывает весьма серьёзные ограничения на межмодульное взаимодействие.
Кроме того, в общем случае (общий знаменатель) мы можем рассчитывать на массовый верифицированный софт, который верифицирован только на базовые свойства (типа нет сегфолтов, и пр), а верификация продуктовой-логики всё-равно будет специализирована по конкретным областям применения софта.
Даже к одному и тому же софту в разных областях могут предъявляться существенно разные требования.
Что, на мой взгляд, серьёзно затрудняет появление массового верифицированного софта.
Во-первых — спасибо за статью, много нового узнал. А во-вторых — пока читал не отпускала мысль: это очень похоже на property based testing, даже у Hillel Wayne в блоге оно неоднократно упоминается. Так вот, вопрос: даст ли какие-то преимущества использование Alloy/TLA+ по сравнению с написанием хорошо изолированной бизнес-логики, покрытой property based тестами? Понятно, что скорее всего на Alloy прототип можно набросать быстрее, чем даже на каком-нибудь питоне, но потом все равно придется писать реализацию, проверять на соответствие прототипу (глазами?) и крыть теми же тестами с проверками инвариантов — и разве генерация тест кейсов не даст те же плюшки, что и Alloy? Или там есть еще какие-то неочевидные преимущества?
Во-первых — спасибо за статью, много нового узнал.
Пожалуйста! Рад, что статья оказалась полезной.
А во-вторых — пока читал не отпускала мысль: это очень похоже на property based testing, даже у Hillel Wayne в блоге оно неоднократно упоминается.
Да, во многом сходство есть. Но есть и фундаментальное различие: property testing — это те же самые тесты, пусть и направленные (засчёт шейпинга случайных данных по precondition предикатам), но всё-таки тесты. То есть они пространство состояний покрывают не сплошным покрытием, а выборочным.
Alloy же, при поиске моделей, просматривает все состояния вплоть до заданного предела.
TLС тоже просматривает (в основном режиме работы) все состояния порождаемые TLA+ формулой.
Ну и собственно, это в основном и отличает их от тестов.
Например, те пространства, которые доступны Alloy, недоступны тестам.
Так вот, вопрос: даст ли какие-то преимущества использование Alloy/TLA+ по сравнению с написанием хорошо изолированной бизнес-логики, покрытой property based тестами?
Тут в одном вопросе на самом деле несколько тем затронуто:
- Выразительность: Alloy и TLA+ напрямую с тестами тяжело сравнивать, так как выразительные свойства Alloy и TLA+ намного лучше, так как там мы пишем декларативно и на высоком уровне абстракции.
Например, в тестах мне явно нужно писать функцию сортировки или функцию проверки того, что массив отсортирован, в Alloy (и в TLA+ тоже, только синтаксис немного другой) я пишу предикат, где описываю нужное мне свойство: pred sorted [s: seq Obj] { all disj x,y: s.elems | x < y => s.idxOf[x] < s.idxOf[y]}
Зачастую выразить свойства объектов намного проще декларативно в логике, чем описывать в каком-либо языке программирования процедуру вычисления этого свойства.
То есть, абстрактные описания на Alloy и TLA+ получаются существенно короче, чем если то же самое описывать, например, на питоне.
- TLA+ и Alloy предназначены для разных вещей, которые тестами тяжело либо невозможно сделать.
Например, на базе тестов нельзя нормально искать контр-примеры к конфигурации какой-либо системы. Alloy же позволяет не только это, а ещё, например, поиск конфигураций с учётом классов эквивалентности (редукция симметрии), как такого эффекта достичь с помощью тестов — сразу не могу придумать.
TLA+ позволяет довольно просто описать несколько взаимодействующих процессов системы и промоделировать их на наличие гонок, дедлоков и пр. Частично этого можно достичь тестами, но TLC просматривает все возможные состояния, причём делает это весьма эффективно и может запускаться на кластере машин. Тестами такое сложно сделать, ну и покрытия такого сложно достичь.
Кроме того, TLA+/TLC позволяет проверить систему не только на safety свойства, но ещё и на liveness, то есть то что система у нас не только не делает плохих вещей, но и то что она обязательно делает что-то хорошее и полезное. Проверка liveness свойств с помощью тестов — тоже что-то такое, на что у меня воображения не хватает, так как там нужно проверять темпоральные формулы по трассам переходов системы в пространстве состояний.
То есть, с помощью model-finders/model-checkers решается существенно другой класс задач, чем тестами (даже направленными, фаззингом и др.). Что совсем не исключает тестов, а напротив, эти инструменты серьёзно усиливают тесты.
Понятно, что скорее всего на Alloy прототип можно набросать быстрее, чем даже на каком-нибудь питоне, но потом все равно придется писать реализацию, проверять на соответствие прототипу (глазами?) и крыть теми же тестами с проверками инвариантов — и разве генерация тест кейсов не даст те же плюшки, что и Alloy?
В статье есть хороший пример того, что сделать тестами весьма сложно — проверка свойств операций. Инварианты для нужных мне свойств операций я разрабатывал с помощью модели и поиска контр-примеров. Как примерно то же самое делать с тестами, да ещё и более менее эффективно — я не знаю.
Реализацию конечно придётся писать, и тесты на реализацию тоже. Но на модели можно обкатать все нужные свойства, предикаты и инварианты и уже на их базе разрабатывать направленные тесты.
Ну и ещё есть класс вещей, которые тестам практически не доступны: это распределённые системы, параллельное и асинхронные системы, в общем любой класс систем с существенным недетерминизмом в логике управления (когда много потоков управления с асинхронным недетерминированными событиями и реакциями на них).
Зато такой класс систем вполне успешно можно разрабатывать с применением model-checkers/model-finders, закрывая ими сложные недетерминированные места в логике, а последовательную логику можно и тестами закрыть.
Или там есть еще какие-то неочевидные преимущества?
Почему неочевидные?
Преимущества как раз хорошо очевидны:
На спеках с помощью Alloy/TLA+ и др мы отлаживаем архитектуру и самые базовые абстрактные вещи, отлаживаем синхронизационный скелет системы и основные сложные моменты. Это даёт нам шанс избежать дорогостоящих архитектурных, синхронизационных и др. ошибок, которые тестами тяжело, либо практически невозможно (ошибки в распределённых и параллельных системах) потом поймать стабильно на тестах и отладить.
На основе спек мы получаем множество предикатов, инвариантов и прочего, которые закладываем в код и тесты. Тесты в этом случае можно сделать намного более направленными и специфичными.
Намного проще становится делать серьёзный рефакторинг, который затрагивает архитектуру и базис системы. Мы всегда новый функционал можем проверить на спеках на совместимость с уже существующим. Что позволяет опять же избегать дорогостоящих ошибок.
Alloy же, при поиске моделей, просматривает все состояния вплоть до заданного предела. TLС тоже просматривает (в основном режиме работы) все состояния порождаемые TLA+ формулой.
Теоретически никто не запрещает в property-based тестах генерировать не случайные состояния, а вообще все (в пределах заданных ограничений), но из-за комбинаторного взрыва это может быть очень медленно. Если TLC тупо брутфорсит все пространство состояний — это ведь ничем не лучше, или там все-таки есть какие-то оптимизации? Alloy — да, за счет использования SAT-солвера может проверить пространство состояний гораздо быстрее, но как вы сами показали в статье далеко не все модели можно им проверить в принципе.
Выразительность: Alloy и TLA+ напрямую с тестами тяжело сравнивать, так как выразительные свойства Alloy и TLA+ намного лучше, так как там мы пишем декларативно и на высоком уровне абстракции. Например, в тестах мне явно нужно писать функцию сортировки или функцию проверки того, что массив отсортирован, в Alloy (и в TLA+ тоже, только синтаксис немного другой) я пишу предикат, где описываю нужное мне свойство: pred sorted [s: seq Obj] { all disj x,y: s.elems | x < y => s.idxOf[x] < s.idxOf[y]}
Питон тоже умеет очень даже декларативно и коротко:
def is_sorted(s: List) -> bool:
return all(a <= b for a, b in zip(s, s[1:]))Например, на базе тестов нельзя нормально искать контр-примеры к конфигурации какой-либо системы.
Ну почему же? Вот пример такого теста для протокола binary agreement: https://github.com/poanetwork/hbbft/blob/master/tests/binary_agreement.rs#L64 Насчет учета классов эквивалентности — к сожалению, не уверен, что правильно понимаю о чем речь, можете показать пример и/или кинуть ссылкой почитать именно в этом контексте?
TLA+ позволяет довольно просто описать несколько взаимодействующих процессов системы
При наличии небольшого фреймворка такое можно провернуть и в "обычных" языках программирования. Вот пример теста, который проверяет кучу инвариантов для протокола смены лидера (в частности, упрощенно, что если он начался, то в итоге закончится и все запросы выполненные хотя бы на одной ноде окажутся в очереди на выполнение всеми нодами): https://github.com/hyperledger/indy-plenum/blob/master/plenum/test/consensus/test_sim_view_change.py#L9 Причем проверяет это непосредственно для продакшн-кода на большом количестве конфигураций, а за счет инъекции всех внешних зависимостей (в частности времени, шедулера и сетевого стека) тест работает повторяемо и достаточно быстро. Багов в начальной имплементации кстати этот тест наловил прилично.
К сожалению, пока я вижу только следующие плюсы (с оговорками):
- Alloy, и возможно TLC, могут эффективнее перебирать пространства состояний (но при этом Alloy довольно ограничен в том, какие свойства в принципе поддаются проверке)
- Alloy и TLA+ заточены под быстрое прототипирование высокоуровневых моделей (но при этом те же генераторы состояний и тесты инвариантов придется дублировать и для продакшн кода)
В общем, я все это не к тому, что "TLA не нужен" — мне этот подход очень даже понравился, в каком-то смысле есть ощущение, что это как бы следующая ступенька над обычными спецификациями и генеративными тестами по их мотивам, но просто ощущения скорее всего будет недостаточно, чтобы "продать" эту идею менеджменту, при том, что мы уже используем property-based тестирование.
Теоретически никто не запрещает в property-based тестах генерировать не случайные состояния, а вообще все (в пределах заданных ограничений), но из-за комбинаторного взрыва это может быть очень медленно. Если TLC тупо брутфорсит все пространство состояний — это ведь ничем не лучше, или там все-таки есть какие-то оптимизации?
В принципе, можно и тестами перебирать все состояния.
Но задавшись вопросами оптимизации этого процесса, сначала (в случае explicit state model checker'а) вы придёте к идее абстракции, чтобы уменьшить комбинаторный взрыв, потом к идее о том, что нужно состояния перебирать эффективно, учитывая симметрию (это, например, когда у нас есть две модельных переменных x и y, принимающие значения из одного множества S, и в логике учитывается только случай x == y и x != y, тогда мы эффективно можем считать что S состоит всего из двух элементов, так как остальные варианты значения пар {x, y} приведут нас либо к трассам изоморфным всего двум трассам для x==y и x!=y), потом вы захотите проверять не только safety свойства, но и liveness и тд.
И таким образом, постепенно придёте к идеям и реализациям, которые лежат в основе TLC (и похожих инструментов).
Ну и если зададитесь более удобным (и надёжным с точки зрения математики) формализмом, то придёте к идее чего-то подобного TLA+.
Кроме того, для TLA+ есть ещё TLAPS, который позволяет формально доказывать! свойства TLA+ формул. Со всей математической строгостью.
То есть, то что невозможно нормально проверить (не всё, конечно, но довольно многое) с помощью TLC (получается комбинаторный взрыв), можно доказать с помощью TLAPS.
То есть вы можете перейти от model-checking к формальному доказательству в тех случаях, где TLC не хватило оставаясь в рамках одного формализма и даже одного набора инструментов (TLA toolbox IDE + TLC + TLAPS).
Кроме того, TLC из коробки сразу предлагает возможность запуска на кластере машин и тд.
В общем, тут вопрос в удобстве и уровнях абстракции. А TLAPS вообще никак не сымитировать тестами, даже самыми навороченными property-based.
Кроме того, property-based тестирование, на мой взгляд не предлагает удобного уровня абстракции, оно весьма низкоуровневое и там нужно прилагать усилия, чтобы использовать его на высоких уровнях абстракции. И тут же встаёт проблема надёжного перехода к более низким уровням, то что в TLA+ решается за счёт обычной импликации TLA+ формул (которую можно закрыть TLAPS абсолютно надёжно), в property-based тестировании опять же надёжно не сделать.
Ну или, например, взять B-method (AtelierB), там можно надёжно спуститься от самых высоких уровней абстракции вплоть до кодогенерации надёжно и доказуемо закрыв процесс уточнения моделей. На основе property-based тестов такого не достичь.
Тут всё зависит от того, что вам нужно, какие сроки, бюджеты, срок жизни проекта и тд.
Серьёзно закрывать всё формальными методами — это весьма дорого, хотя иногда может дать серьёзный выигрыш (см. OpenCOM RTOS) по объёмам разработки и отладки.
Alloy — да, за счет использования SAT-солвера может проверить пространство состояний гораздо быстрее, но как вы сами показали в статье далеко не все модели можно им проверить в принципе.
Alloy — это уникальный инструмент, который, когда понимаешь как он работает и как его использовать, становится очень полезным для быстрого прототипирования архитектур и их свойств. Сделать набросок конфигураций какой-либо системы и посмотреть, как она может меняться под воздействием каких-либо операций, какие варианты развития возможны — это очень быстро и просто при определённом навыке.
Да, у него есть ограничения, и на сколемизацию, и на рекурсию в формулах и на порядок отношений. Но эти все ограничения позволяют ему быть крайне эффективным в своём классе задач (всё что можно выразить в реляционной логике первого порядка с операторами замыкания и join, а это очень широкий класс задач).
И в реальности, по моему опыту (весьма небольшому, нужно признать) в ограничения Alloy я почти никогда не упирался. А если и упирался где-то, то зачастую весьма просто их обходил, переписав отношения или ослабив некоторые условия в системе.
Кроме того, сейчас идёт усиленные подвижки в сообществе Alloy в сторону SMT солверов, что ещё больше расширит класс задач, где можно использовать Alloy. Есть определённое развитие в сторону Higher-Order Alloy, там тоже интересные результаты.
Питон тоже умеет очень даже декларативно и коротко:
Да, часть предикатов он может коротко. Но если потребуется выражать чуть более сложные свойства, содержащие транзитивные замыкания, например, то тут уже становится далеко не так красиво и совсем неэффективно.
Ну почему же? Вот пример такого теста для протокола binary agreement: https://github.com/poanetwork/hbbft/blob/master/tests/binary_agreement.rs#L64
Я не совсем точно выразился, контр-примеры искать конечно можно для safety свойств, но крайне неэффективно в общем случае, а про liveness свойства можно забыть, так как никакие тесты не позволят нормально проверить все трассы которые удовлетворяют или не удовлетворяют определённым LTL формулам. Ну либо вы уже среду тестирования превратите в model-checker :) И это уже будет model-checker с опцией тестирования :) Прямо как TLC (у него есть режим тестирования на рандомных цепочках трасс состояний) :)
Вот пример теста, который проверяет кучу инвариантов для протокола смены лидера (в частности, упрощенно, что если он начался, то в итоге закончится и все запросы выполненные хотя бы на одной ноде окажутся в очереди на выполнение всеми нодами): https://github.com/hyperledger/indy-plenum/blob/master/plenum/test/consensus/test_sim_view_change.py#L9 Причем проверяет это непосредственно для продакшн-кода на большом количестве конфигураций, а за счет инъекции всех внешних зависимостей (в частности времени, шедулера и сетевого стека) тест работает повторяемо и достаточно быстро. Багов в начальной имплементации кстати этот тест наловил прилично.
Ну это уже явное движение в сторону explicit state model checkers, как я уже и писал, можно в эту сторону дойти до функционального аналога TLC, но с особенностями в виде потери возможности уточнения моделей и возможности верификации (TLAPS), так как для этих возможностей нужен уже соотв. формализм (с определённым математическими свойствами, этот формализм, в принципе можно получить из целевого языка (питона, например), если его ограничить до определённой степени, но боюсь, там от питона только часть синтаксиса останется, семантика уже будет совершенно другая)
Только вы не подумайте, что я агитирую за Alloy/TLA+ в противовес тестированию и в частности property-based тестированию. Совсем нет. Наоборот model-checkers и model-finders могут дать огромный буст тестированию при правильном применении. И уж тем более они не заменяют тестирование.
Alloy, и возможно TLC, могут эффективнее перебирать пространства состояний (но при этом Alloy довольно ограничен в том, какие свойства в принципе поддаются проверке)
Не только эффективнее, но и могут делать то, что тестами сделать невозможно (TLAPS, как уже писал выше). Или оператор транзитивного замыкания отношений в Alloy (SAT солверы его вычисляют мгновенно, а у тестов будет комбинаторный взрыв и время улетит в бесконечность)
Кроме того, что Alloy, что TLA+ — это формализмы со специально разработанными свойствами, что тоже даёт определённые бонусы.
Alloy и TLA+ заточены под быстрое прототипирование высокоуровневых моделей (но при этом те же генераторы состояний и тесты инвариантов придется дублировать и для продакшн кода)
Да, в основном высокоуровневые спеки и прототипы особенно критичных частей системы и общей архитектуры компонент.
И да, в тесты придётся переносить часть инвариантов и предикатов и тесты будут всё-равно нужны.
Но, прототипирование и проверка свойств прототипов на Alloy и TLA+ просто несопоставимо быстрее, чем если это делать, например на питоне (даже без учёта написания тестов, просто описать модель в коде питона будет на порядок — два медленнее).
Возможно, если поискать различные DSL и фреймворки, задача прототипирования и станет чуть проще, но, думаю, к Alloy/TLA+ всё равно будет тяжело приблизиться.
И ещё такой момент, когда возникает "пощупать" какую-либо архитектурную идею, то на формальных спеках это можно сделать очень быстро и эффективно (ну и соответственно быстро найти фундаментальные проблемы), чем пытаться проверить её на уже готовом пуле кода и тестов.
В общем, я все это не к тому, что "TLA не нужен" — мне этот подход очень даже понравился, в каком-то смысле есть ощущение, что это как бы следующая ступенька над обычными спецификациями и генеративными тестами по их мотивам, но просто ощущения скорее всего будет недостаточно, чтобы "продать" эту идею менеджменту, при том, что мы уже используем property-based тестирование.
Круто, что используете property-based тестирование! Реально весьма мало кто использует хотя-бы нормальное тестирование с хорошим покрытием.
О! Оккам. Считаю, что он слишком сильно опередил своё время и поэтому не смог получить (вместе с транспьютерами) заслуженной оценки и распространения. Хотя идеологичеки (и даже синтаксически :) ) сильно повлиял на многие языки.
Что касается спецификации/верификации, то разбиение системы на небольшие модули (как программные так и аппаратные) с точки зрения свойств системы в целом, в общем случае задачу не облегчает.
Так как сложность верификации системы в целом определяется в первую очередь сложностью свойств, которые могут (и часто будут) и не декомпозироваться по модулям.
Хорошо это расписано у Рона Преслера: https://pron.github.io/posts/correctness-and-complexity
Если удастся это "скрещивание" надёжно убрать за абстракции DSL, и эти абстракции будут обладать хорошими с точки зрения верификации свойствами, то можно задачу верификации и упростить.
Рон Преслер и про DLS'и тоже писал :) Как один из способов расширения класса программ, которые можно верифицировать.
Есть другой подход — correct by construction. Сделать формализм, в рамках которого создать с нужными свойствами программу, а затем синтезировать нужные программные и аппаратные блоки из этого формализма. Пример такого подхода — b-method (AtelierB), например.
Есть другой подход — correct by construction. Сделать формализм, в рамках которого создать с нужными свойствами программу, а затем синтезировать нужные программные и аппаратные блоки из этого формализма. Пример такого подхода — b-method (AtelierB), например.
звучит круто, но непонятно )
звучит круто, но непонятно )
Я же прямо пример привел: AtelierB
Это инструмент, помогающий работать в рамках формализма b-method, который позволяет итеративно и последовательно разрабатывать ПО от абстрактной модели к конкретному коду.
То есть, не сначала пишем код, потом спеки на свойства и пытаемся доказать соответствие одного другому, а сначала высокоуровневая модель, которая потом итеративно и через верификацию уточняется вплоть до кода (на C, Ada и тд).
Такой подход называется correct by construction. Есть довольно много вариантов такого подхода, и у всех них отличительная черта то, что весь процесс разработки закрыт формальной верификацией, от начальных спек до готового кода.
Инженерный подход к разработке ПО