TodoMVC Showdown Specification

intro.md

A Brief Introduction

In WebCheck, the behavior of a web application is specified using a custom specification language based on PureScript. It's a propositional temporal logic and functional language, inspired by the temporal logic of actions (PDF) from TLA+ and linear temporal logic, most notably adding web-specific operators.

Like in TLA+, specifications in WebCheck are based on state machines. A behavior is a 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.

In WebCheck, a syntactic form is called a formula, and every formula evalutes to a value. A proposition is a boolean formula, evaluating to either true or false.

Propositions

The proposition in a WebCheck specification generally takes the form:

proposition = initial && always (transition1 || transition2 || ... || transitionN)

The initial formula specifies the initial state. Each transition specifies a valid step, and generally takes a form like:

transition1 =
    formula1 == next formula1 -- unchanged
    && formula2 `someComparisonWith` next formula2 -- specify relation between the current and next state
    && ...

Formulas are usually defined in terms of DOM queries, where either queryOne or queryAll is used, along with a selector and the relevant attributes, properties, CSS styles, etc:

formula1 = queryAll "ul li" { text: textContent, color: cssValue "background-color" }

In the end, the proposition is one big boolean expression, and it's run on the sequence of observed states to verify a web application's correctness. Expressed with proper academic terms, it's a safety property. WebCheck, being limited to finite behaviors, does not support liveness properties.

The TodoMVC Specification

Now that we've gone through some of the basics, I'm hoping the spec below can make some sense. In the future I'll write real documentation for the WebCheck specification language.

TodoMVC.spec.purs

module WebCheck.PureScript.TodoMVC where

import WebCheck.DSL

import Data.Array (filter, foldMap, head, last, zip)
import Data.Foldable (length)
import Data.Int as Int
import Data.Maybe (Maybe(..), fromMaybe)
import Data.String (Pattern(..), split, trim)
import Data.Tuple (Tuple(..))

-- Start running actions once this selector matches an element.
readyWhen :: Selector
readyWhen = queries.newTodo

-- Actions to draw from, with assigned probabilities.
actions :: Actions
actions = appFoci <> appClicks <> appKeyPresses 
  where
    appClicks = 
      [ Tuple 5 (Click queries.filters.notSelected)
      , Tuple 1 (Click queries.filters.selected)
      , Tuple 1 (Click queries.toggleAll)
      , Tuple 1 (Click queries.destroy)
      ]
    appFoci = [ Tuple 5 (Focus queries.newTodo) ]
    appKeyPresses =
      [ Tuple 5 (keyPress 'a')
      , Tuple 5 (specialKeyPress KeyReturn)
      ]
      
-- The safety property of the specification.
proposition :: Boolean
proposition =
  initial
  && always (enterText
             || addNew
             || changeFilter
             || checkOne
             || uncheckOne
             || delete
             || toggleAll
            )
  && always hasFilters
  where

    initial :: Boolean
    initial =
      (selectedFilter == Nothing || selectedFilter == Just All)
        && (numItems == 0)
        && (pendingText == "")
    
    enterText :: Boolean
    enterText =
      pendingText /= next pendingText
        && itemTexts == next itemTexts
        && selectedFilter == next selectedFilter
    
    changeFilter :: Boolean
    changeFilter =
      case selectedFilter, next selectedFilter of
          Nothing, Just All -> true -- adding the first todo item switches to the All filter
          Nothing, _ -> false -- any other transition from an empty todo list is incorrect
          _, Nothing -> false -- removing the last todo item is not handled by this action
          Just All, _ -> numItems >= next numItems
          _, Just Active -> next (numItemsLeft == Just numUnchecked && numItems == numUnchecked)
          Just f1, Just f2
            | f1 == f2 -> false
            | otherwise -> pendingText == next pendingText
    
    addNew =
      next (pendingText == "")
      && case next selectedFilter of
           Just All -> Just pendingText == next lastItemText
           Just Active -> Just pendingText == next lastItemText
           Just Completed -> itemTexts == next itemTexts
           Nothing -> false

    checkOne =
      pendingText == next pendingText
        && selectedFilter == next selectedFilter
        && (selectedFilter /= Just Completed)
        && ( (selectedFilter == Just All)
                `implies` (numItems == next numItems && numChecked < next numChecked)
            )
        && ( (selectedFilter == Just Active)
                `implies` (numItems > next numItems && numItemsLeft > next numItemsLeft)
            )

    uncheckOne =
      pendingText == next pendingText
        && selectedFilter == next selectedFilter
        && (selectedFilter /= Just Active)
        && ( (selectedFilter == Just All)
                `implies` (numItems == next numItems && numChecked > next numChecked)
            )
        && ( (selectedFilter == Just Completed)
                `implies` (numItems > next numItems && numItemsLeft < next numItemsLeft)
            )
    
    delete =
      pendingText == next pendingText
        && case selectedFilter, numItems of
          _, 1 -> next (numItems == 0)
          Just filter, n -> 
            selectedFilter == next selectedFilter
            && next numItems == n - 1 
            && case filter of
                 All -> true
                 Active -> numItemsLeft == next ((_ - 1) <$> numItemsLeft)
                 Completed -> numItemsLeft == next numItemsLeft
          Nothing, _ -> false

    toggleAll =
      pendingText == next pendingText
        && selectedFilter == next selectedFilter
        && case selectedFilter of
          Just All -> numItems == next numItems && next (numItems == numChecked)
          Just Active -> (numItems > 0) `implies` (next numItems == 0)
                        || (numItems == 0) `implies` (next numItems > 0)
          Just Completed -> numItems + fromMaybe 0 numItemsLeft == (next numItems)
          Nothing -> false
    
    
    selectedFilter = do
      f <- queryOne queries.filters.selected { text: textContent }
      parse f.text
      where
        parse = case _ of
          "All" -> pure All
          "Active" -> pure Active
          "Completed" -> pure Completed
          _ -> Nothing

    hasFilters = 
      case length items, availableFilters of
        0, _ -> true
        _, ["All", "Active", "Completed"] -> true
        _, _ -> false
      where
        availableFilters = map _.textContent (queryAll queries.filters.all { textContent })
    
    items :: Array { text :: String }
    items =
      foldMap (\(Tuple li label) -> if li.display /= "none" then pure label else mempty)
      (zip
        (queryAll queries.items.listItems { display: cssValue "display" })
        (queryAll queries.items.labels { text: textContent }))
    
    itemTexts = map _.text items
    
    lastItemText = last itemTexts
    
    numItems :: Int
    numItems = length items
    
    checkboxes = queryAll queries.items.checkboxes { checked: checked }
    
    numUnchecked :: Int
    numUnchecked = length (filter (not <<< _.checked) checkboxes)
    
    numChecked :: Int
    numChecked = length (filter _.checked checkboxes)
    
    pendingText :: String
    pendingText = case queryOne queries.newTodo { value: value } of
      Just el -> el.value
      Nothing -> ""
    
    numItemsLeft :: Maybe Int
    numItemsLeft = do
      strong <- queryOne queries.todoCount { text: textContent }
      first <- head (split (Pattern " ") (trim strong.text))
      Int.fromString first

data Filter = All | Active | Completed

derive instance eqFilter :: Eq Filter

-- All queries used in this specification.
queries = {
  top: ".todoapp",
  filters: {
    all: ".todoapp .filters a",
    selected: ".todoapp .filters a.selected",
    notSelected: ".todoapp .filters a:not(.selected)"
  },
  destroy: ".todoapp .destroy",
  toggleAll: ".todoapp label[for=toggle-all]",
  newTodo: ".todoapp .new-todo",
  todoCount: ".todoapp .todo-count strong",
  items: {
    listItems: ".todo-list li",
    labels: ".todo-list li label",
    checkboxes: ".todo-list li input[type=checkbox]"
  }
}