Documentation
Literate Specifications

Literate Specification

We have developed a workflow for writing literate, executable formal specs using the tool lmt (opens in a new tab). This allows us to embed the formal specification of a system within informal, natural language specifications, and to extract the formal parts into executable code. This code can then be used for testing or verifying the spec, or fed into a toolchain for model based testing.

Prerequisites

If you use nix, you can use this nix expression (opens in a new tab).

Writing a literate spec

A literate quint spec is a markdown file that includes quint code blocks that declare a file into which the fragment of the code will be extracted.

Here is an example of a literate spec describing a trivial counter system:

<!-- in myspec.md -->
# Counter
 
A counter has a single state variable `n`:
 
```quint myspec.qnt +=
module Counter {
  var n : int
```
 
The initial value of `n` is `0`:
 
```quint myspec.qnt +=
  action init = n' = 0
```
 
At each step, the counter increments the value of `n` by `1`:
 
```quint myspec.qnt +=
  action step = n' = n + 1
}
```
 
If you run a counter for 10 steps, the value of `n` at each step will be equal
to the `i`th step:
 
```quint myspecTests.qnt +=
module TestCounter {
  import Counter.* from "myspec"
 
  run countTest = {
    init.then(10.reps(i => all { step, assert(n == i) }))
  }
}
```

Each code block is labeled with three things:

  • the language of the code block (quint),
  • the file into which the code block will be extracted (e.g. myspec.qnt),
  • the operator +=, which tells lmt to append the content of the code block to the named file.

See the lmt documentation for other features supported by that tool.

Extracting the executable spec and testing it

The following makefile extracts two .qnt files from the markdown using lmt, and then calls quint to run the tests:

.PHONY: test clean

test: myspecTests.qnt myspec.qnt
	quint test --main TestCounter $<

myspec.qnt myspecTests.qnt &: myspec.md
	lmt $<

clean:
	rm myspec.qnt myspecTests.qnt
Secret SantaDesign Principles