Séminaire Cambium, Inria Paris, 2 rue Simone Iff
                        Salle Emmy Noether, bâtiment A
                          Vendredi 20 octobre, 11h00

                        Samuel Hym et Nicolas Osborne
                                   Tarides

                       Ortac/QCheck-STM 0.1, Gospel 0.2

In this talk, we will present the first usable version of Ortac/QCheck-STM. This
tool can turn some Gospel specifications into tests that those specifications
hold. As the name suggests, the generated tests use the state-machine testing
library QCheck-STM. We will give a demonstration of the tool on a few use cases
and talk about the limitations on which functions can be tested and which
specifications can be translated in that first version.

This work builds on, and extends, Ortac, created by Clément Pascutto. It is a
complete rewrite of a first proof-of-concept developed by Naomi Spargo.

We will also present recent work done on the Gospel tool, leading to a new
release of the `gospel` package. In particular, it now provides a way to
display the Gospel specifications in the odoc documentation. Finally we will
present some of the smaller improvements we have worked on and discuss some
issues we encountered in the development and some other issues reported by
colleagues when they tried those tools.

            Vous pouvez vous abonner à nos annonces de séminaires:
                     http://cambium.inria.fr/seminar.html

             Nos séminaires sont accessibles en ligne en direct
                            via le lien ci-dessus.