Re: Silly and stupid post-condition or not ?

["Yannick Duchêne (Hibou57)" <yannick_duchene@yahoo.fr>]

Le Fri, 03 Feb 2012 14:18:40 +0100, Dmitry A. Kazakov  
<mailbox@dmitry-kazakov.de> a écrit:
> Supposed to specify the semantics of the operation in terms of the
> parameter and result values. Not in Ada 2012, of course...
It do: the postcondition refers to both F'Result and its parameter, and  
relate both.

> You are confusing the semantics of the language types with the problem
> domain. In the problem domain Format_Error should tell something about  
> the image object, rather than to disallow anything. Your postcondition  
> is not
> to deliver that message.

The type definition for Parsed_Type express the problem domain. Returning  
an access to value and Null when nothing is available was not an option  
(excluded on purpose), and was preferred the SML way to do and defined a  
discriminated record.

The function may returns an instance which was parsed, and will not return  
an instance if the input image is erroneously formated. This is not so  
randomly, the result is always the same for each same input.

Parsed_Type express what the function result can be: either an instance or  
nothing (kind of Null).

Format_Error has nothing to tell except nothing was parsed. If Null was  
not an Ada reserved word, I would have name it simply Null. Its purpose is  
indeed to disallow access to an instance which does not exist. It's there  
in place of any instance, because there is no instance. Just like you  
cannot access any data referred to by a null access: there is no data;  
Null has nothing to tell more, except there is nothing there.

The postcondition act as an indirect precondition. This is not a  
precondition because, first, you cannot refer to F'Result in a  
precondition (would not make sens), second, the function returns in any  
case and never raise an exception.

 From the returned type definition, you have an implicit postcondition: you  
either get an instance or nothing. As Georg explained better than I  
previously did, whatever is the reason for the failure to return a  
non‑null instance, a result meaning nothing was returned is to be dropped  
(the program won't fix any erroneous input, it just can drop). What ever  
the program will know about why there was a failure, this would always be  
the same. A complete postcondition (a complex and long one) could tell  
more, but this, first, would be useless as still resulting in always the  
same behavior, second, as useless this would just be bloat.

But there is still something the postcondition tells, and that's where it  
acts as an indirect pseudo‑precondition: if image's length is out of  
bounds, the program is assured Image will return a kind of Null result  
(but will not raise an exception). Knowledge of this property, is useful  
for any program using this function.

-- 
“Syntactic sugar causes cancer of the semi-colons.” [1]
“Structured Programming supports the law of the excluded muddle.” [1]
[1]: Epigrams on Programming — Alan J. — P. Yale University