15 Sep
2008
15 Sep
'08
10:32 a.m.
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. Stefan