company_banner

Инженерный подход к разработке ПО

    Как проверить идеи, архитектуру и алгоритмы без написания кода? Как сформулировать и проверить их свойства? Что такое model-checkers и model-finders? Требования и спецификации — пережиток прошлого?


    Привет. Меня зовут Васил Дядов, сейчас я работаю программистом в Яндексе, до этого работал в Intel, ещё раньше разрабатывал RTL-код (register transfer level) на Verilog/VHDL для ASIC/FPGA. Давно увлекаюсь темой надёжности софта и аппаратуры, математикой, инструментами и методами, применяемыми для разработки ПО и логики с гарантированными, заранее определёнными свойствами.


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


    Не буду лукавить: основная задача статьи — возбудить интерес. Так что в ней будет минимум пространных рассуждений и максимум конкретики.



    В статье две части. В первой я опишу, что подразумеваю под инженерным подходом, во второй покажу пример использования подхода в рамках простой задачи (близкой к области микросервисной архитертуры).


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


    Часть 1. Инженерный подход к разработке


    Что это такое? Покажу на примере возведения моста:


    • Этап 1 — это сбор требований к мосту: тип моста, грузоподъёмность и т. д.
    • Этап 2 — уточнение требований и расчёт конструкций (спецификация).
    • Этап 3 — собственно само строительство на основе инженерных расчётов (спецификаций).

    Конечно, это упрощённая аналогия. Никто не делает прототипов мостов, чтобы уточнить требования и спеки. В мост нельзя добавить параметризации, чтобы он становился то арочным, то подвесным. Но в целом, думаю, аналогия ясна.


    В разработке ПО этапы 1 и 2 часто отсутствуют либо очень слабо выражены. Если требования и зафиксированы, то расплывчато, неполно и неформально. Лишь единицы детализируют требования и разрабатывают чёткие спецификации.


    Многие считают, что это трата времени, пережиток прошлого, особенно если выбран agile-подход к разработке (особенно с короткими итерациями). И это большое заблуждение.


    Почему?


    Для начала разберёмся, что такое требование и спецификация и в чём их существенное отличие, которое даже многим профессионалам не всегда очевидно.


    Что такое требования?


    Если кратко, требования — это формулирование свойств продукта в терминах предметной области. Например, так: «Все экземпляры программы должны одинаково обрабатывать входные запросы».


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


    Важно понимать это и чётко отделять одно от другого.


    Почему?


    1. Требования должны быть понятны потребителям ПО, поэтому должны быть из предметной области, для которой разрабатывается ПО (часто к формулировке требований и постановке задачи на разработку ПО приходится привлекать экспертов, далеких от разработки).


    2. Свойства ПО, которые видит потребитель, оцениваются по метрикам предметной области. Нужно разделять требования и спецификации, чтобы иметь возможность 1) выделить основные метрики продукта, по которым потребитель будет оценивать наше ПО, и 2) ясно понимать, какие свойства продукта важны для пользователя, а какие нет.



    А иначе может получиться так: разработчики, не укладываясь в срок, пожертвуют важными свойствами и уделят много времени и внимания неважным. Причём то, что кажется важным с точки зрения разработки ПО, может быть неважным с точки зрения для пользователя.


    Классический пример такого несоответствия приведён в разнообразной литературе о разработке пользовательского интерфейса и в статьях (например: System Response Time and User Satisfaction: An Experimental Study of Browser-based Applications, Computer latency: 1977–2017). Разработчики обычно стараются оптимизировать время выполнения операции, например поиска информации в базе данных, а для пользователя важно время отклика системы. И если поиск идёт медленно, но пользователь начинает видеть выдаваемые результаты как можно быстрее, то ему кажется, что такое ПО работает лучше, чем то, которое ищет быстро, но сначала аккумулирует результаты и в конце выдаёт их все.


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


    И, наконец, самая важная причина:


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


    Об этом хорошо написал Michael Jackson в книге Problem Frames: Analysing & Structuring Software Development Problems. На мой взгляд, это одна из самых полезных книг для разработчиков ПО. Она учит в первую очередь анализировать проблемы пользователей, которые и должно решать хорошее ПО. Супербыстрая программа, которая потребляет мало ресурсов системы, но не решает задач пользователей, — это плохая программа. Крутая, но плохая.


    Что есть спецификация?


    Спецификация — это формулирование свойств ПО в терминах области разработки ПО. Вот тут появляются понятия сложности, синхронизации и т. д.


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


    Особенно стоить отметить пользу и важность спецификаций на протоколы и интерфейсы между компонентами системы, что позволит избежать вот таких ситуаций:


    В чём отличие от обычного подхода к разработке?


    При инженерном подходе мы заранее проектируем ПО с требуемыми характеристиками в соответствии со спецификациями. Спецификации проверяем на нужные свойства, которые идут из требований.


    Я сделал сравнение в виде таблички (весьма субъективной):


    Свойство Инженерный подход Ремесленный подход
    Формулирование требований Детальное, часто используется формат ReqIF и сопутсвующие инструменты (Eclipse RMF, например) Детализация обычно мала, формулировки неточные, неформальные
    Спецификации Часто формальные, используются B-method, Z, VDM, TLA+, Alloy и т. д Вы что? Какие спеки? Мы в файлике написали, что нам нужно сделать и как оно должно работать, и хватит
    Отладка и моделирование спецификаций Pro-B, Atelier B, TLA+/TLC, Alloy, PRISM, VECS и т. д. Ой, а что, так можно было?
    Выделение метрик Детальное, на основе спецификаций и моделей Ну, какие-то метрики придумаем, напишем на вики-страничке
    Разработка кода На основе спецификаций и моделей Ну, тут как обычно: хлоп-хлоп — и в продакшн
    Тестирование Направленные тесты на основе моделей на краевые случаи, выявленные на моделях; направленные рандомизированные генерируемые по моделям. Интеграционные на краевые случаи по спецификациям интерфейсов и протоколов взаимодействия.
    Контролирующие автоматы на основе LTL-свойств моделей; направленный фаззинг; Bounded model checking (Divine, например)
    Ну, как обычно: немножко юнит-тестов, потом подумаем над типовыми случаями и добавим интеграционных и системных; фаззинг для некоторых критичных функций (слабо фаззингом найти ошибку синхронизации в многопоточном ПО?); немного погоняем тесты под санитайзерами
    Верификация Например, возьмём GNATprove или Frama-C, возьмём свойства из спецификаций, аннотируем код и докажем формально соответствие кода формальным спецификациям; или будем использовать Atelier B, чтобы итеративно от спецификации перейти к реализации через кодогенерацию на финальном этапе; или выберем другой способ Не-е, это страшно, долго и дорого, да мы и не сформулировали свойства для формальной верификации: на соответствие чему проверять-то?

    А не за водопадную ли модель разработки тут идёт агитация?


    Инженерия ПО, включая даже формальные спеки и моделирования, отлично сочетается с agile-подходом.


    Есть мнение, что инженерный подход к разработке несовместим с быстрой итерационной разработкой ПО (так утверждается во многих статьях, вот пример).


    Но это не так. Инженерный подход с успехом применяется во многих проектах, в том числе в проектах с короткими итерациями.


    Раньше из-за слабо развитых средств и инструментов поддержки инженерный подход действительно был тесно связан с водопадной моделью.


    Но сейчас всё кардинально поменялось.


    Благодаря прорывным успехам в области моделирования, SAT/SMT-солверов и др. теперь можно быстро проверять огромные пространства состояний системы на наличие нужных нам свойств и отсутствие ненужных, верифицировать промышленные объёмы кода и т. д.


    Появились первоклассные промышленные инструменты типа Alloy, TLA+/TLC, Atelier B, PRISM, которые перевели задачу формализации и проверки спецификаций из академической/математической, требующей высокой квалификации и огромных усилий, в задачу push-button, доступную большинству программистов.


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


    Требования легко уточнять итеративно, особенно с современными подходами и инструментами.
    И уточнение требований, спецификаций, рефакторинг моделей, написание кода и его рефакторинг легко могут идти параллельно — в рамках одной итерации.


    В общем, инженерный подход сейчас совсем не равен водопадной модели, это уже две независимые вещи.


    Инженерный подход легко сочетается с любой методологией организации разработки.


    В блоге Hillel Wayne показано, как просто работать с формальными спецификациями и моделями. У него есть отличный пример, как за 10 минут формально специфицировать логику пользовательского интерфейса программы и проверить некоторые её свойства.


    Не буду вдаваться в детали и переводить статью целиком, просто покажу саму спецификацию на языке Alloy:


    Спецификация UI
    open util/ordering[Time]
    sig Time {
        state: one State
    }
    abstract sig State {}
    abstract sig Login extends State {}
    abstract sig Reports extends Login {}
    
    one sig Logout extends State {}
    one sig Students, Summary, Standards extends Reports {}
    one sig Answers extends Login {}
    
    pred transition[t: Time, start: State, end: State] {
      t.state in start
      t.next.state in end
    }
    
    pred logout[t: Time] { transition[t, Login, Logout] }
    pred login[t: Time] { transition[t, Logout, Summary] }
    pred students[t: Time] { transition[t, Reports, Students] }
    pred summary[t: Time] { transition[t, Reports, Summary] }
    pred standards[t: Time] { transition[t, Reports, Standards] }
    pred answers[t: Time] { transition[t, Students, Answers] }
    pred close_answers[t: Time] { transition[t, Answers, Students] }
    
    fact Trace {
      first.state = Summary
      all t: Time - last |
        logout[t] or
        login[t] or
        students[t] or
        summary[t] or
        standards[t] or
        answers[t] or
        close_answers[t]
    }

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


    Свойства для проверки тоже легко задаются:


    check {all t: Time | t.state = Answers implies 
            t.prev.state = Students} for 7

    Спецификация похожа на небольшую программу.


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


    С такими спецификациями можно легко работать в стиле agile.


    Зачем нужны такие спецификации и что с ними делать — покажу далее.


    Формализация спецификаций


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


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


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


    Чтобы не утомлять читателя лишними словами, перейдём к простому примеру.


    Часть 2. Пример использования Alloy


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


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


    Представленный подход к обработке данных на основе вычислительных графов применим для широкого класса задач.


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


    Отношения


    Традиционно в математике бинарным отношением называется множество пар $\big\{x,y\big\}$, где $x \in X$ и $y \in Y$.


    В Alloy принята такая запись: X->Y.


    Описание отношений и их свойств поместим в отдельный модуль (который очень близок к стандартному util/relation):


    Модуль relation.als
    module relation
    
    -- Мультипликаторы:
    -- set A - множество элементов из A, может быть пустым
    -- one A - множество ровно из одного элемента из A
    -- lone A - один элемент из A или пустое множество
    -- some A - один и больше элементов из A
    
    -- Универсумы:
    -- univ - множество всех элементов во всех множествах модели,
    --        можно считать объединением всех сигнатур
    -- iden - множество пар {A0, A0}, где первый и второй элемент
    --        пары один и тот же и из univ
    --        iden = {a : univ, b: univ |  a=b}
    --        то есть это отношение идентичности
    -- none - пустое множество
    
    -- Операции:
    -- логические: and, or, => (импликация), != (не равно), not
    -- над множествами:
    -- & - пересечение
    -- A->B - множество кортежей с элементами из соотв.
    --        множеств
    -- X<:Y - выбор из кортежей в Y тех, которые начинаются с
    --         кортежей из X
    -- A in B - множество A содержится в B
    -- ~A - перевернуть все кортежи в A
    -- A + B - объединение
    -- no A - A пустое, эквивалент A = none
    -- ^A - транзитивное замыкание бинарного отношения A,
    --      минимальное бинарное отношение B такое, что:
    --      A in B,
    --      {E0, E1}, {E1, E2} in B => {E0, E2} in B
    -- A.B - оператор JOIN, работает след. образом:
    --       {A0, B0} in A, {B0, C0, D0} in B, тогда
    --       {A0, C0, D0} in A.B 
    
    -- Кванторы:
    -- all X : Y | .... - всеобщности
    -- some X : Y | .... - существования
    
    -- применение предикатов:
    -- pred[a: A, b:B] {...} есть две синтаксические формы
    -- применения: pred[a, b] и a.pred[b]
    -- вторая форма сделана для мимикрии под некоторые
    -- ООП-языки, где методы определяются как
    -- method(self : Object, args ...)
    
    pred valid [rel : univ->univ, dom : set univ, cod : set univ] {
      rel.univ in dom and rel.univ in cod
    }
    fun domain [rel : univ->univ] : set (rel.univ) { rel.univ }
    fun codomain [rel : univ->univ] : set (univ.rel) { univ.rel }
    pred total  [rel: univ->univ, dom: set univ] {
      all x: dom | some x.rel
    }
    pred partial [rel: univ->univ, dom: set univ] {
      all x: dom | lone x.rel
    }
    pred functional [rel: univ->univ, dom: set univ] {
      all x: dom | one x.rel
    }
    pred surjective [rel: univ->univ, cod: set univ] {
      all x: cod | some rel.x
    }
    pred injective [rel: univ->univ, cod: set univ] {
      all x: cod | lone rel.x
    }
    pred bijective [rel: univ->univ, cod: set univ] {
      all x: cod | one rel.x
    }
    pred bijection [rel: univ->univ, dom, cod: set univ] {
      rel.functional[dom] and rel.bijective[cod]
    }
    pred reflexive [rel: univ->univ, s: set univ] {
      s<:iden in rel
    }
    pred irreflexive [rel: univ->univ] {no iden & rel}
    pred symmetric [rel: univ->univ] {~rel in rel}
    pred antisymmetric [rel: univ->univ] {~rel & rel in iden}
    pred transitive [rel: univ->univ] {rel.rel in rel}
    pred acyclic [rel: univ->univ, s: set univ] {
      all x: s | x not in x.^rel
    }
    pred complete[rel: univ->univ, s: univ] {
      all x,y:s | (x!=y => x->y in (rel + ~rel))
    }
    pred preorder [rel: univ->univ, s: set univ] {
      rel.reflexive[s] and rel.transitive
    }
    pred equality [rel: univ->univ, s: set univ] {
      rel.preorder[s] and rel.symmetric
    }
    pred partial_order [rel: univ->univ, s: set univ] {
      rel.preorder[s] and rel.antisymmetric
    }
    pred total_order [rel: univ->univ, s: set univ] {
      rel.partial_order[s] and rel.complete[s]
    }

    Многое из этого модуля нам не понадобится, оно приведено в качестве примера того, как можно даже сложные свойства отношений легко и лаконично выражать Alloy.


    Графы


    Теперь на основе отношений определим основные свойства графов.


    Модуль для описания графов близок к стандартному utils/graph, но, в отличие от модуля отношений, в данный модуль вошли только необходимые нам предикаты и функции:


    Модуль graph.als
    module graph[node]
    open relation
    
    -- функция получения всех узлов графа
    fun nodes[r: node->node]: set node {
      r.domain+ r.codomain
    }
    
    -- граф связан, то есть из любой вершины
    -- можно добраться до любой другой по рёбрам
    -- без учёта направленности
    pred connected[r: node->node] {
      all n1,n2 : r.nodes | n1 in n2.*(r + ~r)
    }
    
    -- граф ацикличный и направленный
    pred dag [r: node->node] {
      r.acyclic[r.nodes]
    }
    
    -- получить все корневые вершины
    -- корневая вершина та, в которую нет
    -- никаких входящих путей
    fun roots [r: node->node] : set node {
      let ns = r.nodes | -- ns - все узлы графа
        ns - ns.^r -- из всех узлов убираем те,
                   -- в которые есть какой-либо
                   -- входящий путь
    }
    
    -- получить все листья
    -- лист - конечный узел, из которого
    -- нет исходящих путей
    fun leaves [r: node->node] : set node {
      let ns = r.nodes | -- ns - все узлы графа
        ns - ns.^~r -- из всех узлов убираем те,
                    -- из которых есть какой-либо
                    -- исходящий путь
    }

    Вычислительный граф


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


    Основные характеристики:


    • (1) есть исток — узел, куда передаются входные данные, над которыми и выполняются вычисления;
    • (2) есть сток — узел, куда поступает результат вычислений, который отправляется дальше вовне;
    • (3) есть вычислительные узлы — они принимают данные, вычисляют и передают данные дальше;
    • (4) сток один, исток — тоже;
    • (5) у вычислительного узла может быть множество входящих и исходящих дуг. Типы данных и синхронизацию пока не рассматриваем. Для простоты считаем, что данные, пришедшие по входящей дуге, обрабатываются и передаются на все исходящие дуги;
    • (6) граф направленный, между любой парой узлов — максимум одна дуга, двух дуг в противоположных направлениях быть не может.

    На данном этапе мы рассматриваем в основном топологию.


    Теперь опишем вычислительный граф, который удовлетворяет вышеприведённым свойствам, на Alloy:


    Модуль compgraph.als
    module compgraph[node]
    
    open graph[node]
    open relation
    
    pred valid [edges: node->node,
                source : one node, -- свойство 1
                drain : one node -- свойство 2
    ] {
      edges.antisymmetric and edges.irreflexive -- свойство 6
      graph/roots[edges] = source -- свойство 1 и 4
      graph/leaves[edges] = drain -- свойство 2 и 4
    }

    Посмотрим на пару примеров вычислительных графов:


    open compgraph[node] as cg -- cg - это псевдоним
    
    enum node {n0, n1, n2, n3, n4}
    -- зададим узлы как перечисление, чтобы было более наглядно
    
    run cg/valid -- ещё дополнительно указываем модуль cg, так как
      -- предикат valid есть в двух модулях: relation и compgraph

    Примеры графов можно увидеть на следующем рисунке:


    Примеры вычислительных графов


    Можем заметить, что некоторые графы не совсем подходят для вычислений (есть подозрительные циклы).


    Подумав над свойствами вычислительных графов по отношению к обрабатываемым данным, мы придём к идее консистентности.


    Консистентность вычислительного графа


    Под консистентностью тут понимаются свойства графа по отношению к потоку данных, которые обрабатываются в графе.


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


    Понятно, что потерять данные можно только после получения. Мы можем классифицировать узлы по возможности потери данных:


    • активный узел — до него есть путь от истока, т. е. сюда могут прийти данные для вычислений;
    • неактивный узел — до него нет пути от истока;
    • безопасный узел — от него все пути ведут в сток, т. е. нет опасности подключения к узлу исходящего ребра от активного узла, переданные в него данные не потеряются.

    Граф консистентен, если в нём не теряются результаты вычислений и все вычислительные процессы конечны, т. е. мы получим результат за конечное время (все вычисления в графе останавливаются за конечное время, и мы можем считать результат из стока).


    Консистентности можно достичь, добавив ещё несколько свойств к свойствам вычислительного графа:


    • (7) нет циклов (для простоты описания). В реальных графах могут быть циклы при условиях, которые исключают бесконечную циркуляцию данных по путям цикла, но тут считаем граф ациклическим;
    • (8) все пути из активных узлов должны вести к стоку, т. е. нет потерь данных.

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


    То есть все узлы, которые являются корнями, кроме истока, это просто неактивные узлы.


    • (9) могут быть дополнительные корневые узлы, являющиеся неактивными узлами.

    И (правда, избыточное, оно следует из других) свойство:


    • (10) все активные узлы безопасны.

    Теперь уточним спецификацию вычислительного графа:


    Модуль compgraph.als
    module compgraph[node]
    
    open graph[node]
    
    pred active[edges : node->node,
                source: node,
                n : node
    ] {
      -- n находится в множестве узлов,
      -- достижимых от истока
      n in source.^edges
    }
    
    pred safe[edges : node->node,
              drain : node,
              n : node
    ] {
      -- если есть ещё листья, кроме drain,
      -- то не один путь из n
      -- не должен вести в эти узлы
      -- и n не должно быть одним из
      -- этих узлов
      no n.*edges & (leaves[edges] - drain)
      -- одно из свойств безопасных узлов, что
      -- можно подать туда данные из активных узлов
      -- и данные не будут теряться,
      -- таким образом, должен быть путь до drain
      drain in n.*edges
    }
    
    pred valid [edges: node->node,
                source : one node, -- свойство 1
                drain : one  node -- свойство 2
    ] {
      edges.connected -- так как мы ослабили ограничения
                      -- на корни и вершины (теперь и
                      -- тех и тех может быть не по одной),
                      -- то граф может быть не графом, а
                      -- лесом, поэтому нужно дополнительное
                      -- условие connected
      edges.dag -- свойство 6 и 8
      source in edges.roots -- свойство 1, 4 и 9
      drain in edges.leaves -- свойство 2, 4 и 8
      all n : edges.roots - source |
        not active[edges, source, n] -- свойство 9
      all n : edges.nodes | -- 10 свойство
        active[edges, source, n] => safe[edges, drain, n]
    }

    Для экономии времени и места картинки с уточнёнными вычислительными графами приводить не буду.


    Операции над вычислительным графом


    Для работы с вычислительными графами нам нужны операции.


    Сначала подумаем, как граф будет жить в системе и что из этого может следовать.


    В простейшем случае жизнь графа состоит из шести этапов:


    1. создание графа;
    2. проверка валидности графа;
    3. запуск данных в граф;
    4. работа графа;
    5. прекращение подачи данных;
    6. уничтожение графа.

    Изменение работающего графа не подразумевается. Сценарий простой и для большинства задач подойдёт. Не надо заботиться о консистентности графа по отношению к данным во время работы: после создания граф валидируется и далее не меняется.


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


    Это серьёзно усложняет задачу.


    Подумаем о том, как менять граф во время работы, чтобы изменения не нарушали его консистентность.


    Предположим, у нас уже есть валидный и работающий граф.


    Сначала подумаем, какие операции нам минимально необходимы:


    • добавление нового узла и дуги (граф задаётся дугами, поэтому добавить новый узел без связей не получится);
    • добавление дуги;
    • удаление дуги;
    • удаление узла и связанных с ним дуг.

    Новый узел при добавлении очевидно считается неактивным.


    Основные свойства определяются дугами, поэтому рассмотрим добавление дуги между узлами.


    Соединять узлы мы можем несколькими вариантами:


    1. неактивный -> неактивный;
    2. неактивный -> активный;
    3. активный -> неактивный;
    4. активный -> активный.

    Первый и последний вариант тривиальны, а второй и третий уже интереснее.


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


    Остался самый интересный вариант, третий: активный -> неактивный.


    Такое подключение будет безопасным, только если:


    • неактивный узел безопасен;
    • не образуется циклов.

    Опишем операции в виде предикатов над графами, которые связывают граф до и после операции.


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


    Операция добавления дуги
    pred connect[
      old_edges : node->node,
      new_edges : node->node,
      source : one node,
      drain : one node,
      from : one node, 
      to : one node
    ] {
      -- ребра ещё не было
      from->to not in old_edges
    
      -- from недостижим из to,
      -- чтобы не возникло цикла
      from not in to.*old_edges
    
      -- to должен быть узлом графа,
      -- иначе граф может стать
      -- лесом
      to in (old_edges.nodes - source)
    
      -- подключение к to должно быть
      -- безопасно, то есть передаваемые
      -- данные в to не потеряются
      safe[old_edges, drain, to]
    
      -- новый граф определяется рёбрами,
      -- берём все старые рёбра и добавляем
      -- новое ребро
      new_edges = old_edges + from->to
    }

    Предикат connect покрывает все случаи добавления узла с ребром или только ребра к графу.


    Давайте проверим, что connect сохраняет валидность графа:


    open compgraph[node] as cg
    
    sig node {}
    
    check {
      -- для всех возможных наборов рёбер r1, r2
      all r1, r2 : node->node |
      -- для всех возможных узлов source, drain, from, to
      all source, drain, from, to : node  {
        -- r1 является валидным вычислительным графом с
        -- source/drain истоком/стоком
        -- и r2 является графом r1 с добавленным операцией
        -- connect ребром from->to
        (cg/valid[r1, source, drain] and
         connect[r1, r2, source, drain, from, to])
        -- это влечёт то, что r2 + source/drain
        -- также является валидным вычислительным
        -- графом
        implies cg/valid[r2, source, drain]
        -- то есть операция connect сохраняет валидность
        -- вычислительного графа
      }
    } for 8

    Результат
    Executing "Check check$1 for 8"
       Sig this/node scope <= 8
       Sig this/node in [[node$0], [node$1], [node$2], [node$3],
         [node$4], [node$5], [node$6], [node$7]]
       Generating facts...
       Simplifying the bounds...
       Solver=sat4j Bitwidth=4 MaxSeq=7 SkolemDepth=4 Symmetry=20
       Generating CNF...
       Generating the solution...
       8374 vars. 168 primary vars. 22725 clauses. 108ms.
       No counterexample found. Assertion may be valid. 26904ms

    Alloy не смог найти контрпример во всём пространстве конфигураций графов с количеством узлов до восьми включительно. Это большое пространство, "168 primary vars" говорит о том, что оно размером $2^{168}$ возможных значений основных переменных. И это заняло на среднем ноутбуке меньше 30 секунд!


    То есть мы можем быть вполне уверены, что операция connect сохраняет валидность любых вычислительных графов.


    Теперь обратная операция, удаление дуги:


    Удаление дуги
    pred disconnect[
      old_edges : node->node,
      new_edges : node->node,
      source : one node,
      drain : one node,
      from : one node,
      to : one node
    ] {
      -- рёбра есть в старом графе
      from->to in old_edges
    
      -- при удалении ребра from
      -- должен остаться безопасным
      safe[new_edges, drain, from]
    
      -- граф должен оставаться связанным
      new_edges.connected
    
      -- удаляем ребро
      new_edges = old_edges - from->to
    }

    Пробуем:


    open compgraph[node] as cg
    sig node {}
    check {
      all r1, r2 : node->node |
      all source, drain, from, to : node  {
        (cg/valid[r1, source, drain] and
         disconnect[r1, r2, source, drain, from, to])
        implies cg/valid[r2, source, drain]
      }
    } for 8

    Ого! Найдены контрпримеры! Парочку из них можно увидеть на следующем рисунке:


    Контрпримеры для disconnect


    Дуги, помеченные как r1, — это дуги графа до операции disconnect, r2 — после неё. Там, где есть r1, но нет параллельной ей r2, эта r2 и была удалена операцией.


    Видно, что причина контрпримеров — это удаление единственной дуги from->to, в случае когда source (он же from) перестаёт быть связанной вершиной графа.


    Поправляем операцию disconnect:


    исправленная операция удаления дуги
    pred disconnect[
      old_edges : node->node,
      new_edges : node->node,
      source : one node,
      drain : one node,
      from : one node,
      to : one node
    ] {
      from->to in old_edges
      ( safe[new_edges, drain, from] or
       (from not in new_edges.nodes and
        from != source))
      new_edges.connected
      new_edges = old_edges - from >to
    }

    Результат проверки
    Executing "Check check$2 for 8"
       Sig this/node scope <= 8
       Sig this/node in [[node$0], [node$1], [node$2], [node$3], [node$4], [node$5], [node$6], [node$7]]
       Generating facts...
       Simplifying the bounds...
       Solver=sat4j Bitwidth=4 MaxSeq=7 SkolemDepth=4 Symmetry=20
       Generating CNF...
       Generating the solution...
       8505 vars. 168 primary vars. 24808 clauses. 207ms.
       No counterexample found. Assertion may be valid. 18369ms.

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


    Полнота операций


    У нас есть множество валидных графов, а достаточны ли наши операции для построения любого валидного графа из любого валидного?


    Не окажется ли так, что мы не сможем поменять топологию работающей системы нужным образом? И она окажется в тупике и придётся останавливать и перезапускать всю систему?


    Давайте проверим:


    -- для любых двух валидных графов
    -- есть последовательность промежуточных валидных графов,
    -- такая, что два следующих друг за другом графа
    -- приводятся друг к другу за одну операцию
    check {
      all r1,r2: node->node | all source,drain: node |
      some intermediate : seq node->node {
         cg/valid[r1, source, drain] and cg/valid[r2, source, drain]
         =>
         intermediate.first = r1 and
         intermediate.last = r2 and
         all i : intermediate.inds - intermediate.lastIdx {
           let from = intermediate[i] |
           let to = intermediate[i+1] |
           some n1, n2 : node |
             connect[from,to, source, drain, n1, n2]
             or
             disconnect[from, to, source, drain, n1, n2]
         }
      }
    } for 3

    И вот тут мы получаем:


    Executing "Check check$3"
       Sig this/node scope <= 3
       Sig this/node in [[node$0], [node$1], [node$2]]
       Generating facts...
       Simplifying the bounds...
       Solver=sat4j Bitwidth=4 MaxSeq=4 SkolemDepth=4 Symmetry=20
       Generating CNF...
       Generating the solution...
    A type error has occured: (see the stacktrace)
    Analysis cannot be performed since it requires higher-order
    quantification that could not be skolemized.

    Что это значит?


    Мы столкнулись с ограничением Alloy: квантификация может быть только первого порядка либо должна сводиться к первому порядку.


    А здесь не получилось сделать сколемизацию квантора «some intermediate…», так как подкванторная переменная должна пробегать по структуре высшего порядка — последовательности графов.


    И к первому порядку такую конструкцию не свести.


    Иногда (но не так часто, как хотелось бы) можно переформулировать предикат так, чтобы он свёлся к первому порядку.


    Хотя уже есть higher-order Alloy, но он пока экспериментальный, квантификация высших порядков у него имеет существенные ограничения по размеру моделей. Она катастрофически замедляет моделирование, так как идёт через CEGIS — counter-example guided inductive synthesis.


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


    Если ослабить условие и проверять не достижимость любого валидного из любого валидного, а возможность сделать шаг между двумя валидными, которые отличаются на одно ребро, то получим:


    check {
      all edges, edges1 : node->node |
      all source,drain, from, to : node {
        (cg/valid[edges, source, drain] and
        cg/valid[edges1, source, drain] and
        edges1 = edges + from->to and
        edges1 != edges)
        =>
        some n1, n2: node | connect[edges, edges1, source, drain, n1, n2]
      }
    } for 7

    Эта проверка уже работает, и мы видим результат:


    результат проверки connect на полноту
    Executing "Check check$3 for 7"
       Sig this/node scope <= 7
       Sig this/node in [[node$0], [node$1], [node$2], [node$3],
         [node$4], [node$5], [node$6]]
       Generating facts...
       Simplifying the bounds...
       Solver=sat4j Bitwidth=4 MaxSeq=7 SkolemDepth=4 Symmetry=20
       Generating CNF...
       Generating the solution...
       6471 vars. 133 primary vars. 16634 clauses. 200ms.
       Counterexample found. Assertion is invalid. 116ms.

    Найден контрпример!


    контрпример


    Красные дуги — это дуги графа до шага, чёрные пунктирные — после шага. На этом шаге добавляется дуга from->to.


    Тут мы видим, что операция connect не позволяет добавить дугу от неактивной вершины к небезопасной (и, соответственно, неактивной).


    Поправляем connect:


    исправленная версия connect
    pred connect[
      old_edges : node->node,
      new_edges : node->node,
      source : one node,
      drain : one node,
      from : one node, 
      to : one node
    ] {
      from->to not in old_edges
      from not in to.*old_edges
      to in (old_edges.nodes - source)
      -- вот тут поправили
      active[old_edges, source, from] => safe[old_edges, drain, to]
      -- учитываем безопасность to только для активной from,
      -- и, так как to теперь может быть отдельной вершиной,
      -- как и from, то нужно добавить условие
      -- сохранения связанности графа
      new_edges.connected
      -- это стало очевидным, так как старая проверка
      -- стала давать контрпримеры :)
      new_edges = old_edges + from -> to
    }

    Проверяем снова:


    результат
    Executing "Check check$3 for 7"
       Sig this/node scope <= 7
       Sig this/node in [[node$0], [node$1], [node$2], [node$3],
         [node$4], [node$5], [node$6]]
       Generating facts...
       Simplifying the bounds...
       Solver=sat4j Bitwidth=4 MaxSeq=7 SkolemDepth=4 Symmetry=20
       Generating CNF...
       Generating the solution...
       6513 vars. 133 primary vars. 16837 clauses. 125ms.
       No counterexample found. Assertion may be valid. 291ms.

    Теперь всё нормально.


    Точно так же проверяем обратный шаг для операции disconnect. Там тоже будет контрпример, придётся внести правки:


    исправленная версия diconnect
    pred disconnect[
      old_edges : node->node,
      new_edges : node->node,
      source : one node,
      drain : one node,
      from : one node,
      to : one node
    ] {
      from->to in old_edges
      -- если удаляем исходящее ребро из активной вершины,
      -- то она должна оставаться безопасной
      active[old_edges, source, from] => safe[new_edges, drain, from]
      -- заметьте, что теперь не нужно анализировать на
      -- то, что вершина вышла из графа:
      -- (from not in new_edges.nodes and
      --  from != source)
    
      new_edges.connected
      new_edges = old_edges - from->to
    }

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


    Это означает, что, начав с минимального работающего валидного графа (например, source->drain), мы можем дойти до больших валидных графов с помощью операций connect/disconnect и всегда вернуться к начальному графу.


    Этого свойства хватит для построения широкого класса вычислительных графов (есть основание предполагать, что всех интересных на практике вычислительных графов или же вообще всех, но это требует более серьёзного доказательства).


    Что дальше?


    Дальше можно развивать идею в направлении локальности операций, например.


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


    То есть хорошо бы разработать операции со свойством локальности: им понадобится знание только об узлах, что участвуют в операции (признаки safe/active и пр.).


    При небольших ограничениях на возможные топологии графа эта задача решаема.


    Далее, хорошо бы проводить множество параллельных операций над графом одновременно.


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


    Либо можно изначально проектировать систему таким образом, чтобы операции были локальные и параллельные.


    Ещё хорошо бы ввести типы входных и выходных из узлов данных, чтобы конструировать графы с учётом специфики узлов обработки.


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


    А сколько времени ушло на эту модель вычислительного графа?


    На написание кода на Alloy и отладку спек ушло не более часа.


    Намного больше времени заняли сопровождающий текст и подготовка иллюстраций.


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


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


    Как поэкспериментировать с моделями графов?


    Установите Alloy Analyzer, скопируйте файлы из репозитория на GitHub — и экспериментируйте.


    А что нам даёт описание на Alloy?


    Тут всё довольно очевидно:


    • промоделировав высокоуровневую архитектуру и её свойства, мы будем уверены, что нам не придётся кардинально менять систему из-за проблем в архитектуре;
    • предикаты, выражающие основные свойства системы, можно использовать, чтобы расставлять assert’ы в коде, писать статичные и динамические чекеры и т. д.;
    • мы можем на основе моделей сделать направленные тесты на краевые случаи (по мотивам найденных во время отладки контрпримеров);
    • При расширении функциональности системы мы можем сначала посмотреть, как новая функциональность работает со старой на моделях, а затем уже её реализовывать в коде, что позволяет развивать систему стабильно и предсказуемо. Например, при добавлении новых операций легко проверяется то, что они сохраняют консистентность вычислительного графа.

    Заключение


    Сейчас разработка серьёзного ПО уже немыслима без грамотного инженерного подхода. Facebook, Google, Microsoft, Amazon уделяют много внимания и сил разработке надёжных систем и ПО.



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


    Обычные agile-подходы во многих областях недостаточны для быстрой адаптации к рынку, нужна быстрая адаптация с минимумом ошибок.


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


    И тут на помощь придёт инженерный подход.


    Во многих областях разработку ПО можно и нужно вести в рамках гибких методологий с применением инженерных методов.


    В следующих статьях я собираюсь подробнее рассказать о требованиях и спецификациях, их плюсах, минусах, возможностях и ограничениях, о других весьма полезных инструментах (TLA+/TLC, B-method/Atelier B, Promela/SPIN). Постараюсь сопроводить статьи примерами использования инструментов.


    Библиография


    Книги для погружения в область


    Тут собраны книги, которые отличаются практическим подходом, минимумом сложной математики, максимумом объяснений и примеров. Список упорядочен по возрастанию сложности.


    1. Michael Jackson Problem Frames: Analysing & Structuring Software Development Problems
      Хорошая книга об анализе проблем (не способов решения!), которые встают перед разработчиками ПО. Будет интересна тем, кто хочет грамотно анализировать задачи и составлять требования.
    2. Daniel Jackson Software Abstractions: Logic, Language, and Analysis
      Книга о model finder Alloy и его принципах. От читателя особой подготовки не требуется, но нужны внимание и вдумчивость. Поможет понимание реляционной алгебры (операции join, транзитивного замыкания отношений). Но это необязательно, в книге всё хорошо объяснено.
    3. Юрий Карпов. MODEL CHECKING. Верификация параллельных и распределённых программных систем
      Хорошая обзорная книга о моделировании. Доходчиво написана, рассмотрены все основные темы, приведено множество примеров. Никакой серьёзной подготовки от читателя не требуется, знания матлогики и дискретки в объёме стандартной вузовской программы более чем достаточно.

    Примеры практического применения Alloy


    1. Pamela Zave. How to Make Chord Correct
      С помощью Alloy была составлена модель алгоритма DHT Chord, найдена ошибка (именно в алгоритме, так что все реализации содержали её), предложена исправленная версия алгоритма. Яркий пример того, как бывает полезно формально специфицировать и моделировать алгоритмы.
      1. Примеры спецификаций
        В репозитории много примеров спецификаций на Alloy, часть которых взята из промышленных задач.

    Блоги


    1. Hillel Wayne
      Много интересного материала и примеров. Лёгкий стиль, простая подача. Рекомендую тем, кто начинает изучать моделирование.

    Презентации


    1. Ю. Г. Карпов, И. В. Шошмина, А. Б. Беляев. Верификация параллельных и распределённых программных систем
      Интересная презентация, где хорошо объясняется, что такое моделирование и зачем оно нужно.

    Alloy


    1. Alloy Analyzer + Higher-Order Alloy
      Инструменты для работы со спецификациями на языке Alloy.
    2. Online Tutorial
      Материал немного устарел, но может быть полезным для новичков.
    3. Tutorial Materials
      Обучающие материалы.
    Яндекс
    641,86
    Как мы делаем Яндекс
    Поделиться публикацией

    Комментарии 75

      +8

      При том, что такой подход выглядит многообещающе, сколько ресурсов (человеков) он потребляет? Более того, если называть это "инженерным" подходом против "ремесленного", то сколько широкоиспользуемого ПО было написано таким образом? СУБД, операционные системы общего назначения, веб-браузеры, веб-сервера, графические/текстовые редакторы?


      В целом такой подход подразумевает, что цена пропущенного бага такова, что "никаких денег не жалко" на его предотвращение.


      Мы точно хотим, чтобы стержни опустились в реактор, даже если на эти 3000 строк уйдёт год работы десятка программистов.


      Но точно ли мы хотим год работы десятка программистов на безупречную работу фильтра "комикс" в графическом редакторе?

        0
        Ну понятно, что начинать надо с критичных областей, но как упомянуто в статье, инструменты развиваются и в какой-то момент может оказаться, что так дешевле разрабатывать даже фильтр в графическом редакторе, ибо не надо долго ловить баги.
          +1

          Тут же дело не в инструментах, а в полноте требований. Никакой инструмент не поможет разработать хорошие требования быстрее, чем требуется для осознания всех особенностей предметной области. А дальше там вопрос бюджета (денег, времени).

            +1
            Это хороший вопрос, про полноту требований и тд.

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

            В результате — забиваем гвозди микроскопами, пытаемся ломом починить микросхемы и пр. Получаем в результате больших плохоподдерживаемых монстров из сильносвязанного спагетти-кода и пр.

            Хотя весьма хорошо развивается область Requirements Management, есть хорошая литература по проблематике анализа и разработки требований (например, уже упомянутая в статье «Problem Frames») и тд. То есть, есть методики, инструменты и пр. для того, чтобы и к разработке требований подходить профессионально и серьёзно.

            Причем современные инструменты позволяют серьёзно уменьшить затраты усилий на хорошую проработку требований. С требованиями сейчас тоже можно работать итеративно в стиле agile.

            Очень интересный пример, когда сначала проанализировали требования, затем написали спеки и потом только стали кодить: OpenCOM RTOS. В итоге объем кода, по сравнению с предшествующим вариантом ПО, уменьшился на порядок (в 10 раз, как пишут в книге). Что было удивительно даже для самих авторов проекта, они даже не предполагали настолько сильный эффект.
          0
          Изначально статья была чуть больше (раза в два :) ), но для публикации это показалось слишком объёмным и поэтому оставлено было только самое интересное с точки зрения разработчиков. Вот в первоначально варианте и была большая мотивировочная часть, где как раз и писалось про то, что везде нужен разумный подход и нет смысла очередную игру «тетрис» для мобильников разрабатывать используя, например, формальные методы.

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

          Рекомендую посмотреть примеры в блоге Hillel Wayne, там видно, что моделирование можно легко и малозатратно применять даже для моделирования логики UI (в статье есть ссылка на это).

          Одна из целей данной статьи — показать, что моделирование (поиск и проверка моделей) сейчас стало весьма дешёвым и удобным в использовании и его вполне можно применять в весьма широком классе задач.

          Естественно, нужно разумно подходить ко всем используемым инструментам и хорошо понимать, где и какие инструменты стоит использовать. Но для этого нужно минимальное знакомство с инструментами, на что и направлена данная (и последующие) статья.

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

          Данная статья эти вопросы оставила в стороне, так как в основном такие вопросы для разработчиков существенно менее интересны, чем технические подробности и примеры применения.
          +2
          Тема очень крутая, без формальных методов просто страшно делать софт для критичных областей, так что пока цивилизация не дозреет до понимания важности таких подходов будет стрёмно. Ну и пока работы требующей таких знаний считай нет, хотя было бы интересно.
          К сожалению это вам не новый язык/фреймворк — сходу не вскочишь, нужно приличное количество сосредоточенной работы (поэтому пример я пролистал, ибо работа), по хорошему самое время ботанить такие вещи было во время учёбы, но увы.
            0

            Спасибо за Alloy. Уже пробовал TLA+ на учебных задачах, классная вещь.


            Ещё было бы прикольно иметь фреймворк, который генерил бы шаблон под спеку по UML диаграмме, чтобы можно было бы изящно встроить model-checker'ы в пайплайн разработки, но не знаю есть ли уже такое

              0
              Ну даже в теории это означает что UML диаграмма должна быть в каком-то семантическом формате, что-то вроде PlantUML
                0
                У меня была (и есть) немного другая идея: по спеке генерить код, который можно было вставлять в код рабочего продукта и снимать трассу выполнения. И эту трассу отправлять в параллельно бегущий model-checker (например, TLC), который бы сравнивал трассу на соответствие модели.

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

                Это позволило бы быстро ловить ошибки в логике ПО, где эта логика расходится с моделью.
                И, кажется на первый взгляд, это вполне можно применять даже в продакшн-коде (зависит от величины модели и её детализации), когда рядом с боевым кодом всегда бежит проверяющий автомат и сразу сигнализирует, если вдруг что пошло не так (например, может приостановить боевой экземпляр ПО, запустить gdb attach, закрыть машину от нагрузки и позвать службу поддержки для решения проблемы).

                Таким образом можно будет ловить проблемы на очень ранних стадиях, до того, как эффект от проблемы стал существенным (например, до того как положили в БД некорректные данные).
                0
                Эх, ностальгия за теми временами, когда был «Водопад», спецификации тщательно оговаривались, а затем замораживались на время разработки. И работало все как надо, а не только выглядело красиво, и эффективных менеджеров еще не завезли с их эджайл, оутсорсом, корявыми требованиями и 5 днями на разработку взлетной программы для боинга.
                  0
                  Основная проблема даже не водопад vs agile (моделирование и даже некоторые методы верификации нормально совмещаются с agile), а в том, что в погоне за новомодными методами, языками, фреймворками и тд. утрачивается самое важное качество разработчика — способность думать и анализировать. Хотя сейчас есть очень хорошая инструментальная поддержка для анализа архитектурных решений, алгоритмов и пр., что позволяет проводить серьёзный анализ решений в разработке с относительно небольшими трудозатратами.
                    +1
                    Я идею, к сожалению, не уловил. Как погоня за фреймворком влияет на способность думать и анализировать? Возможно, фреймворк позволяет отгородиться от некой реализации чего-то сложного или шаблонного, что сократит время разработки, но думать и анализировать, пока что, для разработчика — главный навык. Это же какой такой инструментарий серьезный есть для анализа архитектурных решений и алгоритмов? Я не знаю, где вы работаете, но из тех компаний, где я работал, без способностей решать какие-то задачи никого не брали. И фрейворки в большинстве хороших компаний используют с особой осторожностью, взвешивая все за и против. Проблема в том, что хорошие компании часто теряют клиентов из-за тех, кто выбирает дешевле и быстрее, а выбирают их менеджеры, которые не видят разницы между сениором и джуниором, видят только цифры, так и появляются компании индусов, которым и требования не нужны, и сроки минимальные, после них никакой документации не остается и никакие архитектурные решения не применяются. Но это не из-за погони за фреймворком, а потому что так дешевле и быстрее.
                      0

                      У молодого специалиста время всегда в дефиците. Нужно и что-то поизучать и погулять и пиво попить :)


                      А современные фреймворки, языки, NoSQL БД и пр. плодятся как грибы после дождя, ты ещё не успел до конца освоиться с Ruby/Rails, тут выходит более модный Django/Python, все начинают обсуждать его и тд. (я не силён в вебе, поэтому пример может быть несколько неправильным)


                      Всё это отвлекает внимание, требует время на изучение и пр.


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


                      думать и анализировать, пока что, для разработчика — главный навык

                      С этим-то я как раз не спорю совсем. Я лишь говорю о том, что сейчас много инструментов, способов и методов, которые могут существенно помочь в анализе.


                      Но этим инструментам, методам и пр. совсем не уделяется должного внимания.


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


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


                      Кому из молодёжи будет интересно на этом фоне сесть и начать вдумчиво читать "Specifying Systems" Лампорта?


                      Более того, многие даже не знают, что можно свой свежепридуманный алгоритм или ещё какую-нибудь идею быстро проверить на model-checkers/model-finders.


                      И цель этой статьи немного рассказать о том, что есть интересные инструменты, которые помогают разрабатывать и анализировать архитектуру, алгоритмы и пр.


                      без способностей решать какие-то задачи никого не брали

                      Решать задачи зачастую бывает недостаточно. Иногда нужно решать и гарантировать определённые свойства решения, вот о способах гарантировать определённые свойства решения и идёт речь в статье.


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

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

                        –1
                        Вы молодых специалистов с интернами-студентами путаете. Но я все равно не сильно понял к чему это. Все тут хают университеты за то, что они учат основам и фундаментальным вещам в информатике и математике, а вот фрейворкам и новым модерновым штукам не учат. Я как раз таки считаю, что университеты все правильно делают, не хватает практики только. Фреймворк, как вы правильно заметили, это проходящее, а вот основы остаются. И если вы не делаете сайтики, то ваши фундаментальные знания и умения ценятся выше знания фремворков. Так что тут как раз таки все в порядке, как по мне. model-checkers не используют даже старые дядьки с опытом в 20 лет и больше. Просто потому, что любая современная IDE имеет встроенные проверки на race conditions, потенциально возможные исключения и тп и тд. Я бы не рекомендовал читать Лампорта просто потому, что литература устаревшая и специфичная. На сколько я знаю, тот-же TLA больше не используется. Но в любом случае подобная литература явно не для новичков.
                        У тойоты залипал газ из-за отсутствия интеграционного тестирования(коврик не давал педали газа отжаться).
                          +1

                          По пунктам контр-аргументировать будет долго, поэтому только самые некорректные прокомментирую:


                          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


                          Там не просто "коврик" был. Весьма интересный материал по ссылке, рекомендую.

                    0
                    Проблема в том, что с тех пор мир изменился, бизнес изменился. Сейчас стала очень важна скорость изменений, так как много где стало, кто первый — тот и победил. И часто на коленке написанный facebook победит тщательно проектируемую noname социальную сеть.
                      0

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


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


                      Например, model-checkers/model-finders могут быть очень хорошим первичным фильтром для идей по изменению архитектуры, что позволяет серьёзно сэкономить время и силы на дальнейшей отладке и поддержке (да и просто писанины кода меньше, чем в случае прототипирования, тестирования, отката изменений и пр.).


                      Если у вас есть формальная отлаженная спека ПО (например Alloy и/или TLA+), то на ней можно быстро тестировать реализуемость нового функционала, который серьёзно может затронуть архитектуру ПО и соответственно результатам моделирования корректировать вносимые изменения, что позволяет в серьёзной степени исключить в дальнейшем длительную отладку для поиска редкого критичного бага, который проявился только у потребителей ПО под боевой нагрузкой, переписывание огромного объема кода, чтобы скорректировать такие баги (и как правило, это переписывание — просто обкладывание костылями, что множит проблему) и тд.


                      TLA+/Alloy и тд спеки очень хорошо разрабатываются итеративно и иерархически, что хорошо сочетается с agile подходом. И работать со спеками не сложнее чем работать с обычными исходниками.

                        0
                        А когда победит начнёт тонуть из-за наколенного кода который невозможно поддерживать и либо утонет (ибо стартапы напишут новый наколенный код быстрее и победят его), либо начнёт юзать инженерные методы.
                          +1
                          В идеальном мире да. Все зависит от конкретного рынка. Например, facebook как-то не тонет (так как основная его ценность не в продуктах, а в пользователях). И они потиху стараются перестраивать все на нормальную архитектуру в уже летящем самолете. Это конечно гораздо сложнее и опаснее, но другие самолеты просто не успели взлететь.
                            +1

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

                      0
                      Спасибо за статью.

                      Юрий Карпов. MODEL CHECKING. Верификация параллельных и распределённых программных систем


                      Вы советуете книгу, которую нигде не найти :(
                        0
                        Спасибо за статью.


                        Да не за что.
                        Рад, что статья понравилась.

                        Вы советуете книгу, которую нигде не найти :(


                        К сожалению да, бумажный вариант думаю уже тяжело будет найти (хотя ещё относительно недавно видел его в продаже).
                        Но есть возможность электронного варианта: www.ozon.ru/context/detail/id/32561151
                          0
                          Из электронного сейчас должно быть несложно и недорого сделать бумажный, правда не знаю законно ли с купленного электронного издания делать бумажный, ведь мы живём в сумасшедшем мире, всё может быть.
                            0
                            Думаю распечатку для личного пользования одного экземпляра никто как преступление рассматривать не будет :)
                          0
                          Помню вроде у potan во френдах в фейсбуке был человек который сделал пособие по формальной верификации.
                            +2
                            Формальная верификация, во всяком случае как я её понимаю (строгое доказательство свойств, а-ля логика Хоара для верификации кода, зависимые типы и пр), это всё-таки вещь весьма трудоёмкая, даже с современными ATP и пр.

                            А вот model-checker/model-finders вполне себе доступная даже для повседневного применения обычными программистами. Конечно есть определённая кривая обучения, но просто несравнимая с кривой у хардкорных формальных методов.

                            Хотя и хардкор я тоже планировал рассмотреть в будущих статьях (есть идея попытаться кратко расписать формальную верификацию реализации TLSF аллокатора памяти в SPARK/Ada)
                              0
                              Помню вроде у potan во френдах в фейсбуке был человек который сделал пособие по формальной верификации.

                              Эта — Камкин А.С. Введение в формальные методы верификации программ: учебное пособие?
                                0
                                Точно не помню, но похоже на то.
                                  +2

                                  Неплохая книга, но Карпов для новичков будет намного понятнее и интереснее.


                                  У Камкина материал слишком сжат и уже нужен хороший уровень матподготовки.


                                  А если нужна хорошая обзорная книга по формальным методам, как ликбез, то мне понравилась вот эта: Understanding Formal Methods

                              +1

                              Что вы думаете про промежуточные варианты (типа Design-by-Contract + DSL)?


                              Мы смотрели в сторону формальных проверок, но пришли к выводу что они для нас запредельно дороги, потому что порог входа высокий и разработчику без магистерской степени объяснить тот же TLA+ очень затруднительно. Продать формальные методы команде тоже оказалось не просто. Критика была в духе: "код писать все равно надо", "это избыточность", "зачем писать спеку в странном псевдокоде", "лучше тратить время на ревью или тесты" и т.д. Это не говоря уже о том, что все эти инструменты допускают математически корректные, но семантически неадекватные (с точки зрения предметной области) модели. Последнее расстраивало архитекторов ("вот я написал абсолютную чушь, а TLA+ всем доволен", "мне теперь что, программировать на ТеХ-е?!", "к вашему птичьему языку надо еще страницу наратива на простом английском, потому что строгость есть, а семантики нет").


                              В итоге для критических вещей мы написали DSL компилятор на базе Scala, который генерирует гарантированно (ну, когда автор с командой не налажали) корректный код для структур данных и интерфейсов сервисов (с проверками целостности, инвариантами, трансформациями между представлениями и прочим) на нескольких языках. А программеры живут под DbC и доказывают друг другу корректность устно проверяя контракты на ревью.


                              Получилось по-моему не плохо. С одной стороны, пришлось пожертвовать универсальностью и строгостью, но с другой стороны удалось выйти за пределы "башни из слоновой кости" в поле, к "ремесленникам".


                              Продать это команде оказалось проще ("круто, я не должен писать тупой код и тесты к нему", "ура-валидация!", "картинки! Оно умеет клевые доки и картинки!11"). К тому же у нас теперь есть бюджет на развитие методов верификации, потому что использование генерации уже себя окупило много раз. В вашей терминологии это что-то вроде "мануфактуры", я полагаю ;-)

                                0
                                Что вы думаете про промежуточные варианты (типа 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 раз! меньше кода.

                                  0

                                  Спасибо!


                                  Вот это дискуссионный вопрос. Мне кажется тут больше от мотивации разработчика зависит, чем от его степени магистра/бакалавра и пр

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


                                  нужно серьёзное внимание уделять корректности кодогенерации

                                  Это да. Мы постепенно эволюционируем в этом направлении, и, кстати, количество поддерживаемого кода внутри компилятора постепенно снижается, по мере перехода не "правильные" методы.


                                  что-нибудь а-ля http://smc.sourceforge.net/

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


                                  PlantUML, Graphviz/Dot, Tex/Tikz? :)

                                  Дык мы через них и генерируем. Сначала был PlantUML, потом пришлось от него отказаться (баги + на статических диаграммах далеко не уедешь). Сейчас делаем интерактивные диаграммы с использованием Graphviz с web assembly напрямую.


                                  Хорошо мотивирует изучать TLA+ вот эта книжка...

                                  Спасибо за наводку!

                                    0
                                    Мотивировать инженера можно двумя путями — либо показав, что это круто и крутые чуваки так делают, либо спустив разнарядку сверху.

                                    Мне кажется путей мотивации всё-таки чуть больше. Например, что меня серьёзно мотивирует в формальных методах — это последующая экономия времени на отладку (отлаживать многопоточные приложения с плаващими логическими багами — это то ещё "удовольствие") и возможность, в случае model-checkers/model-finders, быстро проверять свои идеи.


                                    Сейчас делаем интерактивные диаграммы с использованием Graphviz с web assembly напрямую

                                    Спасибо за идею! Обязательно посмотрю подробнее. Для анимации взаимодействующих FSM'ок (интерфейсы/протоколы) возможно самое оно.

                                      0

                                      Скинул в личку, можем поделиться наработками.

                                  0
                                  А есть статья про это?
                                    0

                                    Про контракты + DSL + кодогенерацию?


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


                                    Так как подход действительно рабочий и зачастую даёт очень хороший эффект (в плане качества ПО по отношению к затратам на разработку).

                                      0

                                      Хмм. Как минимум я давно хотел перевести нашу методичку по DbC для Хабра...


                                      С материалами по DSL все сложно, на самом деле. Наше приключение с ним началось с пинка от CTO, что во многом определило вектор дальнейшего развития. Так сказать по баллистической кривой. Насколько далеко мы ушли от велосипеда сказать трудно. Пожалуйста не забывайте что мы прикладники ;-)


                                      Про DSL что могу вспомнить сходу:


                                      • Есть несколько хороших статей про то, как запилить DSL на Scala. В основном вариации на тему этого.


                                      • С формализмом я ничего напрямую применимого не нашел, ходил NorthEastern University на кафедру PRL, поил пивом людей со смежными интересами. Про интерпретаторы написано очень много чего. А вот про статические структуры не очень. Предлагают брать классические работы по системам типов и выводить оттуда.


                                      • Есть очень смешная поделка baysick которая демонстрирует некоторые приемы комбинаторного DSL. Практической пользы в последнем — никакой, разумеется. Никто так интерпретатор Бейсика писать не будет. А вот всякие декларативные системы правил так пишутся на ура.



                                      Про DbC — наша методичка начинается с отсыла к Бертрану Мейеру, так что наверное я бы начинал с него. Так же статья на вики, если хочется уж совсем на пальцах. Эйфель мы, конечно, не используем. У нас DbC адаптирован под Java и Scala.

                                        0

                                        Интересные ссылки.


                                        Правда подход внутренних 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 возволяют гибко двигать границу между протестированным кодом и отверифицированным.

                                          0

                                          Со внутренними DSL — это из области "чем богаты, тем и рады". Если уж сильно приспичило, в той же Scala можно использовать макросы (та же идея — манипуляция AST в соответствующей фазе компиляции). А если совсем по-взрослому, то можно сделать плагин для компилятора. Или подождать пока уважаемые люди (Евгений Бурмако и компания) наконец определятся с поддержкой мета-программирования. Обещали завезти к 2020 в Scala 3.


                                          В общем мы пытались, но потом решили отказаться. Работа с AST (в Scala) пока имеет два серьезных косяка, поэтому мы стараемся ее избегать:


                                          • во-первых IDE ничего не знает про ваши изощрения с деревьями. Поэтому либо трансформация тривиальная (трансформированное дерево после компиляции соответствует типу из контекста. т.н. blackbox), либо отрубает практически все вещи которые любят разработчики — от подсветки синтаксиса до подсказок и рефакторинга (т.н. whitebox). Даже на среднем проекте (сейчас у нас все DSL определения занимают порядка 105K строк) это уже очень грустно. Встроенные DSL выражения таки являются корректными выражениями на "основном" языке, поэтому с ними такой проблемы нет.
                                          • стоимость разработки новой фичи сильно растет, потому что надо заниматься разбором и трансформацией этих самых AST. Ну и верификацией всего этого кода, что тоже стоит дорого. Доказывать-то приходится трансформацию всего поля AST. А в Scala 2 деревья ого-го, и ко всему прочему с атрибутами и мутируемые. Короче вообще адъ и Израиль. Если немножко раскорячиться можно добиться того, что выражения DSL являются выполнимым и возвращают практически то, что нам надо, даже с грубой типизацией. Т.е. нам на этапе компиляции надо просто выполнить выражение и "допроверить" корректность. Мы так затащили подмножество SQL-92 внутрь нашего языка для поддержки маппинга таблиц и ETL ;-).

                                          Про книжку Пирса совсем забыл. Огромное спасибо что напомнили!

                                  0
                                  Сейчас разработка серьёзного ПО уже немыслима без грамотного инженерного подхода. Facebook, Google, Microsoft, Amazon уделяют много внимания и сил разработке надёжных систем и ПО.


                                  Ага, только для разработки таким методом — надо иметь бюджеты как у Gooogle и Amazon.
                                  Или времени столько, сколько у NASA, когда никто не гонит за быстрый выпуск релизов.

                                  В целом штука занятная, но практической пользы в обычном IT — примерно столько, сколько от интеграла в анекдоте про интеграл.
                                    0
                                    практической пользы в обычном IT

                                    Проблема в том, что не бывает «обычного» IT. Все IT разное и в каждом случае можно и нужно использовать свои подходы. В определенных случаях (например, как в Яндексе) это все вполне применимо.
                                      0

                                      Видимо мне так и не удалось раскрыть основной посыл статьи: современные инструменты делают возможным применение формальных методов при небольших затратах на широком спектре практических задач.


                                      И, если вы посмотрите материал по ссылкам в статье (особенно в блоге Hillel Wayne), вы увидите, что применять формальные методы можно довольно легко и в довольно многих областях разработки ПО.


                                      Вопрос только в том, чтобы грамотно видеть, где применение каких инструментов принесёт наибольший эффект.


                                      Ну и естественно, нужно небольшое знакомство с этими методами и инструментами (на что, в основном и направлена статья)

                                      0

                                      Чем формальные спеки лучше TDD, кроме того, что они хуже и быстро устаревают?

                                        0
                                        Тем что TDD не имеет никакого отношения к гарантиям качества.
                                          +1
                                          Спеки также не дают гарантий. Наоборот, тесты и специфицируют и валидируют бизнес-логику одовременно. Плюс помогают кодированию и отладке. Мало того, фиксируют поведение, отслеживая регресс.
                                            0
                                            какую-то (неизвестно какую) часть, как-то (неизвестно насколько хорошо) они валидируют
                                              0

                                              Ну тесты и спеки пока пишут люди. И там и там уровень детализации и покрытия требованиями даже близко к 100% не приближаются. Причем даже в формальных спецификациях слишком много подразумевается и мало декларируется. Даже из простейших примеров статьи это понятно. А ведь там по сути хелловорд специфицируется.

                                                0

                                                Насчет "неизвестно насколько" я бы поспорил. Анализ покрытия вполне себе точная метрика.

                                                  +1
                                                  Нет, это ничего не значащая метрика, покрытие строк это не покрытие возможных вариантов
                                                    0
                                                    Покрытие вариантов впринципе недостижимо из-за проблемы остановки. Ну и комбинаторный рост тоже никуда не девается.
                                                      +2

                                                      В общем случае — да, проблема останова нам гарантирует отсутствие универсального алгоритма проверки свойств системы. Но современные средства позволяют просматривать огромные пространства состояний за разумное время. Тот же самый 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% покрытие не может гарантировать сохранение контрактов и инвариантов в коде (этого можно добиться только перейдя к формальной верификации).


                                                      Тести и покрытие это хорошо, но этого часто бывает недостаточно даже для однопоточного кода.

                                            +1

                                            Ну во-первых, спеки позволяют быстро проверить какие-то идеи и зачастую при меньших затратах, чем написание тестов и прототипов.


                                            Во-вторых устаревание спек сопоставимо с устареванием тестов при изменении функционала/архитектуры и пр. Во всяком случае, на мой взгляд.


                                            В-третьих, моделирование спек даёт такое покрытие, которое никакими тестами не достичь.


                                            В-четвёртых, в распределённых (и параллельных) системах зачастую такое огромное пространство состояний, что любые тесты тут просто бессильны.


                                            Ну и в-пятых, TDD и спеки совсем не являются антагонистами.
                                            Напротив, формальные спеки очень хорошо сочетаются с любыми тестами, так как на основе спек мы можем делать направленные тесты, которые бы максимально учитывали краевые случаи в системе.

                                              +1

                                              Это два ортогональных подхода.


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


                                              TDD проверяет выполнимость отдельных кейсов. Гарантии в совокупной корректности нет (мы можем показать что заказ пиццы три сыра за 10.99 в условиях успешной оплаты сработал как ожидалось, но сделать из этого вывод что он сработает во всех остальных случаях не можем).

                                                0
                                                Формальная спека позволяет убедиться, что ваш код в совокупности корректен и не приводит в запрещенные состояния

                                                Я бы уточнил: формальные спеки нужны в первую очередь для проверки алгоритмов, которые лягут в основу кода.


                                                Закрыть формально путь от формальных спек к коду можно (чтобы гарантировать соответствие кода спекам), но это уже довольно сложно и дорого в общем случае.


                                                Спеки в первую очередь позволяют не допустить серьёзных косяков в архитектуре, протоколах взаимодействия и тому подобных вещей.


                                                Хорошо закрывает путь от формальных спек к результирующему коду подход Event-B и тулы типа AtelierB. Но там спеки не настолько высокоуровневые, как Alloy или TLA+ и заточены в основном на описании FSM'ок и их постепенного уточнения (с формальным доказательством корректности уточнения) вплоть до результирующей кодогенерации в Ada или C.

                                              0
                                              В очень многих случаях формально отлаженную спеку создать попросту нельзя, поскольку:
                                              1. Юзеры не знают, чего они хотят — мы должны сделать продукт и предложить им, а они уже заценят.
                                              2. Заказчик не знает, сколько времени и денег он готов вложить в продукт, поскольку не понятно, насколько он «зайдёт»
                                              3. Программисты не знают, насколько сложно (и возможно ли вообще) будет реализовать часть фич


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

                                                  Я уже частично написал в комментариях ответы на эти вопросы, но повторюсь ещё раз:


                                                  1. У любых методов, и формальные тут не исключение, своя область применения и критерии применимости.


                                                  2. Нужно ко всему подходить разумно и формальные спеки использовать именно там, где они дадут выигрыш.


                                                  3. Для того, чтобы понимать где и какие формальные методы можно применять, нужно немного с ними ознакомиться, на что и направленна данная статья (ну и будущие статьи)



                                                  Далее, ответы на приведённые аргументы:


                                                  Юзеры не знают, чего они хотят — мы должны сделать продукт и предложить им, а они уже заценят.

                                                  Во-первых, я уже упоминал, что есть хорошие методы и инструменты для работы с требованиями, которые могут помочь в работе даже с быстро-меняющимися требованиями.


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


                                                  В-третьих, многие вещи с пользователями можно обсуждать на основе моделей и результатов моделирования (например, логику работы UI в виде состояний недетерминированных FSM'ок, нужно только выбрать подходящее, понятное для пользователя графическое представление). Это может оказаться существенно быстрее, чем писать и выкидывать прототипы.


                                                  Заказчик не знает, сколько времени и денег он готов вложить в продукт, поскольку не понятно, насколько он «зайдёт»

                                                  Ну тут могу только повториться: нужно хорошо понимать где и какие методы и инструменты применять.


                                                  И если у вас стартап по написанию игрушки для андроид на деньги венчурного фонда, то тут да, формальные методы и спеки могут быть излишни.


                                                  Программисты не знают, насколько сложно (и возможно ли вообще) будет реализовать часть фич

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

                                                  0
                                                  >> Как видно, спецификация краткая и понятная

                                                  Но давайте вспомним, что включает спецификация? 7 состояний и десяток переходов. Всего пара десятков элементов. Всего!

                                                  В реальности сложные задачи оперируют сотнями, а то и тысячами элементов. Простейший случай — связываем текстовое поле с БД. Одно единственное текстовое поле. Начнём с БД — нужна собственно база (где-то уже установленная), нужна связь с ней, нужны логины/пароли, нужна таблица значений, нужен селект конкретного значения, нужно чтение результатов селекта, нужно положить прочитанное в поле, нужно прочитать из поля в нужный момент, запихнуть в апдейт (который нужно написать), правильно выполнить апдейт, показать юзеру некий фидбэк. Вот такой самый минимальный минимум. Ради одного поля. Без логики. Только лишь тупое копирование.

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

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

                                                  Как некий предварительный шаг в сторону инструмента, который сделает за разработчика большую часть работы, такой подход уместен. В неких узких и очень дорогих нишах такой подход так же может быть применён. Но всё остальное (99.99%) — не из этой оперы. И это — главное, что стоило донести в статье.
                                                    +1
                                                    Но давайте вспомним, что включает спецификация? 7 состояний и десяток переходов. Всего пара десятков элементов. Всего!

                                                    Многие спецификации реально важных алгоритмов (Chord, Paxos и тд) тоже не сильно большие.


                                                    В реальности сложные задачи оперируют сотнями, а то и тысячами элементов. Простейший случай — связываем текстовое поле с БД. Одно единственное текстовое поле. Начнём с БД — нужна собственно база (где-то уже установленная), нужна связь с ней, нужны логины/пароли, нужна таблица значений, нужен селект конкретного значения, нужно чтение результатов селекта, нужно положить прочитанное в поле, нужно прочитать из поля в нужный момент, запихнуть в апдейт (который нужно написать), правильно выполнить апдейт, показать юзеру некий фидбэк. Вот такой самый минимальный минимум. Ради одного поля. Без логики. Только лишь тупое копирование.

                                                    Зачастую нет смысла делать такие детальные спеки. Выше где-то в комментариях, я уже писал о важном навыке — грамотно проводить уровни абстракции.


                                                    Зачастую действительно важные и критичные свойства системы можно проверить на весьма абстрактных (и соответственно небольших) спеках.


                                                    Зачем делать детальную спеку БД, записей, сетевых соединений и пр, если цель — проверить корректность алгоритма аутентификации пользователя?


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


                                                    В целом призыв «давайте наконец будем думать» выше уже нашёл подходящий ответ — думать дорого.

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


                                                    Хотя и без комментариев давно было ясно, что доказывание свойств программы — совсем не панацея.

                                                    Методов и инструментов широкий спектр. Доказывание свойств программы — это отдельная ветвь формальных методов и самая трудоёмкая.


                                                    В статье речь идёт не о формальной верификации программ. А о применении инструментов класса model-finders для исследования прототипа архитектуры.


                                                    Как некий предварительный шаг в сторону инструмента, который сделает за разработчика большую часть работы, такой подход уместен. В неких узких и очень дорогих нишах такой подход так же может быть применён. Но всё остальное (99.99%) — не из этой оперы. И это — главное, что стоило донести в статье.

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


                                                    В неких узких и очень дорогих нишах такой подход так же может быть применён. Но всё остальное (99.99%) — не из этой оперы. И это — главное, что стоило донести в статье.

                                                    Давайте сначала вы всё-таки более внимательно посмотрите статью, а потом уже думаю можно будет обсудить её более детально и предметно.


                                                    Так как именно такие стереотипы (как вышепроцитированное утверждение) я и пытаюсь немного развеять.

                                                      0
                                                      >> Зачастую действительно важные и критичные свойства системы можно проверить на весьма абстрактных (и соответственно небольших) спеках.

                                                      Сложный UI критичен весь. Юзеры должны работать не отвлекаясь на косяки программистов, но в какой-нибудь социальной сети мы встретим под сотню всяких формочек, приспособленных под ту или иную ситуацию, и каждая форма должна корректно взаимодействовать с пользователем. Иначе — негативное восприятие соц.сети и уход пользователей. И вот в такой ситуации — сколько времени потребуется вам лично для вникания во все эти сотни формочек, построения моделей, верификации и т.д.? Просто прикиньте, а потом просто будьте честными сами с собой. А после верификации программисты добавят массу ошибок реализации. Так есть ли вообще хоть какая-то выгода?

                                                      >> В статье речь идёт не о формальной верификации программ. А о применении инструментов класса model-finders для исследования прототипа архитектуры.

                                                      Ну скажем честно — model-finders ничего не находят. То есть вы сами создаёте (находите) модель, и только потом запускаете некие выборочные алгоритмы верификации. Это во первых. И во вторых — в статье как раз и идёт речь о верификации программ. Просто вы используете слово «алгоритм» для обозначения чего-то маленького, вроде бы доступного по цене, но при этом область верификации программ всего лишь декларирует цель максимум в виде полной программы, когда в реальности занимается именно узкими и маленькими алгоритмами, в точности как у вас в примере.

                                                      >> Основная часть статьи — это применение Alloy для исследования свойств архитектуры решения из области организации микросервисной системы.

                                                      Ну какая разница, как называется инструмент и как выглядят его команды, если он именно что занимается стандартным подходом, определяемым названием «верификация программ»? Да, инструмент использует не весь аппарат верификации, ну и что? Да, вы сами пишите скрипты верификации, но суть-то от этого почему изменилась? Вы показали ручной вариант верификации, но алгоритм «модель-проверка» никуда от этого не делся.
                                                        0
                                                        Ну какая разница, как называется инструмент и как выглядят его команды, если он именно что занимается стандартным подходом, определяемым названием «верификация программ»? Да, инструмент использует не весь аппарат верификации, ну и что? Да, вы сами пишите скрипты верификации, но суть-то от этого почему изменилась? Вы показали ручной вариант верификации, но алгоритм «модель-проверка» никуда от этого не делся.

                                                        Знаете, мне сложно дискутировать на таком уровне. Разговор в таком ключе мне представляется довольно беспредметным и неконструктивным.


                                                        Программа/алгоритм/модель и пр — это всё существенно разные понятия, и смешивать их в одну кучу — совсем не правильно.


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


                                                        Если честно, то model-checkers/model-finders — это не совсем про соф (даже совсем не про софт), а про любые системы, которые описываются формализмами, на которых базируется тот или иной инструмент. Например, TLA+ используется для проверки корректности не только софта, но и железа (когерентность кэшей, например).
                                                        Alloy можно использовать для исследования всевозможных структур, например, конфигурации топологий машин в сети и тд.


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

                                                          0
                                                          >> Программа/алгоритм/модель и пр — это всё существенно разные понятия

                                                          Как вам будет угодно. Но всё, что вы описали, на 100% относится к верификации программ. Только инструменты самодельные да плохо автоматизированные. В нормальных же инструментах код доказанной программы генерируется автоматически, а уровень используемых абстракций заметно выше, нежели простейший автомат. Ну и естественно, алгоритмы работы железных модулей там прекрасно доказываются.
                                                          0

                                                          Есть "пример успеха": Hyper-V был формально верифирован для Microsoft.


                                                          Как это вписывается в вашу "картину мира"?


                                                          ( А "сотни формочек" генерировались в Clarion из схемы БД ( .dct ) ещё в 90х.


                                                          И если сейчас это стало трудоёмкой задачей, то где прогресс средств разработки? )

                                                            0
                                                            >> Как это вписывается в вашу «картину мира»?

                                                            Как я и писал выше — 99.99% софта не создают и не будут создавать в ближайшем будущем по такой технологии.

                                                            >> А «сотни формочек» генерировались в Clarion из схемы БД

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


                                                              Решим задачу в стиле отдела кадров Google:
                                                              на первом месте 4 миллиарда Android OS, поделим на 3, пусть на 5 или 16, получим примерно долю Windows с включённым Hyper-V ( см. "device guard"). И не забудем прибавить мощности Azure.


                                                              Т.о. пример верифицированного массового ПО найден.


                                                              В нормальных же инструментах код доказанной программы генерируется автоматически


                                                              Не затруднит чуть подробнее? URL или менее общую терминологию ( для поиска ) ?


                                                              после верификации программисты добавят массу ошибок реализации


                                                              При генерации из создаваемых программистом в RAD среде Clarion "связке" .app + .dct файлов исходного кода ничто не мешает генерировать и пред- и постусловия, инварианты циклов и т.п.


                                                              ( Т.е. большой объём кода, если он более менее типичный — не препятствие )


                                                              Вы, видимо, просто не видели эти формочки в социальных сетях


                                                              Скажем так: если и видел, то не оценил в чём их сложность: в количестве полей? в нестандартных элементах?


                                                              ( Если последнее, то у C. есть и конкуренты: например, французская разработка. )


                                                              Т.к. если в логике обработки, то инженерный подход, как раз, будет не лишним.

                                                                0
                                                                >> Т.о. пример верифицированного массового ПО найден

                                                                Ну если ваша цель — победа, то вы, безусловно, победитель.

                                                                >> чуть подробнее?

                                                                Гуглите isabelle theorem prover. От него по встретившимся терминам найдёте массу аналогов.

                                                                >> большой объём кода, если он более менее типичный — не препятствие

                                                                Так вы уже сгенерировали свой фэйсбук или только теоретически доказываете, что вам это раз плюнуть?

                                                                >> если в логике обработки, то инженерный подход, как раз, будет не лишним.

                                                                И снова здравствуйте! Ждём следующей встречи после генерации аналога фэйсбука с применением инженерного подхода. Вы завоюете мир в один миг, стоит только всё правильно сгенерировать и инженерно подойти.
                                                                  0
                                                                  Гуглите isabelle theorem prover. От него по встретившимся терминам найдёте массу аналогов.

                                                                  Рад, что вы знакомы с ATP. Но это только небольшая часть инструментария для инженерного подхода.


                                                                  И применение ATP:


                                                                  1. Очень дорогое, требующее высокой квалификации
                                                                  2. Подходит только для весьма узких задач (докажите мне пожалуйста корректность алгоритма Paxos с помощью Isabelle/HOL)
                                                                  3. Требует частого ручного вмешательства пользователя в ходе доказательства свойств ПО (ну да, после этого кодогенерация автоматом, хотя и то, только для определённого подмножества целевого языка и как правило ещё и с хаками системы типов этого целевого языка (здравствуй obj.magic в Ocaml и аналоги в Хаскеле), либо генерация в бестиповый ЯП, типа scheme)
                                                                    0
                                                                    >> Но это только небольшая часть инструментария для инженерного подхода.

                                                                    Ну вот, а вы давеча говорили, что инструмент, мол, стал доступнее…

                                                                    >> докажите мне пожалуйста корректность алгоритма Paxos с помощью Isabelle/HOL

                                                                    А вы на автоматах с помощью указанных в статье инструментов это сможете? В смысле асинхронный обмен в них вообще поддерживается?

                                                                    А вообще по асинхронности и доказательству теорем в сети много данных, например такие или такие.

                                                                    И да, даже если некое частное решение всё же можно сделать на ваших инструментах, то всё равно это бесконечно малая часть от реальной потребности. Ну хоть с этим-то вы согласны?
                                                                      +1
                                                                      Ну вот, а вы давеча говорили, что инструмент, мол, стал доступнее…

                                                                      Вы специально троллите? Или просто настолько невнимательно читаете?


                                                                      Писал в статье я про класс инструментов, которые весьма существенно отличаются от 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+ модели.


                                                                      И да, даже если некое частное решение всё же можно сделать на ваших инструментах, то всё равно это бесконечно малая часть от реальной потребности. Ну хоть с этим-то вы согласны?

                                                                      С чем согласен? С вашими утверждениями, которые непонятно на чём основаны с учётом того, что вы вообще не вникаете в ответы на ваши комментарии и не читали статью (есть веские основания это полагать)?

                                                                        +1
                                                                        >> Вы специально троллите?

                                                                        Перечитайте свой предпоследний ответ. Там ясно написано — всё сложно и методов много. Собственно об этом я с самого начала и говорил, но вы упирались, а потом (в предпоследнем ответе) всё же согласились. Хотя да, теперь вы опять отказались, поскольку, оказывается не вы мне невнятно объяснили, но это я вас с самого начала плохо понимал и вообще даже статью не читал.

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

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

                                                                        Общие принципы я вам выше показал, вы мне в ответ начали про «я не читал статью». То есть с принципами вы не спорите, с ними согласны, но тогда зачем мне всё остальное? Если принципы я понял правильно, то уж инструмент выбрать я смогу, и при этом мне совершенно не обязательно опираться на некие примеры синтаксиса, приведённые вами. Мне не синтаксис нужен, мне нужна целостная картина применения инструмента, с упором на сокращение затрат на том или ином этапе разработки. И вот этого у вас просто нет (ну кроме заявлений про «инженерный подход творит чудеса»).
                                                      0
                                                      Спасибо за статью! В последнее время попадаются статьи на хабре, обосновывающие пользу спеков и моделей. Много слов сказано про новое ПО, которое удешевит инженерный подход. Но все примеры которые я нахожу связаны с довольно узким спектром задач. В большинстве проектов в IT и алгоритмы то никакие не используются, не считая библиотечных.
                                                      Можете сказать, насколько реально и целесообразно на данный момент использование данного подхода, скажем в обычном клиент — серверном решении (мобилка + сервер, например). Например, клиент запросил сервис по доставке еды — имеет в этом случае писать спеки и создавать модели?
                                                      Или, скажем, чуть более сложный заказ: клиент хочет разработать систему умного дома, имеет ли это смысл в этом случае? Если да, то можно ли увидеть пример?
                                                      Создание математической модели для алгоритма это одно, у тебя есть входные параметры, их область применения, это все очень похоже на математику и ее теоремы. А вот с бизнес логикой, где много висящих хвостов, ad hoc параметров все выглядит иначе.
                                                        +1
                                                        Спасибо за статью!

                                                        Пожалуйста! Рад что статья оказалась интересной.


                                                        В последнее время попадаются статьи на хабре, обосновывающие пользу спеков и моделей. Много слов сказано про новое ПО, которое удешевит инженерный подход. Но все примеры которые я нахожу связаны с довольно узким спектром задач. В большинстве проектов в IT и алгоритмы то никакие не используются, не считая библиотечных.

                                                        Могу посоветовать посмотреть блог Hillel Wayne, по поводу того какие в каких задачах может быть применёны model-checkers/model-finders. Там много простых примеров из разных областей. А его книга Practical TLA+ начинается с самого что ни на есть примера именно из бизнес-логики: пересылка денег между счетами.


                                                        Можете сказать, насколько реально и целесообразно на данный момент использование данного подхода, скажем в обычном клиент — серверном решении (мобилка + сервер, например). Например, клиент запросил сервис по доставке еды — имеет в этом случае писать спеки и создавать модели?

                                                        На вскидку, где я вижу применение моделей:


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


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


                                                        3. Промоделировать протоколы взаимодействия модулей в системе, чтобы посмотреть, нет ли каких-нибудь неочевидных/невалидных состояний (как пример, из-за сбоя в подтверждении запроса от одного модуля к другому, система зациклилась и начала пользователю складывать в цикле блюда в корзину из-за ретраев).



                                                        Это всё делается весьма быстро и малозатратно при определённом уровне навыков, но при этом может существенно повысить качество системы и user experience.


                                                        Или, скажем, чуть более сложный заказ: клиент хочет разработать систему умного дома, имеет ли это смысл в этом случае?

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


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


                                                        Если да, то можно ли увидеть пример?

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


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


                                                        Создание математической модели для алгоритма это одно, у тебя есть входные параметры, их область применения, это все очень похоже на математику и ее теоремы. А вот с бизнес логикой, где много висящих хвостов, ad hoc параметров все выглядит иначе.

                                                        Принципиальной разницы нет. Опять же рекомендую в блоге Hillel Wayne посмотреть примеры из разных областей.


                                                        Моделирование подходит для любых областей, где есть система с пространством состояний и дискретные переходы между ними (в общем случае недетерминированные).


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


                                                        Важно иметь некоторый опыт и навыки работы с тулами и опыт по абстракции и декомпозиции частей системы, чтобы потом на абстрактном уровне проанализировать их взаимодействие.

                                                        +1
                                                        Благодарю за развернутый ответ! Мне важно было услышать, что в эту сторону имеет смысл двигаться, в том числе если в проектах основная сложность в бизнес логике, а не в алгоритмах.

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


                                                        Моя мотивация для погружения в тему — это то, что мне импонирует подобный подход к задачам. Пока что мне не удалось вызвать интерес к этому ни у одного из коллег (объяснял, кидал ссылки на статьи). Типичный ответ — напишем примерные требования максимум, тесты напишем, разве мало? Планирую погрузиться в данную тему (через приведенную вами литературу и сторонние ресурсы) и все проверить на личном опыте, только так думаю смогу получить сторонников)).
                                                        Тут я думаю можно провести аналогию с университетским курсом: у студента конечно есть исчерпывающая информация в Фихтенгольце, но все хотят тоненькую методичку с конкретными первыми шагами, он их посмотрит, решит задачки, а там может и Фихтенгольца откроет.
                                                        Например, что мне выбрать TLA+ или Alloy? А где будет храниться спецификация? Прямо в проекте или отдельно? Спецификацию пишут на функцию, класс или в отдельных случаях лишь на модуль (если функции и классы малы и понятны)? Было бы здорово, если бы вы помогли сделать первые шаги, как это делают современные курсы по обучению. Это вызовет интерес и далее человеку будет гораздо проще двигаться.

                                                        П.С. Разрабатываемый умный дом базируется на open source технологии z-wave и проприетарном контроллере. Сейчас находится на стадии когда команду придавил обрушивающийся сверху фунционал, который был создан в лучшем стиле ремесленной разработки. У меня есть данные по проекту, было бы интересно посмотреть, как можно было бы ускорить разработку, если применять инженерный подход.

                                                          0

                                                          Немного прокомментирую по пунктам:


                                                          Пока что мне не удалось вызвать интерес к этому ни у одного из коллег (объяснял, кидал ссылки на статьи). Типичный ответ — напишем примерные требования максимум, тесты напишем, разве мало?

                                                          Да, к сожалению разработчики и менеджеры не понимают, что грамотное применение формальных методов может серьёзно помочь с точки зрения уменьшения затрат на разработку, отладку и поддержку (уменьшением вероятности серьёзных архитектурных багов). Ну и вероятность сдать проект в срок тоже может быть увеличена.


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


                                                          Лично я понял полезность 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+ с простыми примерами. Для начала — самое оно.


                                                          У меня есть данные по проекту, было бы интересно посмотреть, как можно было бы ускорить разработку, если применять инженерный подход.

                                                          С этим, наверное, лучше в личку. Может, после обсуждения получится на интересную статью материал сделать (при согласовании того, какие детали допустимо выносить на публикацию).

                                                          0
                                                          Я кстати, хоть и не имею опыта в этой сфере, считаю, что формальные методы это единственный способ обеспечить качество критичных систем и когда-то писал об этом на хабре.

                                                          Только полноправные пользователи могут оставлять комментарии. Войдите, пожалуйста.

                                                          Самое читаемое