Skip to content

Instantly share code, notes, and snippets.

@owickstrom
Last active March 12, 2021 01:19
Show Gist options
  • Save owickstrom/1a0698ef6a47df07dfc1fe59eda12983 to your computer and use it in GitHub Desktop.
Save owickstrom/1a0698ef6a47df07dfc1fe59eda12983 to your computer and use it in GitHub Desktop.
TodoMVC Showdown Specification

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.

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]"
}
}
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment