On Mon, 15 Sep 2008 10:32:44 -0400 Stefan Monnier <[EMAIL PROTECTED]> 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 _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
