README.md 1.82 KB
Newer Older
1
# CFML : a tool for proving OCaml programs in Separation Logic
charguer's avatar
charguer committed
2 3 4 5

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

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

9
CFML consists of two parts:
charguer's avatar
charguer committed
10

11 12 13 14 15 16 17
- 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.
18

19
Installation
20 21
============

22
The current version of CFML requires Coq 8.6 or newer.
23 24

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

26
```sh
27 28 29 30
# 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
31 32 33 34 35 36 37 38
```

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
```
39 40 41 42 43 44 45 46 47 48 49 50 51 52

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
```

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

56
Documentation
57 58
============

59
Some documentation can be found in doc/doc.html.
60 61 62 63 64 65 66

Note that it is currently somewhat outdated and needs updating.

License
======

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

68
If you need a more permissive license, please contact the author.
charguer's avatar
charguer committed
69

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