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=-0.3 required=5.0 tests=BAYES_00,DATE_IN_PAST_03_06
	autolearn=no 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,UTF8
Received: by 10.68.73.229 with SMTP id o5mr16739088pbv.7.1328103060661;
        Wed, 01 Feb 2012 05:31:00 -0800 (PST)
Path: 
 lh20ni248572pbb.0!nntp.google.com!news2.google.com!border1.nntp.dca.giganews.com!nntp.giganews.com!npeer02.iad.highwinds-media.com!news.highwinds-media.com!feed-me.highwinds-media.com!post02.iad.highwinds-media.com!news.flashnewsgroups.com-b7.4zTQh5tI3A!not-for-mail
From: Stephen Leake <stephen_leake@stephe-leake.org>
Newsgroups: comp.lang.ada
Subject: Re: Silly and stupid =?utf-8?Q?post=E2=80=91condition?= or
  =?utf-8?Q?not=C2=A0=3F?=
Date: Wed, 01 Feb 2012 03:36:25 -0500
References: <op.v8w6ptk5ule2fv@douda-yannick>
User-Agent: Gnus/5.13 (Gnus v5.13) Emacs/23.2 (windows-nt)
Message-ID: <82wr86fzos.fsf@stephe-leake.org>
Cancel-Lock: sha1:GW3g95Ao2wDf7/bTbHp6IG2Wa5Q=
MIME-Version: 1.0
X-Complaints-To: abuse@flashnewsgroups.com
Organization: FlashNewsgroups.com
X-Trace: 77ba44f293e94e029e66119117
Content-Type: text/plain; charset=utf-8
Content-Transfer-Encoding: 8bit
Date: 2012-02-01T03:36:25-05:00
List-Id: <comp.lang.ada>

"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