donc@vaxa.isi.edu (Don Cohen) (11/10/90)
I've always thought that a specification is a statement of intent, i.e., it says whatever the specifier considers important. Ideally it should say everything that the specifier wants to say, nothing more, and should be easy to understand. Most often, the IO behavior of a program is what people are interested in, but often it is important to specify such things as timing constraints. It is also conceivable that it might be important to me that the program to do some task be written in Fortran, or that it not use the SQRT function, etc. I don't know any formal languages that are good at all such kinds of specifications, although there are some that are good at describing IO behavior without describing much else. We all know what code is, on the other hand. Clearly the "satisfies" relationship between spec and code is many to many. It is impossible to guess from an implementation which specification it was meant to satisfy. Your attempt to "optimize" an implementation might make it no longer "work" if, say, the purpose of that "useless" loop you removed was to provide a delay.