The Coq mailing list

["Joseph N. Ruskiewicz" <joseph.ruskiewicz AT inf.ethz.ch>]

Jean-Christophe,
   It is good to see a mailing list with good discussion.

   The approach that I will be taking will be from the B side and not 
the C/Java side.

   So, taking a formal method and then generating the proofs into Coq 
for proving.

   Just though I should further clarify.

   I have just started looking into Why and unfortunately don't have 
any comments yet.

Cheers,
Joseph

Jean-Christophe Filliatre wrote:

> Eduardo Gimenez writes:
>
> > 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?).
>
> The  Why input  language  is not  intended  to be  a real  programming
> language;   it  is   more   an  intermediate   language  for   program
> verification. Of  course you can  use the Why language  directly (then
> you are  proving algorithms  rather than real  programs) and  there is
> even an ocaml code output to test your programs.
>
> To  verify  real  programs,  you  need  other  tools  on  top  of  Why
> interpreting  them  into  Why's  own  language.  I  already  mentioned
> Krakatoa for JML-annotated Java programs  and a forthcoming tool for C
> programs. So if you have a  C program to verify, stay tuned. Note that
> the  approach  is quite  different  from the  B  method:  we are  here
> starting  with annotated existing  code instead  of getting  code from
> refinement of an initial specification.
>
> Why  is  already quite  stable  and  provides  everything we  need  to
> interpret Java and C for instance. Beside, we are currently developing
> the following axes: 
>
> - machine arithmetic (integer overflows, floating points)
>
> - use of back-end decision procedures to provide feedback to the user
>  (counter-examples, symbolic testing, etc.)
>
>