# CFML : a tool for proving OCaml programs in Separation Logic

Description
===========

CFML is a tool for carrying out proofs of correctness of OCaml programs with
respect to specifications expressed in higher-order Separation Logic.

CFML consists of two parts:

- a tool, implemented in OCaml, parses OCaml source code and generates Coq
  files that contain characteristic formulae, that is, logical descriptions
  of the behavior of the OCaml code.

- a Coq library exports definitions, lemmas, and tactics that are used
  to reason inside Coq about the code. In short, these tactics allow
  the reasoning rules of Separation Logic to be applied to the OCaml code.

Installation
============

The current version of CFML requires Coq 8.6 or newer.

The simplest way of installing the *latest released version* of CFML is via `opam`.

```sh
# This only needs to be done once, to add the opam repository with coq packages
opam repo add coq-released https://coq.inria.fr/opam/released

opam install coq-cfml
```

If instead you wish to use *the development version* of CFML,
then the last line above should be replaced by the following:

```sh
opam pin add coq-cfml https://gitlab.inria.fr/charguer/cfml.git
```

Getting started
============

Once CFML is installed, you can:

- Step through the tutorial. Clone the CFML git repository, then:

```sh
cd cfml/examples/Tuto
make
coqide Tuto_proof.v
```

- Use [cfml-skeleton](https://gitlab.inria.fr/agueneau/cfml-skeleton) to set up a
  new project that uses CFML.

Documentation
============

Some documentation can be found in doc/doc.html.

Note that it is currently somewhat outdated and needs updating.

License
======

All files are distributed under the GNU-GPL v3 license.

If you need a more permissive license, please contact the author.

Authors: Arthur Charguéraud,
with contributions from others.