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,ASCII
Received: by 10.68.226.10 with SMTP id ro10mr4323689pbc.6.1328260387616;
        Fri, 03 Feb 2012 01:13:07 -0800 (PST)
Path: 
 lh20ni255266pbb.0!nntp.google.com!news2.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: Silly and stupid post-condition or not ?
Date: Fri, 3 Feb 2012 10:12:25 +0100
Organization: cbb software GmbH
Message-ID: <1q29nqwr7e7u4.1qrz4gd6twxim.dlg@40tude.net>
References: <op.v8w6ptk5ule2fv@douda-yannick>
 	<82wr86fzos.fsf@stephe-leake.org>
 	<5af407fc-2868-44ca-84d2-c51a2a64104d@o4g2000pbc.googlegroups.com>
 <82k445fu9n.fsf@stephe-leake.org> <jgfulk$gu$1@dont-email.me>
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="iso-8859-1"
Content-Transfer-Encoding: 8bit
Date: 2012-02-03T10:12:25+01:00
List-Id: <comp.lang.ada>

On Fri, 03 Feb 2012 07:26:00 +0100, J-P. Rosen wrote:

> Le 02/02/2012 10:40, Stephen Leake a �crit :
>> I agree with Dmitry; post conditions should be _complete_. If the Ada
>> post condition language is not strong enough to be complete, don't use
>> it; use natural language comments.
>> 
> I don't agree with that. Imagine you need (pre-2012) a type for even
> numbers between 0 and 100.
> Would you declare:
>    type My_Int is range 0..100;
> 
> or would you use Integer, on the ground that since you cannot express
> all of your requirements, you express none?

This example has nothing to do with the issue. Either of these type
declarations is complete. They define the whole set of type values and
operations.

You and Randy confuse a generalized semantics with an undefined one. The
key question is the relation of the variance of the generalized/unspecified
part to the program's behavior. In your example odd values like 1,3 are not
used by the program, or at least supposed to be unused. In the OP example,
Format_Error of unspecified semantics is to be used heavily.

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