Wiki code snippet testing harness

VerCors supports extracting tests from the tutorial and automatically running the extracted tests. The following syntax is recognized in the tutorial. For example usages of this syntax, see the raw version of the chapter of Axiomatic Data Types. As the annotations will be hidden when viewing the rendered markdown, click on "edit page"

Self-contained code blocks

Testcases defined by template, e.g.:

<!-- testBlock Fail -->
```java
assert false;
```

There are three possible code block annotations:

• testBlock wraps the code in a method and class
• testMethod wraps the code in a class
• test returns the code as is

testBlock and testMethod are compatible with Java and PVL.

The case name of the generated test is derived from the heading structure.

Snippets

To combine multiple code blocks into one test case (potentially with hidden glue code), you can use Snippets. The markdown for that might look like this:

<!-- standaloneSnip smallCase
//:: cases smallCase
//:: verdict Fail
class Test {
-->

<!-- codeSnip smallCase -->
```java
boolean never() {
  return false;
}
```
*Here could be some more explanation about "never".*

<!-- standaloneSnip smallCase
void test() {
-->

Then the following example will **fail**:

<!-- codeSnip smallCase -->
```java
assert never();
```

<!-- standaloneSnip smallCase
}
}
-->

Note that the hidden glue code uses standaloneSnip, and includes the code inside the HTML comment tags <!-- and -->. The visible code snippets use codeSnip, and the code is outside the comment tags, enclosed in triple back-ticks like any displayed code block.