Re: Silly and stupid post-condition or not ?

[Adam Beneschan <adam@irvine.com>]

On Feb 1, 12:36 am, Stephen Leake <stephen_le...@stephe-leake.org>
wrote:
> "Yannick Duchêne (Hibou57)" <yannick_duch...@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.

I don't see this.  It would be misleading to someone who doesn't
understand the fallacy of the converse, but I'd hope that computer
science students would be taught not to make this mistake by the end
of the first or second year.

                             -- Adam