The Specification Language

In Quickstrom, the behavior of a web application is described in a specification language. It’s a propositional temporal logic and functional language, heavily inspired by TLA+ and LTL, most notably adding web-specific operators. The specification language of Quickstrom is based on PureScript.

Like in TLA+, specifications in Quickstrom are based on state machines. A behavior is a finite sequence of states. A step is a tuple of two successive states in a behavior. A specification describes valid behaviors of a web application in terms of valid states and transitions between states.

As in regular PureScript, every expression evaluates to a value. A proposition is a boolean expression in a specification, evaluating to either true or false. A specification that accepts any behavior could therefore be:

module Spec where

proposition = true

... -- more definitions, explained further down

To define a useful specification, though, we need to perform queries and describe how things change over time (using temporal operators).

Queries

Quickstrom provides two ways of querying the DOM in your specification:

  • queryAll

  • queryOne

Both take a CSS selector and a record of element state specifiers, e.g. attributes or properties that you’re interested in.

For example, the following query finds all buttons, including their text contents and disabled flags:

myButtons = queryAll "button" { textContent, disabled }

The type of the above expression is:

Array { textContent :: String, disabled :: Boolean }

You can use regular PureScript function to map, filter, or whatever you’d like, on the array of button records.

In contrast to queryAll returning an Array, queryOne returns a Maybe.

Temporal Operators

In Quickstrom specifications, there are three core temporal operators:

  • next :: forall a. a -> a

  • always :: Boolean -> Boolean

  • until :: Boolean -> Boolean -> Boolean

They change the modality of the sub-expression, i.e. in what state of the recorded behavior it is evaluated.

There are also utility functions built on top of the temporal operators:

  • unchanged :: Eq a => a -> Boolean

Let’s go through the operators and utility functions provided by Quickstrom!

Always

Let’s say we have the following proposition:

proposition = always (title == Just "Home")

title = map _.textContent (queryOne "h1" { textContent })

In every observed state the sub-expression must evaluate to true for the proposition to be true. In this case, the text content of the h1 must always be “Home”.

Until

Until takes two parmeters: the prerequisite condition and the final condition. The prerequisite must hold true in all states until the final condition is true.

proposition = until (loading == Just "loading...") (title == Just "Home")

loading = map _.textContent (queryOne "loading" { textContent })
title = map _.textContent (queryOne "h1" { textContent })

In this case, we presumably load the “Home” text from somewhere else, so we wait until the loading is done, and then assert that the title must be set accordingly.

Unchanged

In addition to the core temporal operators, the unchanged operator is a utility for stating that something does not change:

unchanged :: forall a. Eq a => a -> Boolean
unchanged x = x == next x

It’s useful when expressing state transitions, specifying that a certain queried value should be the same both before and after a particular transition.

For instance, let’s say we have a bunch of top-level definitions, all based on DOM queries, describing a user profile:

userName :: String
userName = ...

userProfileUrl :: String
userProfileUrl = ...

We can say the user profile information should not change in a transition t by passing an array of those values:

t = unchanged [userName, userProfileUrl]
    && ... -- actual changes in transition

Actions

We must instruct Quickstrom what actions it should try. The actions definition in a specification module has the following type:

Array (Tuple Int Action)

It’s an array of pairs, or tuples, where each pair holds a weight and an action specifier. The weight specifies the intended probability of the action being picked, relative to the other actions.

To illustrate, in the following array of actions, the probability of a1 being picked is 40%, while the others are at 20% each. This is assuming all actions are possible at each point an action is being picked.

actions = [
    Tuple 2 a1,
    Tuple 1 a2,
    Tuple 1 a3,
    Tuple 1 a4
  ]

The Action data type is defined in the Quickstrom library, along with some aliases for common actions. For instance, here’s the definition of foci:

-- | Generate focus actions on common focusable elements.
foci :: Actions
foci = [ Tuple 1 (Focus "input"), Tuple 1 (Focus "textarea") ]

More action constructors and aliases should be introduced as Quickstrom evolves.

Note

When specifying complex web applications, one must often carefully pick selectors, actions, and weights, to effectively test enough within a reasonable time. Aliases like clicks and foci might not work well in such situations.