Formally Specifying UIs

Good UI is necessary to making correct software. If people have trouble using the product, they’re more likely to do the wrong thing. Personally, though, I can’t stand UI work. I don’t think it’s “beneath me” or anything, it just doesn’t quite mesh with my brain. Visuals and interfaces give me anxiety. Mad respect for the people who can handle it.

I love formal methods. Recently my friend Kevin Lynagh released Sketch.systems, a new tool to bring formal specification to UI designers.¹ Can my love of formal methods beat my fear of UI? Let’s find out.

The Problem

Way back in Edmodo I worked on the UI for our “Snapshot” app. It was our first second attempt to make any money: we’d start by giving all the teachers a free product and then ask for donations or something? Edmodo didn’t have great business sense.²

In “Snapshot”, teachers could assign students quizzes, or “snaps”. We’d aggregate the quiz results and give the teachers several realtime reports: a “summary”, a “by student” report, and a “by standard”. We were also supposed to have an “answers report” for the students report: if you clicked on one, you could see the questions they got wrong.

We have some concept of the user switching reports by clicking buttons, and all of the reports should be reachable from all the other reports, except the answers (which is only by grades). “Reachable” is ill-defined here. It could mean “you could eventually click through to get to a report” or it could mean “directly accessible”. This is just the UI for one part. The reports would have to be integrated with the rest of the app, which would have their own navigation quirks.

When a system starts getting complicated, we need to get precise. That means writing a specification. So how should we specify this? I see a teacher is on a given view and can take actions which change that view. That suggests to me we’re looking at a state machine.

Finite State Machines

A finite-state machine (FSM) is one of the simplest possible state machines. You have a finite set of states, a set of transitions between states, and a set of events which trigger transitions. Each transition is tied to an event, so that if the event happens, you may or may not change your state.³ In our case, the events would be “the teacher clicking on buttons”. Here’s what the FSM for our current system looks like:

I immediately see two problems with our UI. First, all FSMs need a starting state, and we don’t have one. When the teacher enters the reports page, which report should they see first? Second, we don’t specify what happens when you click a button while already on a page. This is ambiguous, as there’s two possible things we could do:

1. If you’re on the Summary report, the “summary” button isn’t shown or does nothing.
2. If you’re on the Summary report, the “summary” button resets the page.

In the product, we had the second case. Our starting state was the “Summary” report. Updated FSM:

This accurately represents our UI. It is also very cluttered. This is a big limitation of FSMs: they can’t handle lots of redundant transitions. Every single summary transition points at Summary, and the same holds true for student and standard.

This is especially problematic when you try to compose two FSMs. At any point the teacher could log out. If they log back in, they start on Summary again. This is the new FSM:

In order to add a logout feature we had to add four more edges. This quickly gets untenable. We need some way to represent “common” transitions. We can get this by adding nesting states, which complicates our formalism but simplifies our specs.

Harel Statecharts

Several of our states share a common superstate-esque logic: our four “Report” states all share the same logout logic and the main three share the same report transitions. If we can group them in a report “parent state”, we would only need to define a logout transition on the parent state and let it propagate to the child states. This is analogous to inheritance: child states inherit (or override) transitions from parent states.

State machines with nested states are called hierarchical-state machines and there are few different ways to formalize them. The most appropriate notation for UI machines is the Harel Statechart (HSC).⁴ The rules are:

1. All parent states are abstract. Every parent state must define a “default” child state.
2. Child states automatically inherit all parent transitions, but can also override specific transitions.
3. A transition can point at any state. If you transition to a parent state, instead go to its default child. If that child is also a parent, repeat recursively.

You can design HSCs in Graphviz but it’s a nightmare of cluster subgraphs and lheads and rank tweaking. So let’s use the considerably-nicer Sketch.systems UI:

Snapshot
  logout -> Login Page

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

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

I’d recommend clicking the source link up there, as the diagram is interactive. You can click on the transitions and see how states change. That’s a big benefit of HSCs: not only are they formal and concise, they’re also kinetic. You can explore them.

In exploring, I found a bug with my state machine: You can transition directly from Answers to Standards. We can fix that by making Answers a direct child of Login instead of a child of Reports:

Ideally, we’d like to make these problems more obvious, which means using some form of automated verification.

Verification

There are two benefits to formal specification. One is implicit: the act of clearly expressing yourself leads to a better understanding of the system. The other is explicit: once we have a formal spec, we can check its properties. Does our UI have any dead-ends? Is it possible to get locked-out of a chunk of the UI? Are any of our transitions ill-specified?

Sketch.systems can check if an HSC is ill-formed but does not support verifying behavior. There are other tools for specifying state machines, particularly UML state diagrams, but these are all focused on code-level specs, not system-level specs. Their goal is to eventually generate C or Java code from the state diagram. But they’re too low-level to check abstract properties, and we’re too high-level to want code generation. If we want formal verification, we’ll need to rewrite our state machine in a general-purpose specification language.

Fortunately, for this case that’s pretty easy to do. We’re going to use Alloy here, as it can most closely mimic the HSC structure.⁵ We can use signature extensions to represent nested states: Standards extends Reports means that every Standards atom is also a Report, which is equivalent to saying it’s a child state in the corresponding HSC. This makes it easier to define the transitions. Each is represented by a single predicate taking a time, a start state, and an end state, and declares that the state at t goes from start to end by t.next. Even though parent states are abstract, we can still use them as the start, which gives us parent transitions.

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

Now we can verify properties of our state machine. For example, is it possible to reach answers report without going through the students report?

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

We can also ask it to give us an example where someone logs out and logs back in again:

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

Alloy also gives us greater depth of specification, as we can define atoms that aren’t states. There’s also some properties we can’t easily verify in Alloy, such as finding deadlocks. That said, I’m not the first person to see how nicely Alloy works with statecharts. Waterloo professor Nancy Day recently announced a variant of Alloy called DASH, which adds first-class HSM semantics to Alloy. You can read about it here.

Value

Does any of this add value? What makes an interactive HSC better than simply having a bunch of English notes? It matters a lot when you scale up. I remember the Snapshot project having about two dozen teacher pages nested under several larger hierarchies. Without a formal spec we couldn’t sanity-check our work. To the best of my memory, some of the mistakes we made:

• We forgot to consider “closing the answer report” as something a user would do, so that report became a dead-end
• Creating a new quiz had a bunch of circular paths we really didn’t need
• We didn’t have clear direction on what the UI was suppose to do after a teacher created a quiz, so we just dumped them back at the beginning of the quiz creator, so they’d end up thinking it failed and create multiple quizzes
• Several pages were hard to get to, so nobody ever went to them.

I think having a formal spec would have helped a lot here. The example I did above took about five minutes to write up, and even the full app could have been specced in under two hours. If that caught even one of those mistakes in the design phase, that would have saved us a ton of time.

Conclusion

We just talked about formally specifying user interactions. Does my love of FM trump my fear of UI? Hell no. If you checked out the Sketch.systems links, you’d have seen that you can attach a javascript prototype to your statechart. That shit’s witchcraft.

But I think there’s some potential here. People usually think of formal methods as a thing for NASA and academia. A running theme of this blog is that they’re powerful tools for everyday work. I mostly focus on how it applies to backend and concurrent systems, because that’s what I enjoy doing. But it’s more widely useful than that. This is especially important for UI. I don’t think HSCs are necessarily the best possible specification, but it’s a good first step.

Oh hey I’m doing formal methods consulting now. Tell yer boss!