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,FREEMAIL_FROM
	autolearn=ham autolearn_force=no version=3.4.4
X-Google-Thread: a07f3367d7,43216c2d2bcda533
X-Google-Attributes: gida07f3367d7,public,usenet
X-Google-NewGroupId: yes
X-Google-Language: ENGLISH,ASCII-7-bit
Path: 
 g2news1.google.com!postnews.google.com!u9g2000yqb.googlegroups.com!not-for-mail
From: =?ISO-8859-1?Q?Hibou57_=28Yannick_Duch=EAne=29?=
 <yannick_duchene@yahoo.fr>
Newsgroups: comp.lang.ada
Subject: Re: Specifying the order of ops on an ADT with aspects
Date: Fri, 5 Feb 2010 19:35:58 -0800 (PST)
Organization: http://groups.google.com
Message-ID: <f5252d62-d4bf-440d-b5ce-4b2e39d9cc01@u9g2000yqb.googlegroups.com>
References: <4b6aaed4$0$7625$9b4e6d93@newsspool1.arcor-online.net>
	<91ab6070-fc9e-4575-a967-8fe43353ba26@36g2000yqu.googlegroups.com>
	<hki59g$vjq$1@munin.nbi.dk>
 <a5c90484-a8c0-4ed4-a90a-9ba6fedbcb42@f15g2000yqe.googlegroups.com>
NNTP-Posting-Host: 86.75.149.60
Mime-Version: 1.0
Content-Type: text/plain; charset=ISO-8859-1
X-Trace: posting.google.com 1265427359 19579 127.0.0.1 (6 Feb 2010 03:35:59
 GMT)
X-Complaints-To: groups-abuse@google.com
NNTP-Posting-Date: Sat, 6 Feb 2010 03:35:59 +0000 (UTC)
Complaints-To: groups-abuse@google.com
Injection-Info: u9g2000yqb.googlegroups.com; posting-host=86.75.149.60;
	posting-account=vrfdLAoAAAAauX_3XwyXEwXCWN3A1l8D
User-Agent: G2/1.0
X-HTTP-UserAgent: Mozilla/4.0 (compatible; MSIE 6.0; Windows NT 5.1;
	fr),gzip(gfe),gzip(gfe)
Xref: g2news1.google.com comp.lang.ada:8933
Date: 2010-02-05T19:35:58-08:00
List-Id: <comp.lang.ada>

Side comment.

There is another good side effect of pre-post-conditions, apart their
abilities to better express contracts and to check usages and
implementations conformance : as you define pre-post-conditions, you
see what's needed to define these, so it enforce completeness of ADTs.
With this kind of design, one is less likely to miss a required
function to test an instance of an ADT. Last and although indirectly,
these functions, in turn sometimes makes the need of some associated
procedures more clear.

This is an aid in setting up specifications.