← Back to list

Embedding Examples Generator in Specifications

Generating all examples

Marc Petit-Huguenin · 2025-02-15 15:50 · 20 claps · 3.0 min read paywalled
#specifications #testing #formal-verification #confluence
Open on Medium ↗
Wiki topics: RAG · RAG & Retrieval

Embedding an Examples Generator in Specifications

Generating all examples

Fourleaflover/shutterstock.com

Fourleaflover/shutterstock.com

It is established that when confronted to a plain English text that describes something and examples of the same thing, developers tends to build their understanding from the examples and ignore the explanations. This is fine until the examples are incorrect, which happens more often than people think.

The correct way to use examples in a specification is to use them to validate what was learnt by reading the text surrounding it, which does not work if the reader is focused only on these examples. A first line of defense against that problem is to generate the handful of static examples from an underlying formal specification, making it less likely that the text and the examples tell a different story.

But if the goal is really to help the readers validate their understanding of the text, there is no reasons to limit the examples to a small selection. The next step in helping the readers is to let them provide what they think are good and bad examples, and have a piece of code in the specification validating that for them. I call that dynamic examples and that uses something called a test oracle.

It is possible to have both static and dynamic examples in a specification, but an even better idea is to replace the static examples with another piece of code that is embedded in the specification and that can generate all the possible examples:

Here the test oracle verifies that the input (0:) matches the JSON encoded output [""]. Clicking on the Next example button generates the next example and verifies it, thus providing the equivalent to static examples. The reader can still modify the input and output and click on the Validate and verify button, which will check if the reader provided example is correct or not:

Here the input provided does not match the output, so the test oracle detects this, and even provides a corrected example.

Generating all possible examples is not that difficult (the subtitle of this story is a nod to section 7.2.1 of Volume 4A of The Art of Computer Programming, which was an inspiration for that work). This is reminiscent of property-based testing, where the testing software generates valid examples that match a property. Property testing tools generally use a random generator for that, which is fine because a computer will test them as fast as possible, and so the order of the examples are presented does not really matter.

But when presenting examples to a reader, we want we propose first a good sampling of examples that will immediately cover most of the corner cases (the most frightening sentence in software engineering is “this is just a corner case, we can ignore it for now”). The main difficulty is to define what “good sampling” actually means in the presence of a near-infinite or actually infinite (or actually infinite as in the example above) number of possible examples.

The first stepis to transform a infinite series of examples into an infinite series of finite series of examples and parts of examples. Each of these finite series is carefully designed to list first the examples that are more likely to be misunderstood. For instance for a 16 bit signed integer, the list of examples would be something like “0, 1, 32767, -1, -32768, …”.

The second idea is to use something called Cantor’s Zigzag Method. Each of these finite series are combined using that method and because the number of these series is infinite, it generates an infinite series of examples. If the order of each of these finite series really put the most misunderstood parts first, then the few tens first examples should really challenge the user and improve their understanding of that part of the specification.

No technology that cannot explain its results (e.g., LLM) have been involved in the creation of this article.


메타데이터
post_id
94b835cfa4f7
slug
embedding-examples-generator-in-specifications-94b835cfa4f7
url
https://medium.com/@petithug/embedding-examples-generator-in-specifications-94b835cfa4f7
canonical_url
https://medium.com/@petithug/embedding-examples-generator-in-specifications-94b835cfa4f7
author_url
https://medium.com/@petithug
status
ok
fetched_at
2026-06-26 08:21:59