On Mon, 15 Sep 2008 10:32:44 -0400
Stefan Monnier
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