OCaml used in demonstrations?

Question

I'm looking for examples of usages in OCaml to demonstrate simple properties or theorems. An example may be, given an ocaml definition of binary trees, demonstrate that the maximum number of nodes is 2^(h+1)-1.

I have founds such kind of examples for binary trees and graphs but nothing else.. any suggestion or links?

Answer 1

If you are speaking of proofs written on paper, the usages are essentially the same that with other languages: an informal reasoning based on a reasonable (but not formalized) model of the semantics of the program. To handle your case I would write two functions size and height, and prove by inductive reasoning on the tree that size h <= pow 2 (height h + 1) - 1, using an induction hypothesis on the two subtrees -- I can make this explanation more detailed but prefer to let you do it yourself if you wish.

If you want more formal proofs, there are several approaches.

• Proof techniques based on hoare logics have been adapted to functional programming languages. See for example the 2008 work of Régis-Gianas and Pottier, A Hoare logic for call-by-value functional programs. They provide a formal basis for what can be used, still in hand-written proofs, to give a more rigorous (because down-to-the-metal) proof of your claim. It could also be used in a theorem prover but I'm not sure this approach has been fully worked out yet.

• Another natural approach would be to write your program directly in the Coq proof assistant, whose programming language is mostly a purely functional subset of OCaml, and use its facilities for proving. This is not exactly like writing in OCaml, but quite close; then you can either mirror the implementation in OCaml directly, or use the extraction facility of Coq to get honest-looking OCaml code that has been "compiled" from the Coq program. This approach has been used to formalize the implementation of the balanced binary trees present in the OCaml standard library, and the two implementations (the OCaml one and the Coq one) are sufficiently synchronized that you can transfer results to prove some OCaml-side changes correct.

• In the same vein, there are some attempts to design languages for certified programming that may be more convenient, on some domains, than a general theorem prover such as Coq. Why3 is such a "software verification platform": it defines a programming languages (not very far from OCaml) and a specification language on top of it. You can formulate assertions about your program and verify them using a variety of techniques such as general proof assistants (eg. Coq) or more automated theorem provers (SMT solvers). Why3 strives to support verification of classic imperative-style algorithm implementations, but also support a functional programming style, so it may be an interesting choice for experiments with certified programming if you don't want to go to full-Coq (for example if you're not interested in ensuring termination of your algorithms, which can be inconvenient in Coq).

• Finally, there has been work on the following technique: read your OCaml program and automatically produce a "Coq description" out of it, that you can properties about with the guarantee that what you prove correct also holds in the OCaml implementation. This has been the main result of Arthur Charguéraud's 2010 PhD thesis, where the "Coq description" is based on the technique of "Characteristic fomrulae". He has been able to prove correct ML implementations of relatively sophisticated algorithms such as Union-Find or examples out of the Chris Okasaki's excellent "Purely Functional Data Structures" book.

(I frequently mention the Coq proof assistant; other tools such as Isabelle and Agda are equally suitable, but Coq is closer in syntax to the OCaml language, so is probably a good choice if you want to re-implement ML programs to prove them formally correct.)