Silly and stupid post‑condition or not ?

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

Hi people out there,

A matter of style or more than style.

I wanted to add a post‑condition to a function to make its specification  
more predictive. The function returns a type à la SML, i.e. instead of a  
boolean status on failure along with an undefined value, it returns a  
record containing nothing. There is an obvious case where it is sure to  
fail, so I wanted to express this obvious behavior in a post‑condition.  
But I can't make up my mind, can't clearly feel if that's simply silly and  
useless wast of source or else.

May I request for your opinion on the simple sample please ? The main  
point is on the function post‑condition at the end.


    type Parsed_Type (Status : Parsed_Status_Type) is record
       case Status is
          when Parsed =>
             Instance : Instance_Type;
          when Format_Error =>
             null;
       end case;
    end record; -- Parsed_Type

    function Parsed (S : String) return Parsed_Type
       with Post =>
         (if S'Length not in Image_Length_Type then
             Parsed'Result.Status = Format_Error);
          -- There may be other failure conditions.


Is such a post‑condition a good or bad practice in your humble or  
authoritative opinion ?

Keep in mind there may be many other cases where “Parsed'Result.Status =  
Format_Error” could be True; the one in the Post is not the only possible  
one.


-- 
“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