# \[ANN\] Ortac/Wrapper: a new plugin for specification driven unit testing
**URL:** https://discuss.ocaml.org/t/ann-ortac-wrapper-a-new-plugin-for-specification-driven-unit-testing/17304
**Category:** Ecosystem
**Tags:** announce
**Created:** [September 23, 2025, 9:56am UTC](https://discuss.ocaml.org/t/ann-ortac-wrapper-a-new-plugin-for-specification-driven-unit-testing/17304 "2025-09-23T09:56:20Z")
**Posts on this page:** 1
**Page:** 1
### Author:  [@Lucccyo](https://discuss.ocaml.org/u/Lucccyo)
#### Post date: [September 23, 2025, 9:56am UTC](https://discuss.ocaml.org/t/ann-ortac-wrapper-a-new-plugin-for-specification-driven-unit-testing/17304/1 "2025-09-23T09:56:20Z")
Hello everyone,
We, at Tarides, are excited to announce the release of a new plugin for `ortac`: [Ortac/Wrapper](https://github.com/ocaml-gospel/ortac/tree/main/plugins/wrapper)!
This plugin is part of the Gospel project, a contract-based behavioural specification language for OCaml. `ortac` is a tool that converts an OCaml module interface with [Gospel](https://github.com/ocaml-gospel/gospel) specifications into code to check those specifications. There are various ways to check specifications, all provided by plugins, and this post announces the new plugin: Ortac/Wrapper!
This plugin is designed to generate a wrapped module that exposes the same interface as the original module but instruments all function calls with assertions corresponding to the Gospel specifications.
The main objective is to assist with unit testing. You provide the Gospel specification for your file, and Ortac will instrument it. When you run the unit tests on the wrapped version, if a specification is violated, Ortac will crash with an explicit error, telling you which portion of your code is incorrect and which specifications were violated.
This work has been started by Clément Pascutto during his PhD at LMF and Tarides [[Runtime verification of OCaml programs](https://theses.hal.science/tel-04696708v1) ].
I continued his work to support some Gospel features such as the `old` operator and models.
### Installation
To install the Wrapper plugin, use the following command:
`opam install ortac-wrapper`
This will install the following OPAM packages:
- `ortac-core.opam` which provides the `ortac` command-line tool and the core functionalities used by all plugins,
- `ortac-runtime.opam` which provides the support library for the code generated by the Wrapper Ortac plugin,
- `ortac-wrapper.opam` which provides the Wrapper plugin for the `ortac` command-line tool.
#### To automatically generate dune files
If you need dune rules to integrate Ortac into your project, you can install the Dune plugin:
`opam install ortac-dune`
This will install the following OPAM packages:
- `ortac-core.opam` which provides the `ortac` command-line tool and the core functionalities used by all plugins,
- `ortac-dune.opam` which provides the Dune plugin for the `ortac` command-line tool.
### Try it!
Let’s dive into a mini tutorial to see how the Ortac/Wrapper plugin can be used to enhance your unit testing with Gospel specifications. We’ll walk through creating a simple polymorphic container type with limited capacity and see how to specify and test its behavior using Gospel.
#### 1- Define the type and models
First, we define a polymorphic container type `'a t` with Gospel specifications. This type will have a fixed capacity and a mutable list of contents.
```ocaml
type 'a t
(*@ model capacity: int
mutable model contents: 'a list
with t
invariant t.capacity > 0
invariant List.length t.contents <= t.capacity *)
```
Here, we define two models:
- `capacity`: Represents the fixed size of the container.
- `contents`: Represents the mutable list of elements currently stored in the container.
The invariants ensure that the capacity is always positive and that the contents list never exceeds the declared capacity.
#### 2- Specify function behavior
Next, we specify the behavior of functions that manipulate the type `'a t`. We’ll define a `create` function to initialize the container and an `add` function to insert elements into the container.
```ocaml
val create: int -> 'a t
(*@ t = create c
requires c > 0
ensures t.capacity = c
ensures t.contents = [] *)
val add: 'a t -> 'a -> unit
(*@ add t x
modifies t.contents
ensures t.contents = x :: (old t.contents) *)
```
Here the functions `create` and `add` are specified in Gospel.
- The `create` function requires the capacity `c` to be strictly positive and ensures that the model of the new container has the specified capacity and an empty list of contents.
- The `add` function modifies the contents of the container and ensures that the new element `x` is added to the list of contents.
#### 3- Define projection functions
To validate these specifications at runtime, you need to provide projection functions that link OCaml values to their Gospel models. Projection functions can be defined in two ways.
- Using the same name as the model.
- Using a different name, annotated with the attribute `@@projection_for` and the name of its Gospel model.
For our example, we define the projection functions as follows.
```ocaml
val capacity : 'a t -> int
val to_list : 'a t -> 'a list [@@projection_for contents]
```
Where we encounter the two types of naming.
- The `capacity` function directly corresponds to the `capacity` model.
- The `to_seq` function is explicitly declared as the projection for the `contents` model using the `@@projection_for` attribute.
These projection functions are mandatory for the Wrapper plugin to instrument the specifications. If any projection function is missing, nothing will be generated and an error will be printed.
#### 4- Generate the wrapped version
Once you have both of the interface file annotated with Gospel and your implementation, you can start the generation.
If you have installed the `ortac-dune` package (which is recommended), you need to add the following in the dune file where you want to put the tests.
```auto
(rule
(alias runtest)
(mode promote)
(action
(with-stdout-to
dune.wrapper.inc
(setenv
ORTAC_ONLY_PLUGIN
dune-rules
(run ortac dune wrapper )))))
```
This will generate an additional Dune file called `dune.wrapper.inc` that you will need to include once created: `(include dune.wrapper.inc)`. Also, add the name of the wrapped module to the `libraries` stanza of the test folder.
#### 5- Add unit tests
In order to test the `Lib` module, we can now simply write a program using the wrapped version. No need to specify the expected behaviour as the instrumentation will take care of that.
For example, if you run the following program:
```ocaml
open Lib_wrapped
let () =
let q = create 3 in
add q 1;
let q2 = create (-1) in
add q2 1;
()
```
You will obtain the following result:
```auto
File "lib.mli", line 8, characters 0-175:
Runtime error in function `create'
- the pre-condition
`c > 0'
was violated.
Fatal error: exception Ortac_runtime.Error(_)
```
This process helps ensure that your code adheres to the specified behavior, making your unit tests more robust and informative.
### Feel free to report
For more information here is the link of the [dedicated README](https://github.com/ocaml-gospel/ortac/blob/main/plugins/wrapper/README.md).
If you encounter any bugs or misunderstandings, please feel free to report them as an issue on [GitHub](https://github.com/ocaml-gospel/ortac/issues).
We hope this plugin will be useful to you and look forward to your feedback!
### Acknowledgments
This work is partly founded by the ANR grant ANR-22-CE48-0013.