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: 103376,34257fd17abeba14
X-Google-Attributes: gid103376,public
X-Google-Language: ENGLISH,ASCII-7-bit
Path: 
 g2news2.google.com!postnews.google.com!p79g2000cwp.googlegroups.com!not-for-mail
From: roderick.chapman@googlemail.com
Newsgroups: comp.lang.ada
Subject: Re: Code safety and information hiding
Date: 16 Aug 2006 01:53:12 -0700
Organization: http://groups.google.com
Message-ID: <1155718392.684202.17080@p79g2000cwp.googlegroups.com>
References: <ebuj47$bal$1@sunnews.cern.ch>
NNTP-Posting-Host: 217.205.167.137
Mime-Version: 1.0
Content-Type: text/plain; charset="iso-8859-1"
X-Trace: posting.google.com 1155718397 11611 127.0.0.1 (16 Aug 2006 08:53:17
 GMT)
X-Complaints-To: groups-abuse@google.com
NNTP-Posting-Date: Wed, 16 Aug 2006 08:53:17 +0000 (UTC)
In-Reply-To: <ebuj47$bal$1@sunnews.cern.ch>
User-Agent: G2/0.2
X-HTTP-UserAgent: Mozilla/5.0 (Windows; U; Windows NT 5.1; en-GB;
 rv:1.8.0.6) Gecko/20060728 Firefox/1.5.0.6,gzip(gfe),gzip(gfe)
Complaints-To: groups-abuse@google.com
Injection-Info: p79g2000cwp.googlegroups.com; posting-host=217.205.167.137;
   posting-account=EhC47gwAAABJYiJ7JUJjwDyYMTWH1OKq
Xref: g2news2.google.com comp.lang.ada:6223
Date: 2006-08-16T01:53:12-07:00
List-Id: <comp.lang.ada>

> The issue with this example is the apparent strong coupling between the
> specification of Rand (of the whole package, in fact) and the
> implementation details that pop up in specs in terms of the Seed name
> used in annotations.

SPARK promotes the hiding of _detail_, but not the hiding of
_information_.

The package spec you cite _does_ need to announce the existance of
"Seed" (but not its type, structure, or anything else).  You are also
correct
to identify that choosing the name "Seed" is crucial, since changing it
later
can have a non-trivial impact on clients of this package.

(Put another way - the abstraction offered by the package should be as
simple as it can be but no simpler (cf Occam's rule))

If you removed the announcement of "Seed" altogether, then the only
legal information flow relation for your PRNG would be

 --# derives X from ;

which (in information flow terms) means "The final value of X is a
constant" - not
a very good abstraction of a random number generator! :-)

 Yours,
  Rod Chapman, SPARK Team