[Haskell-cafe] Re: Haskell Weekly News: Issue 85 - September 13, 2008

[Robin Green]

On Mon, 15 Sep 2008 10:32:44 -0400
Stefan Monnier <monnier at iro.umontreal.ca> wrote:

> > A more difficult question is: how do I know that the formal
> > specification I've  written for my program is the right one? Tools
> > can fairly easily check that  your programs conform to a given
> > specification, but they cannot (to my  knowledge) check that your
> > specification says exactly what you want it to say.
> 
> The key is *redundancy*: as long as your property is sufficiently
> different (in structure, in authorship, etc...) you can hope that if
> the spec has a bug, the code will not have a corresponding bug and
> vice versa.  It's only a hope, tho.

There are other meta-level properties one might desire in a
specification, too, such as:

* Simplicity - if a specification is too long-winded, you might not
spot a bug in it because it's too hard to read.

* Definite description - if a specification is a definite description,
it is satisfied by one and only one value (up to functional
equivalence). For example, if I say that a list sorting function must
preserve the length of its input, that's not a definite description,
because it is satisfied by the identity function, as well as a correct
sorting function. However, if I say (in a suitably formal way) that a
sorting function must output a list where every element in the input
occurs the same number of times in the output as it occurs in the
input, and vice-versa, and the output is ordered according to the
specified order - then that *is* a definite description, because any
two functions that follow that specification must be equivalent.

* Reusable (and perhaps reused!) - As in ordinary programming, reuse of
specifications can help avoid errors.

-- 
Robin