Применение формальных методов валидации моделей для UI

Привет! Представляю вашему вниманию перевод статьи «FORMALLY SPECIFYING UIS» автора Hillel Wayne.

От автора

Относительно недавно я наткнулся на статью про Инженерные методы в разработке ПО, где vasil-sd рассказал про формальную валидацию спецификаций к создаваемым программным продуктам. В качестве инструментария был использован Alloy. Одним из основных лейтмотивов в комментариях был — разобрать статью в контексте какого-нибудь современного веб проекта, потому что дорогодолгосложно использовать формальные методы там, где все делают быстродешево. Так как автор ссылался на блог Hillel Wayne, где такие примеры были, я решил перевести что-то из его статей в качестве дополнения к основному тексту vasil-sd

Предупреждение:

• Все, что автор называет finite-state machine, я буду называть конечным автоматом или моделью конечного автомата.
• Часть терминологии я почерпнул из статьи, ранее мною упомянутой, об инженерном подходе к разработке. Тем не менее, тема для меня относительно новая, потому обоих авторов(как зарубежного, так и не очень) мог понять не так — не ругайтесь.

Формальная спецификация UI

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

Я люблю формальные методы. Недавно мой друг Кевин Лина(Kevin Lynagh) выпустил sketch.systems ¹, новый инструмент формальной спецификации для дизайнеров UI. Что ж, давайте выясним — сможет ли моя любовь к формальным методам победить мой страх?

Проблема

Еще в Edmodo я работал над пользовательским интерфейсом для нашего приложения «Snapshot». Это была наша первая вторая попытка заработать деньги: мы начали с того, что дали всем учителям бесплатную программу, а затем просили пожертвования или что-то типа того. Как видите, тогда Edmodo не отличались особой деловой хваткой. ²

В «Snapshot» учителя могут проводить «опросы» или «снимки»(«snaps») среди учащихся. Далее, программа агрегирует результаты опросов и предоставляет учителям несколько отчетов в реальном времени в следующих разрезах: «сводный» отчет, «по студентам» и «по стандартам». Кроме того, мы решили, что программа должна иметь отчет «ответы», который можно было б открыть из отчета «по студентам» и который давал информацию о неправильных ответах.

МЫ представляли себе, что пользователь перемещается между отчетами, нажимая необходимые кнопки, и что все отчеты должны быть доступны из других отчетов, за исключением ответов. Значение слова “доступны" в контексте переходов довольно неопределенно: это может означать “вы можете каким-то образом перейти к отчету”, или это может означать “в один клик перейти сразу к нужному отчету”. Все, что описано выше — лишь часть пользовательского интерфейса всего приложения, которое, помимо навигации в отчетах, имеет свою собственную систему навигации.

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

Конечные автоматы

Конечные автоматы(finite-state machine, FSM) — это одна из самых простых математических моделей теории абстрактных автоматов. У вас есть конечный набор состояний(states), набор переходов(transitions) между состояниями и набор событий(events, triggers), которые запускают переходы. Каждый переход привязан к событию, так что, если событие произойдет, состояние может измениться. ³ В нашей модели событиями будут “учитель нажимает кнопки". Ниже представлена модель конечного автомата для нашей текущей системы:

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

1. Если вы находитесь в сводном отчете, кнопка “сводка" не отображается или ничего не делает.
2. Если вы находитесь в сводном отчете, кнопка “сводка" сбрасывает отчет.

Мы выбрали второй вариант. Нашим исходным состоянием стал ”сводный" отчет. Обновленная модель:

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

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

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

Диаграммы Состояний Харела

Большинство из наших состояний имеют общую логику так называемого супер-состояния: все наши четыре «отчета» имеют одну и ту же логику выхода из системы, а основные три имеют одни и те же переходы. Если мы сможем сгруппировать их в отчет «родительское состояние», все, что нам осталось бы — это определить переход на «выход» и распространить этот переход в дочерних состояниях. Логика аналогична наследованию: дочерние состояния наследуют (или переопределяют) переходы родительских состояний.

Конечные автоматы с вложенными(nested) состояниями называются автоматами иерархического состояния(hierarchical-state machines), и существует несколько различных способов их формализации. Наиболее подходящий из способов записи моделей конечного автомата для UI — Диаграмма состояний Харела (Harel Statechart). ⁴ Правила для нее следующие:

1. Все родительские состояния абстрактны. Каждое родительское состояние должно определять дочернее состояние «по умолчанию».
2. Дочерние состояния автоматически наследуют все родительские переходы, но могут также переопределять их.
3. Переход может указывать на любое состояние. Если вы переходите в родительское состояние, вместо этого перейдите к его дочернему состоянию по умолчанию. Если дочернее состояние также является родителем, то состояние определяется рекурсивно.

Вы можете разрабатывать Диаграммы состояний Харела в Graphviz и каждый раз ужасаться множеству вершин, ребер и прелестям графического представления графов. Мы же будем использовать значительно более приятный пользовательский интерфейс от Sketch.systems:

Snapshot
  logout -> Login Page

  Reports
    summary -> Summary
    students -> Students
    standards -> Standards

    Summary*
    Students
      answer -> Answers
    Standards
    Answers
      close -> Students
    
Login Page
  login -> Snapshot

_{источник}

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

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

_{источник}

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

Проверка

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

Sketch.systems может проверить, если Диаграмма состояний Харела имеет корректный формат, но не может проверить поведение модели. Существуют и другие инструменты для определения состояний конечного автомата, в частности, диаграммы состояний UML, но все они ориентированы на спецификации уровня кода, а не на спецификации уровня системы. Их цель — в конечном итоге сгенерировать код C или Java из диаграммы состояний. Но они слишком низкоуровневые, чтобы проверять абстрактные свойства, а мы слишком высокоуровневые, чтобы хотеть генерировать код. Если мы хотим формализованной проверки, нам нужно будет описать нашу модель на языке спецификации общего назначения.

К счастью, для этого случая это довольно легко сделать. Для этого мы воспользуемся Alloy, так как в нем можно наиболее точно отразить структуру Диаграммы состояний Харела. ⁵ Мы можем использовать расширения сигнатур(signature extensions) для представления вложенных состояний: «Стандарты» расширяют «Отчеты» означает, что каждая частичка «Стандартов» также является «Отчетом», что эквивалентно утверждению, что это дочернее состояние в соответствующей Диаграмме Харела. Это упрощает определение переходов. Каждый из них представлен одним предикатом, принимающим время(t), начальное состояние(start) и конечное состояние(end), и объявляет, что состояние в момент времени t переходит от start к end за t.next. Несмотря на то, что родительские состояния абстрактны, мы все равно можем использовать их в качестве начала и воспользоваться родительскими переходами.

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]
}

Теперь мы можем проверить свойства нашей модели. Например, можно ли получить отчет «ответы», не проходя через отчет «студенты»?

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

Мы также можем смоделировать пример, когда кто-то выходит из системы и снова входит:

run {some disj t1, t2: Time | logout[t1] and login[t2]} for 7

Alloy предоставляет довольно широкии возможности спецификации. С проверкой некоторых свойств, например, тупиоков, могут возникнуть сложности. Тем не менее, я не первый человек, который видит, как хорошо Alloy работает с диаграммами состояний. Профессор Нэнси Дэй(Nancy Day) недавно анонсировала вариант Alloy под названием DASH, который добавляет первоклассную семантику Диаграмм Харела в Alloy. Вы можете прочитать об этом здесь.

Ценность

Есть ли ценность у всего этого? Что делает интерактивную диаграмму состояний лучше, чем просто заметки на английском языке? Определенно, диграмма становится ценее, когда вы масштабируетесь. Я помню, что в проекте Snapshot было около двух десятков экранов учителя, вложенных в несколько больших иерархий. Без формальной спецификации мы не могли бы проверить нашу работу. Насколько я помню, некоторые из ошибок, которые мы совершили:

• Мы забыли рассмотреть “закрытие отчета об ответе” как событие, и «ответы» стали тупиком
• Создание нового опроса имело кучу окружных маршрутов, которые нам действительно не нужны
• Мы не определили поведение пользовательского интерфейса после создания опроса, поэтому мы возвращали учителя на экран создания опроса, он думал, что в ходе ошибки опрос не был создан и создавал его повторно
• До нескольких экранов было трудно добраться, так что никто никогда к ним не переходил

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

Вывод

Мы обсудили формальную спецификацию взаимодействия пользователя с UI. Может ли моя любовь к формальным методам побороть мой страх перед UI? Черт возьми, нет. Если вы переходили по ссылкам на Sketch.systems, вы наверняка увидели, что можете прикрепить прототип на Javascript к своей диаграмме состояния. Это магия!

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

Кстати, эй, я консультирую по формальным методам. Расскажи своему боссу!

1. Предупреждение, я был одним из альфа тестроев. Большая часть моей обратной связи была вида “вам следует сделать это более сложным!”. Да, я так себе альфа тестер. ^[return]
2. В 2017 они получили 1 миллион и потеряли 20 миллионов. ^[return]
3. Конечная машина состояний имеет много общего с детерминированным конечным автоматом, что является важной составляющей частью компьютерной науки. Основное различие в области применения: применение детерминированного конечного автомата обосновано «множеством распознаваемых им регулярных языков”, применение конечной машины состояний “консистентностью спецификации” ^[return]
4. Основным конкурентом является Диаграмма состояний UML(UML State Diagram), которая в основном представляет Диаграмму состояний Харера, дополняя своими спецификациями кода. Она более выразительна, но сложно анализируема. ^[return]
5. Если вы не знакомы с Alloy, я написал несколько статей по нему тут и тут.

Автор: Александр

Источник