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 autolearn=ham
	autolearn_force=no version=3.4.4
X-Google-Thread: 103376,34257fd17abeba14,start
X-Google-Attributes: gid103376,public
X-Google-Language: ENGLISH,ASCII-7-bit
Path: 
 g2news2.google.com!news3.google.com!border1.nntp.dca.giganews.com!nntp.giganews.com!newsfeed00.sul.t-online.de!t-online.de!130.59.10.21.MISMATCH!kanaga.switch.ch!news-zh.switch.ch!switch.ch!cernne03.cern.ch!cern.ch!news
From: Maciej Sobczak <no.spam@no.spam.com>
Newsgroups: comp.lang.ada
Subject: [SPARK] Code safety and information hiding
Date: Wed, 16 Aug 2006 09:56:55 +0200
Organization: CERN - European Laboratory for Particle Physics
Message-ID: <ebuj47$bal$1@sunnews.cern.ch>
NNTP-Posting-Host: abpc10883.cern.ch
Mime-Version: 1.0
Content-Type: text/plain; charset=ISO-8859-2; format=flowed
Content-Transfer-Encoding: 7bit
X-Trace: sunnews.cern.ch 1155715015 11605 (None) 137.138.37.241
X-Complaints-To: news@sunnews.cern.ch
User-Agent: Thunderbird 1.5.0.5 (X11/20060801)
Xref: g2news2.google.com comp.lang.ada:6222
Date: 2006-08-16T09:56:55+02:00
List-Id: <comp.lang.ada>

Consider the following simple SPARK example:

package Random_Numbers is
   --# own Seed

   type Seed_Type is private;

   procedure Rand(X out Float);
   --# global Seed
   --# derives Seed from Seed & X from Seed;

private
   -- ...
end Random_Numbers;


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.
It looks that the dependency between the body and spec is no longer 
one-way, as it logically should be, but the coupling is stronger - I 
cannot even change the name of the own Seed object, because it will 
force me to update the annotations in the specs; which in turn will 
force other packages (which should not depend on what name I use for 
Seed) that depend on these specs to recompile.

I don't find the above to be particularly disturbing, but I'm tempted to 
conclude that in SPARK increased code safety has the price of reduced 
information hiding, which itself was always considered to be a good 
engineering practice.

Your comments are welcome.

-- 
Maciej Sobczak : http://www.msobczak.com/
Programming    : http://www.msobczak.com/prog/