The Coq mailing list

[Jean-Christophe Filliatre <Jean-Christophe.Filliatre AT lri.fr>]

Hello,

As  suggested by  Jean-François there  is  already a  tool called  Why
generating  proof  obligations  from  annotated programs  for  various
provers, including Coq.

Before you try to use it, it  would help to know what kind of programs
you are trying to prove correct.

If  these are  purely functional  programs, I  would suggest  a direct
proof in Coq (together with an extraction of ocaml code from the proof
if  necessary --  see  the Coq  extraction  mechanism if  you are  not
already aware  of its existence).  An example of  such a proof  can be
found  here: http://www.lri.fr/~filliatr/fsets/index.en.html  ;(this is
the correctness proof of the ocaml Set module).

If these are imperative programs, the  Why tool may be indeed what you
need. It  generates proof obligations from  annotated programs written
in a small yet powerful imperative language containing :

- references (over purely functional types)
- while, if-then-else, sequence
- local variables
- functions, possibly recursive and/or local
- exceptions

This language has a caml-like syntax but has strong restrictions w.r.t
ocaml (almost no higher-order,  no polymorphism, no modules, etc.). It
is  rather  a language  specialized  for  Hoare  logic. Though  it  is
powerful enough to interpret for instance the whole Java language in a
suitable model (see http://krakatoa.lri.fr/). A similar interpretation
could be  done for other  languages (we are  currently doing it  for C
programs).

Hope this helps,
--
Jean-Christophe Filliâtre (http://www.lri.fr/~filliatr)


Joseph N. Ruskiewicz writes:
 > Hello Everybody:
 >     I am quite new to both OCaml and Coq.  (2 weeks).
 > 
 >     I am enjoying both of them immensely.
 > 
 >     I would like to implement a formal method front end that will 
 > generate the proof obligations and allow the user to prove them using Coq.
 > 
 >     My question is this:  What is the best way to move forward with this?
 > 
 >     I have investigated a few possibilities and have come up with two 
 > that I would like to pursue.
 >    
 >     1.  using coqmktop, which I have been playing with but not having 
 > much luck.  Any pointers?
 > 
 >     2.  Or using the libraries from Coq and writing a specialized front 
 > end.  I would like to do my pre-parsing and then introduce the user with 
 > the usual Coq input/output (coqtop) with the proof obligations.
 > 
 >     Will any of these work?  Or should I pursue a different path?
 > 
 >     Also, is there any word on when Coq'Art will be purchasable?
 > 
 >    Thank you all.
 > 
 > Joseph
 > --------------------------------------------------------
 > Bug reports: http://coq.inria.fr/bin/coq-bugs
 > Archives: http://pauillac.inria.fr/pipermail/coq-club
 >           http://pauillac.inria.fr/bin/wilma/coq-club
 > Info: http://pauillac.inria.fr/mailman/listinfo/coq-club