The Coq mailing list

[Michael Soegtrop <MSoegtrop AT yahoo.de>]

Hi Adam,

> My opinion is that a lot of people think they agree on what "formal 
> specification" means, but it actually means almost nothing and is best 
> to avoid using! Instead, formal methods is all about proving connections 
> between systems, often where one system is markedly simpler than the 
> other and thus easier to build confidence in.

I don't agree with this view. The specifications are supposed to define 
desirable properties of a system, not how these are achieved. These 
specified properties are those which a larger system requires from a 
subsystem.

An arbitrary example:

A specification of a C function doing minimization states that there is 
a tuple of input parameters which may be varied and a goal function 
which maps this tuple to a real number. One can then abstractly define 
the minimum (or infimum) of the goal function over all possible 
parameter tuple values. Then one can specify that the goal function 
applied to the set of parameters the C function returns shall not be 
worse than a well defined increase over this abstract minimum. Such a 
specification has nothing to do with refinement, simplified systems or 
possible implementations. It simply states what it means to minimize 
something and what deviation from perfection is tolerable. In a larger 
context such a specification is more interesting than stating that the 
optimization function behaves approximately like some simplified 
prototype algorithm. To the reader of the specification it tells exactly 
what (s)he can expect from the C code. A comparison with a simplified 
reference implementation wouldn't tell that, unless one analyzes this 
simplified algorithm in detail.

Every reasonable system has a purpose and a specification should 
describe this purpose, not a simplified system which serves this 
purpose. At least in the area I work in (RF), there is always a purpose 
which is much easier to write down than even the most simplistic system 
which could achieve this purpose. The exception is if the purpose is 
"compliance to standard XYZ" and standard XYZ describes a simplified system.

Maybe my view is subjective to my work area, but if you say it is 
frequent that for a systems it is harder to describe its purpose than to 
describe a possible implementation, I would like to discuss a few examples.

Best regards,

Michael