From mboxrd@z Thu Jan  1 00:00:00 1970
X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on polar.synack.me
X-Spam-Level: 
X-Spam-Status: No, score=-1.9 required=5.0 tests=BAYES_00 autolearn=ham
	autolearn_force=no version=3.4.4
X-Google-Thread: 103376,ad06d2d7cb045687
X-Google-NewGroupId: yes
X-Google-Attributes: gida07f3367d7,domainid0,public,usenet
X-Google-Language: ENGLISH,ASCII
Received: by 10.68.226.10 with SMTP id ro10mr5807490pbc.6.1328113932262;
        Wed, 01 Feb 2012 08:32:12 -0800 (PST)
Path: 
 lh20ni249034pbb.0!nntp.google.com!news2.google.com!postnews.google.com!o4g2000pbc.googlegroups.com!not-for-mail
From: Adam Beneschan <adam@irvine.com>
Newsgroups: comp.lang.ada
Subject: Re: Silly and stupid post-condition or not ?
Date: Wed, 1 Feb 2012 08:30:14 -0800 (PST)
Organization: http://groups.google.com
Message-ID: <5af407fc-2868-44ca-84d2-c51a2a64104d@o4g2000pbc.googlegroups.com>
References: <op.v8w6ptk5ule2fv@douda-yannick>
 <82wr86fzos.fsf@stephe-leake.org>
NNTP-Posting-Host: 66.126.103.122
Mime-Version: 1.0
X-Trace: posting.google.com 1328113932 20483 127.0.0.1 (1 Feb 2012 16:32:12
 GMT)
X-Complaints-To: groups-abuse@google.com
NNTP-Posting-Date: Wed, 1 Feb 2012 16:32:12 +0000 (UTC)
Complaints-To: groups-abuse@google.com
Injection-Info: o4g2000pbc.googlegroups.com; posting-host=66.126.103.122;
 posting-account=duW0ogkAAABjRdnxgLGXDfna0Gc6XqmQ
User-Agent: G2/1.0
X-Google-Web-Client: true
X-Google-Header-Order: ARLUEHNKC
X-HTTP-UserAgent: Mozilla/4.0 (compatible; MSIE 8.0; Windows NT 6.0; WOW64;
 Trident/4.0; SLCC1; .NET CLR 2.0.50727; Media Center PC 5.0; .NET CLR
 3.5.21022; .NET CLR 3.5.30729; .NET CLR 3.0.30618; .NET4.0C),gzip(gfe)
Content-Type: text/plain; charset=ISO-8859-1
Content-Transfer-Encoding: quoted-printable
Date: 2012-02-01T08:30:14-08:00
List-Id: <comp.lang.ada>

On Feb 1, 12:36 am, Stephen Leake <stephen_le...@stephe-leake.org>
wrote:
> "Yannick Duch=EAne (Hibou57)" <yannick_duch...@yahoo.fr> writes:
>
>
>
>
>
> >    type Parsed_Type (Status : Parsed_Status_Type) is record
> >       case Status is
> >          when Parsed =3D>
> >             Instance : Instance_Type;
> >          when Format_Error =3D>
> >             null;
> >       end case;
> >    end record; -- Parsed_Type
>
> >    function Parsed (S : String) return Parsed_Type
> >       with Post =3D>
> >         (if S'Length not in Image_Length_Type then
> >             Parsed'Result.Status =3D 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
> > =3D 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