Re: [boost] Re: string_algo Formal Review

From: Beman Dawes (bdawes_at_[hidden])
Date: 2003-10-22 08:40:14

At 02:58 AM 10/22/2003, Pavol Droba wrote:

 >On Tue, Oct 21, 2003 at 04:37:06PM -0400, David Abrahams wrote:
 >> You can also make some blanket statements about exceptions, like the
 >> standard does.
 >
 >string_algo library does not throw any exceptions on its own. Only
 >inherited types used by algorithms can do it. But, given the fact that
 >most algorithms are templated, it is not possibly to exactly specify
 >which exception can be thrown.

No, but it is possible to say when exceptions can or can't be thrown, and 
what guarantees are made for the containers when an exception is thrown.

 >So wouldn't it be enought to mention this as a one paragraph in docs?

Yes, if you can write a paragraph that covers all cases.

 >> That leaves you with only preconditions and postconditions, and
 >> exceptions to the blanket statements about exceptions <g> where
 >> appropriate.
 >
 >Is the formal specification of pre/post conditions realy so vital for the
 >usage of the library? Informal specification is given in paramter and
 >result descriptions.

How can a programmer use a function safely without knowing the 
preconditions? Or knowing that there are not preconditions?

The informal specifications currently given often provide no information 
that isn't available by reading the synopsis.  For example:

    Synopsis

    ... trim(ContainerT & Input, ...

    Parameters

    Input
       An input container

    ...

Did the informal description of the Input parameter (which incidentally 
should be named "input", not "Input") tell the reader anything beyond what 
they knew from reading the synopsis?

More formal specifications carry much more useful and precise information. 
Thinking in terms of requirements, concepts, preconditions, exceptions, and 
postconditions (as well as effects and returns) forces the library 
developer to focus on how a function may fail. That results in stronger 
functions.

Having these identifications of failure modes available in the docs alerts 
the user to possible failure cases, and allows the user to avoid them or 
deal with them before they turn into program bugs.

--Beman