The Coq mailing list

["Eduardo Gimenez" <Eduardo.Gimenez AT trusted-logic.fr>]

Hi Jean-Cristophe,

> 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).

I would be quite intersted in having a short comparison between the Why tool
and other tools for proving properties
about imperative programs. In particular, I have been asked several times
about the advantages/disadvantages
of Why with respect to the B tool, and specially with respect to the
possibility of extracting C code from the B0 fragment
of B. Jean-Louis Lanet and Ludovic Casset have used such a tool for
generating C code for a bytecode verifier of
Java Card proved in the Atelier B. They claim that the code generated from B
has been directly compiled and
embedded into a smart card, with no modification. Do you think that it would
be possible to do the same using Why
in some near feature? Which are the main development axes of Why today?
(independence from the proof engine, support
for different programming languages like C and Java, others?).
Best wishes,
Eduardo.

----- Original Message ----- 
From: "Jean-Christophe Filliatre" 
<Jean-Christophe.Filliatre AT lri.fr>
To: 
<joseph.ruskiewicz AT inf.ethz.ch>
Cc: 
<coq-club AT pauillac.inria.fr>
Sent: Wednesday, March 17, 2004 9:37 AM
Subject: Re: [Coq-Club] Formal Methods and Coq


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