In this post I’ll share the results from testing TodoMVC implementations using my new testing tool named WebCheck. I’ll explain how the specification works, what problems were found in the TodoMVC implementations, and what this means for my project.
During the last three months I’ve used my spare time to build WebCheck. It’s a browser testing framework combining ideas from:
In WebCheck, you write a specification for your web application, instead of manually writing test cases. The specification describes the intended behavior as a finite-state machine and invariants, using logic formulae written in a language inspired by the temporal logic of actions (PDF) from TLA+. WebCheck generates hundreds or thousands of tests and runs them to verify if your application is accepted by the specification.
The tests generated by WebCheck are sequences of possible actions, determined from the current state of the DOM at the time of each action. You can think of WebCheck as exploring the state space automatically, based on DOM introspection. It can find user behaviors and problems that we, the biased and lazy humans, are unlikely to think of and to write tests for. Our job is instead to think about the requirements and to improve the specification over time.
In property-based testing, when testing state machines using models, the model should capture the essential complexity of the system under test (SUT). It needs to be functionally complete to be a useful oracle. For a system that is conceptually simple, e.g. a key-value database engine, this is not a problem. But for a system that is inherently complex, e.g. a business application with a big pile of rules, a useful model tends to grow as complex as the system itself.
In WebCheck, the specification is not like such a model. You don’t have to implement a complete functional model of your system. You can leave out details and specify only the most important aspects of your application. As an example, I wrote a specification that states that “there should at no time be more than one spinner on a page”, and nothing else. Again, this is possible to specify in PBT in general, but not with model-based PBT, from what I’ve seen.
Since the start of this project, I’ve used the TodoMVC implementations as a benchmark of WebCheck, and developed a general specification for TodoMVC implementations. The TodoMVC contribution documentation has a high-level feature specification, and the project has a Cypress test suite, but I was curious if I could find anything new using WebCheck.
Early on, checking the mainstream framework implementations, I found that both the Angular and Mithril implementations were rejected by my specification, and I submitted an issue in the TodoMVC issue tracker. Invigorated by the initial success, I decided to check the remaining implementations and gradually improve my specification.
I’ve generalized the specification to work on nearly all the implementations listed on the TodoMVC website. Some of them use the old markup, which uses IDs instead of classes for most elements, so I had to support both variants.
Before looking at the tests results, you might want to have a look at the WebCheck specification that I’ve published as a gist:
The gist includes a brief introduction to the WebCheck specification language and how to write specifications. I’ll write proper documentation for the specification language eventually, but this can give you a taste of how it works, at least. I’ve excluded support for the old TodoMVC markup to keep the specification as simple as possible.
The specification doesn’t cover all features of TodoMVC yet. Most notably, it leaves out the editing mode entirely. Further, it doesn’t cover the usage of local storage in TodoMVC, and local storage is disabled in WebCheck for now.