diff --git a/docs/obstacle-course.md b/docs/obstacle-course.md new file mode 100644 index 0000000..d53364e --- /dev/null +++ b/docs/obstacle-course.md @@ -0,0 +1,103 @@ +# What a deliberately awkward page taught us + +A public obstacle web page — 40 pages, each built to be hard to automate, +each scoring itself by calling its own `obstacleCompleted()` — was used as a +corpus to find gaps in flowproof's grammar. This is what it found, so the +next person starts from the answers rather than the questions. + +**28 of 40 are solved.** The other 12 are listed with reasons, because +"hard" is not a reason and a gap nobody has named gets rediscovered. + +## What it was actually good for + +Not the score. Four separate defects it surfaced share one shape: + +> an operation answered a NARROWER question than the one asked, and the +> narrower answer was always yes. + +- `is visible` checked that a selector RESOLVED. A `display:none` element + resolves, so the assertion could not fail on the one condition anybody + writes it for. +- A table cell was addressed by counting `th`s against `td`s. A header row + with a stub cell shifts every data cell one place, so the assertion passed + against the neighbouring column — a real cell, with real text. +- `Select` fell through to TYPING when no option matched. Typing into a + `