Re: Silly and stupid post‑condition or not ?

[Stephen Leake <stephen_leake@stephe-leake.org>]

"Yannick Duchêne (Hibou57)" <yannick_duchene@yahoo.fr> writes:

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

That means the post condition is misleading, and therefore bad.

--
-- Stephe