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

charguer's avatar
charguer committed
3
---
charguer's avatar
init  
charguer committed
4
5
===========

charguer's avatar
charguer committed
6
**This is CFML 1.0, not to be confused with CFML 2.0.**
charguer's avatar
charguer committed
7

charguer's avatar
charguer committed
8
9
10
11
**CFML 1.0 is expected to be entirely subsumed by CFML 2.0 by the end of 2020.**

Description
===========
charguer's avatar
charguer committed
12

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

16
CFML consists of two parts:
charguer's avatar
init  
charguer committed
17

18
19
20
21
22
23
24
- 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.
25

charguer's avatar
charguer committed
26
27
For related research papers, see: http://www.chargueraud.org/softs/cfml/

28
Installation
29
30
============

charguer's avatar
charguer committed
31
32
CFML 1.0 only works with Coq v8.8. Using OPAM, you might succeed in installing 
CFML using the following commands.
33

34
```
charguer's avatar
charguer committed
35
   opam repo add coq-released https://coq.inria.fr/opam/released
charguer's avatar
charguer committed
36
37
   opam switch create cfml_switch ocaml-base-compiler.4.07.0
   opam install coq-cfml
38
```
39

charguer's avatar
charguer committed
40
41
42
The exact packages that work are:
coq.8.10.2 coq-aac-tactics.8.10.0 coq-tlc.20181116 coq-cfml.20181201.

charguer's avatar
charguer committed
43

44
45
46
Getting started
============

charguer's avatar
charguer committed
47
48
49
50
51
52
53
54
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
```
55

charguer's avatar
charguer committed
56
or play with files accompanying a tutorial on CFML.
57
58

```sh
charguer's avatar
charguer committed
59
60
61
   cd cfml/examples/Tuto
   make
   coqide Tuto_proof.v
62
63
64
```


65
Documentation
66
67
============

charguer's avatar
charguer committed
68
69
Some documentation is available in doc/doc.html.
Disclaimer: Pieces of it might be out of date.
70
71
72
73
74
75


License
======

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

77
If you need a more permissive license, please contact the author.
charguer's avatar
init  
charguer committed
78

79
Authors: Arthur Charguéraud,
charguer's avatar
charguer committed
80
with contributions from François Pottier and Armaël Guéneau.