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:57)
From: Jean-Christophe Filliatre <filliatr@l...>
Subject: Re: [Caml-list] Programming with correctness guarantees

Robert Fischer writes:
 > What, exactly, is the difference between a unit test and formal
 > verification of an application? 

(I hope I don't misunderstand what you mean by "formal verification" here)

At least in its deductive form (i.e. frameworks similar to Hoare
logic), formal verification interprets a program and its specification
as a mathematical formula whose validity implies  the program
correctness. This formula usually includes universal quantifiers, and
thus can only be proved using some logical reasoning, but not testing.

If we consider for instance the following Ocaml code

	let min x y = if x <= y then x else y

and the (incomplete) specification ``forall x y, min x y <= x'' then
the correctness is equivalent to the following formula:

        forall x y, (x <= y implies x <= x) and (x > y implies y <= x)

This is a statement easily established by most automatic provers. Then
there is no need testing function min anymore, since it has been
proved correct for _any_ input values.