Re: [Caml-list] Programming with correctness guarantees

[Jean-Christophe Filliatre <filliatr@lri.fr>]

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.

-- 
Jean-Christophe