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

---
===========

**This is CFML 1.0, not to be confused with CFML 2.0.**

**CFML 1.0 is expected to be entirely subsumed by CFML 2.0 by the end of 2020.**

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.

For related research papers, see: http://www.chargueraud.org/softs/cfml/

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

CFML 1.0 only works with Coq v8.8. Using OPAM, you might succeed in installing 
CFML using the following commands.

```
   opam repo add coq-released https://coq.inria.fr/opam/released
   opam switch create cfml_switch ocaml-base-compiler.4.07.0
   opam install coq-cfml
```

The exact packages that work are:
coq.8.10.2 coq-aac-tactics.8.10.0 coq-tlc.20181116 coq-cfml.20181201.


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

Once CFML is installed, you can replay the demo from the ICFP script.

```sh
   git clone https://gitlab.inria.fr/charguer/cfml.git
   cd cfml/examples/Tour
   make
   coqide MutableQueue_proof.v UFArray_proof.v
```

or play with files accompanying a tutorial on CFML.

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


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

Some documentation is available in doc/doc.html.
Disclaimer: Pieces of it might be out of date.


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 François Pottier and Armaël Guéneau.