The Coq mailing list

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

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

-- 
Jean-Christophe Filliâtre