Programming with correctness guarantees

oleg@p...
 Andrej Bauer

Joshua D. Guttman

JeanChristophe Filliatre

Robert Fischer
 JeanChristophe Filliatre
 Jacques Carette

Robert Fischer

JeanChristophe Filliatre
 JeanChristophe Filliatre
 David MENTRE
[
Home
]
[ Index:
by date

by threads
]
[ Message by date: previous  next ] [ Message in thread: previous  next ] [ Thread: previous  next ]
[ Message by date: previous  next ] [ Message in thread: previous  next ] [ Thread: previous  next ]
Date:  20070201 (20:57) 
From:  JeanChristophe Filliatre <filliatr@l...> 
Subject:  Re: [Camllist] 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.  JeanChristophe