English version
Accueil     À propos     Téléchargement     Ressources     Contactez-nous    

Ce site est rarement mis à jour. Pour les informations les plus récentes, rendez-vous sur le nouveau site OCaml à l'adresse ocaml.org.

Browse thread
Programming with correctness guarantees
[ Home ] [ Index: by date | by threads ]
[ Search: ]

[ Message by date: previous | next ] [ Message in thread: previous | next ] [ Thread: previous | next ]
Date: 2007-02-01 (20:12)
From: Jean-Christophe Filliatre <filliatr@l...>
Subject: Re: [Caml-list] Programming with correctness guarantees

Joshua D. Guttman writes:
 > oleg@pobox.com writes:
 > >   I remember reading somewhere that after a division of
 > >   Siemens applied this technique to a high assurance
 > >   project, they noted an exhilarating feeling of being
 > >   able to program without unit tests. The code was correct
 > >   by construction.
 > This seems really frightening. 

There's a joke around in the formal methods community: ``would you
prefer to get on a plane whose software has been proved correct or
has been tested?''

More seriously, I heard a similar remark from a French company which
formally verified the embedded code of an automatic subway line (using
the B method). They explained that, after the verification had been
completed, the unit phase was not suppressed, but greatly reduced.