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.4 required=5.0 tests=BAYES_00,FORGED_MUA_MOZILLA
	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.74.201 with SMTP id w9mr13481483pbv.0.1328002537204;
        Tue, 31 Jan 2012 01:35:37 -0800 (PST)
Path: 
 lh20ni244322pbb.0!nntp.google.com!news2.google.com!news.glorb.com!de-l.enfer-du-nord.net!feeder2.enfer-du-nord.net!news.imp.ch!newsfeed.tiscali.ch!npeer.de.kpn-eurorings.net!npeer-ng0.de.kpn-eurorings.net!newsfeed.arcor.de!newsspool2.arcor-online.net!news.arcor.de.POSTED!not-for-mail
Date: Tue, 31 Jan 2012 10:35:35 +0100
From: Georg Bauhaus <rm.dash-bauhaus@futureapps.de>
User-Agent: Mozilla/5.0 (Macintosh; Intel Mac OS X 10.6;
 rv:8.0) Gecko/20111105 Thunderbird/8.0
MIME-Version: 1.0
Newsgroups: comp.lang.ada
Subject: Re: Silly and stupid =?UTF-8?B?cG9zdOKAkWNvbmRpdGlvbiBvciBub3TCoA==?=
 =?UTF-8?B?Pw==?=
References: <op.v8w6ptk5ule2fv@douda-yannick>
 <12kegkefstjiy.115bw2vmx23ll.dlg@40tude.net>
In-Reply-To: <12kegkefstjiy.115bw2vmx23ll.dlg@40tude.net>
Message-ID: <4f27b5e8$0$6628$9b4e6d93@newsspool2.arcor-online.net>
Organization: Arcor
NNTP-Posting-Date: 31 Jan 2012 10:35:36 CET
NNTP-Posting-Host: 6c64f044.newsspool2.arcor-online.net
X-Trace: 
 DXC=?KGiBBcedo3U`5g[@c]@J1A9EHlD;3Yc24Fo<]lROoR18kF<OcfhCO;\M8Q7Z_Bh2=PCY\c7>ejV8NdlKh1<FAD5aQ>5PUU0J<=
X-Complaints-To: usenet-abuse@arcor.de
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: 8bit
Date: 2012-01-31T10:35:36+01:00
List-Id: <comp.lang.ada>

On 31.01.12 09:54, Dmitry A. Kazakov wrote:
> 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.

One way to express a "hints only" postcondition is

   with Post => True or  -- yes, mathniks, just FTR:
     (if ... then ...

The idea is that the partial truth, in the shape of a
formal note, can later lead to an improved program
structure.