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,
	REPLYTO_WITHOUT_TO_CC 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.135.231 with SMTP id pv7mr13289258pbb.8.1328000080515;
        Tue, 31 Jan 2012 00:54:40 -0800 (PST)
Path: 
 lh20ni244206pbb.0!nntp.google.com!news1.google.com!goblin1!goblin2!goblin.stu.neva.ru!aioe.org!.POSTED!not-for-mail
From: "Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de>
Newsgroups: comp.lang.ada
Subject: Re:
 =?utf-8?B?U2lsbHkgYW5kIHN0dXBpZCBwb3N04oCRY29uZGl0aW9uIG9yIG5vdMKgPw==?=
Date: Tue, 31 Jan 2012 09:54:03 +0100
Organization: cbb software GmbH
Message-ID: <12kegkefstjiy.115bw2vmx23ll.dlg@40tude.net>
References: <op.v8w6ptk5ule2fv@douda-yannick>
Reply-To: mailbox@dmitry-kazakov.de
NNTP-Posting-Host: FbOMkhMtVLVmu7IwBnt1tw.user.speranza.aioe.org
Mime-Version: 1.0
X-Complaints-To: abuse@aioe.org
User-Agent: 40tude_Dialog/2.0.15.1
X-Notice: Filtered by postfilter v. 0.8.2
Content-Type: text/plain; charset="utf-8"
Content-Transfer-Encoding: 8bit
Date: 2012-01-31T09:54:03+01:00
List-Id: <comp.lang.ada>

On Tue, 31 Jan 2012 00:11:43 +0100, Yannick Duchêne (Hibou57) wrote:

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

I would say it would be a bad practice. The reason is that IMO the
postcondition must be complete, it must tell all truth or nothing. Your
prostcondition is a partial truth, it does not describe all cases when
Status is mandated to be Format_Error.

Yes, it boils down to the implied semantics of the postconditions. If you
consider them mere comments occasionally breaking the program execution by
throwing exceptions at random, then your example might fit into that model.
If you rather view them as contracts, then good contracts should have no
holes.

Note that it is not necessarily about how detailed the semantics is to be
described by pre-/postconditions. I mean, there is a space between
pre-/postconditions suitable for correctness proofs and ones which don't.
You can have the latter if you wish, but still it must be complete. In your
case such a loose postcondition would actually be:

   Status = Format_Error if something is wrong

If you cannot spell that using available means then don't.

-- 
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de