3 марта в 08:28

«Лекарство от болезни»: автоматное программирование

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

Robson# / Flickr / CC

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

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

Откуда растут ноги


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

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

Автоматное программирование вступает в игру


Автоматное программирование — это парадигма программирования, при использовании которой программа или её фрагмент осмысливается как модель какого-либо формального автомата. Этот термин в 1991 году предложил заведующий кафедрой Технологии программирования Университета ИТМО Анатолий Шалыто.

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

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

В качестве примера использования автоматного подхода при построении алгоритма приведем решение задачи прямого обхода (0–9) двоичного дерева.


Пример двоичного дерева

Будем считать, что каждая вершина содержит свой номер и указатели на дочерние вершины. На языке C++ эта структура может быть представлена следующим образом:

struct Node { 
int id; // Номер узла 
Node* left; // Левый дочерний узел 
Node* right; // Правый дочерний узел 
};

Также введем в систему функцию put (int x), которая выводит номер вершины в выходную последовательность, и класс, реализующий стек со следующим интерфейсом:

template class Stack { 
void push(const T& x); // Поместить значение x в стек 
void pop(); // Удалить из стека верхний элемент 
const T& top() const; // Верхний элемент стека 
}; 

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


Схема связей автомата, реализующего обход дерева


Диаграмма переходов автомата, реализующего обход дерева

Отметим, что теория конечных автоматов была успешно применена компанией Corezoid для построения одноименной облачной платформы для ИТ-решений. Анатолий Шалыто говорит о необходимости внедрения этого метода в современную разработку: «Программисты — они ведь очень умные, и применяют автоматы, как и другие математические абстракции, когда считают нужным. А я говорю: всегда его [автоматное программирование] надо применять для описания программ со сложным поведением, в которых имеет место зависимость их поведения от предыстории».

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

P.S. Из приведенного текста может сложиться впечатление, что помощью автоматного программирования можно решать только «игрушечные» задачи. Однако это не так.

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

Правда, и при обучении вычислительным алгоритмам, автоматное программирование пригодилось: Георгий Корнеев и Матвей Казаков показали, что на его основе можно проектировать визуализаторы и автоматизировать их построение даже для весьма сложных алгоритмов дискретной математики, а не каждый раз писать их вручную, как «Бог на душу положит». Пример проектной документации приведен здесь, а вот пример такой документацией для сложного проекта.

С документацией для еще более сложного проекта можно ознакомиться вот тут. На сайте is.ifmo.ru есть еще много проектов, как студенческих, так и других, изучение которых сможет ответить на многие Ваши вопросы. С книгой Поликарповой Н.И. и Шалыто А.А. Автоматное программирование. СПб.: Питер, 2010 можно ознакомиться здесь.

И не фантазируйте – пишите: shalyto@mail.ifmo.ru.
Автор: @itmo
Университет ИТМО
рейтинг 263,00
IT's MOre than a University

Комментарии (27)

  • +1
    Можете более широко раскрыть вопрос границ применимости и неприменимости парадигмы автоматного программирования?
    • +3
      Подозреваю, тут как и с применимостью логики для решения любых математических задач. Вроде бы и да, но нет. Потому что комбинаторный взрыв при сложности отличной от hello_world.
      • 0

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

  • +2
    Как понимаю это паттерн машина состояний?
    • 0
      • +4
        Насколько я знаю, используется на ура в embedded-системах. Правда, не совсем понятно, при чем тут уважаемый ИТМО и проблемы с софтом на атомных станциях: если документацию похерили, то не все ли равно, на какой парадигме был основан исходник? Проблема явно в процессе, а не в том, как веселее описать алгоритм.
      • 0

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


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

        • +4
          Автомат с магазинной памятью — это разновидность конечного автомата (вики). Конечность у автоматов заключается в ограниченном множестве состояний.
          • 0

            И правда… Пора вспоминать курс теории вычислений.

          • –2
            В вики не так написано. Скорее уж, конечный автомат — это разновидность МП-автомата, с доп. ограничениями.
            • +1
              Это ересь. Термин «конечный автомат» не соотносится к какому-то конкретному автомату, тем более — как вы считаете — какому-то самому простому из них. В качестве контрпримера предлагаю Вам напрямую (без конверсии) получить недетерминированный автомат из Вашего понимания конечных автоматов как частного случая МП-автоматов.
              • 0
                Термин «конечный автомат» не соотносится к какому-то конкретному автомату, тем более — как вы считаете — какому-то самому простому из них.
                Тогда укажите, какой, по-вашему, самый простой автомат должен стоять в конце иерархии Хомского:
                1. КЗ-языки
                2. КС-языки — МП-автоматы
                3. регулярные языки — ?
  • 0
    Как мне кажется, при каждом изменении требований заказчика понадобится формировать новый граф состояний и фактически переписывать реализацию.
    • 0
      Если граф формируется по коду, то только реализацию.
  • +3
    В 1991-м был ЛИТМО. А по теме — не очень ясно чем автоматы лучше других способов при равной степени документации. До важных проектов прежде всего нужна подробная документация и хорошие тесты, в том числе нефункциональные. А автоматы, функции, обычные объекты, да хоть скрипты на брэйнфаке — дело десятое.
    • +1

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


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

      • +1

        Стоп. Мы об описании какого-то компонента программы в виде конечного автомата или об его реализации с использованием автоматной семантики?


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

        • 0

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

          • 0

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

  • 0
    Искал одно время книгу в бумажном варианте за авторством того самого Шалыто. Но так и не нашел. Озон молчит как рыба об лед.
    Джентльмены, если у кого есть бумажный вариант — куплю
  • +1
    Про Agda и Coq нет, низачет
    • 0

      Формальная верификация ещё в Ada 83 была.

  • 0
    Идея хорошая. Реализация — страшно сырая.
    Все давно украдено до нас
  • 0
    Хмм… Простите, конечно, но суть технологии раскрыта слабовато, т.к. обход дерева не раскрывает всей мощи автоматного программирования. А вот АЭС вполне можно запрограммировать набором конечных автоматов. Но и неавтоматные подсистемы будут нужны. Вообще говоря «автоматное программирование» к документации не имеет отношения. «Конечные автоматы», «машина состояний» — это парадигма построения алгоритма управления. А документация — это уже детали продукта. Документация может быть или не быть для любой парадигмы.
    В сложных системах управления конечные автоматы позволяют построить программу такой же структуры, что и управляемое устройство. В этом вся вкуснота. Автоматы позволяют не ломать голову над организацией программы (с неизбежными ошибками и архитектурными ограничениями), а просто по структуре аппаратной системы построить программную систему. Работает такая штука хорошо.
    Граф никогда не формируется по коду. Наоборот, код формируется по графу. Парадигма позволяет рисовать типовые графы состояний, и генерить по ним код.
    Если требования заказчика изменились, то графику придётся в любом случае менять, если Ваш проект сопровождается графикой. Если он не сопровождается графикой, тогда не придётся менять. Вопрос в сложности продукта. Если продукт сложный — без графа состояний никуда.
    Тов. Шалыто, рекомендующий пихать конечные автоматы всюду, демонстрирует классическую ситуацию, когда тема диссертации заняла человека всецело.
  • 0
    В рамках автоматного программирования предполагается, что программа пишется только после того, как была спроектирована

    Только предполагается? То есть с этим подходом всё-таки возможно писать программу без проектирования? Ненадёжное получается лекарство…
  • 0
    В принципе, ничего нового. Мое любимое учебное пособие по теории автоматов в ВУЗе было, емнип, 1974 года. Не помню уже, было ли оно чисто «железячным», или с приложением к программированию тоже, но это очевидный шаг, кмк.

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