Releases: ocaml-gospel/ortac
0.7.2
0.7.1
0.7.0
This new release introduces the new Ortac/Wrapper plugin, which includes extended support for projection functions, model-based specifications, and old operator support.
It also fixes some bugs for both the Ortac/Wrapper and Ortac/QCheck-STM plugins.
New introduction of the Ortac/Wrapper plugin
-
Support for
oldoperator
The Ortac/Wrapper plugin now supports theoldoperator in post-conditions,
checking post-conditions mentionning pre-states.
#297 -
Model-based specification support with projection function
-
Improved generated output
Generated files includes a header comment indicating that they were produced by Ortac.
#322 -
Automatic Dune file generation
The Ortac/Dune plugin automatically generatesdunefiles for Ortac/Wrapper plugin.
#314, #335
Tests
-
Test reorganization
Tests for the Ortac/Wrapper plugin have been split into separate files to improve maintainability.
#306 -
Extended test coverage
Several additional tests were added to better cover the Ortac/Wrapper plugin features.
#299
Bug Fixes
-
Ortac/QCheck-STM
-
Ortac/Wrapper
Fixed incorrect error type reporting for violated pre-conditions and post-conditions in generated tests.
#295
0.6.1
0.6.0
0.5.0
0.4.0
This release brings a number of new features and improvements:
- New features:
- Improvements:
0.3.0
This release brings a number of new features and improvements:
- Improvement of the user interface:
- Switch to a module based configuration to simplify the command line
- Release a
duneplugin to generate Dune boilerplate - Overwrite the default
cleanupfunction if there is one defined in the
configuration module
- Extend supported Gospel subset for models:
- Add support for custom ghost type as model: you are no longer limited to
the Gospel standard library to define the model of your OCaml types - Add support for functional type in model: you can use the arrow type as a
model
- Add support for custom ghost type as model: you are no longer limited to
- Extend coverage of generated tests:
- Add support for testing functions without a SUT argument
- Add support for tuples, both as argument and returned value
- Fix:
- Add an error when none of the functions can be tested rather than
generating illegal OCaml code - Handle correctly cast from
inttointegerincluded by Gospel when
computing the expected returned value in failure message - Fix field access translation
- Add an error when none of the functions can be tested rather than
0.2.0
This release brings of number of new features and improvements:
-
Improve test-failure message so that the user knows which part of the Gospel
specification has been violated and get a runnable OCaml program
demonstrating the unexpected behaviour. -
Add support for type invariants so that they are checked at initialisation
and after each function call. -
Add an include option to qcheck-stm cli so that the user can add QCheck
generator andSTM.tytype extension. -
Add a quiet flag
-
Make
--helpand--versionwork even without any plugins installed -
Add a comment warning that the file is generated
-
Check for out of scope variables to avoid generating code that will be
rejected by OCaml compiler. -
Translate constant integer patterns with a guard testing for equality