Re: Code safety and information hiding

["Stuart" <stuart@0.0>]

To follow up on what Rod has said in reply to:

"Maciej Sobczak" <no.spam@no.spam.com> wrote in message 
news:ebuj47$bal$1@sunnews.cern.ch...

<roderick.chapman@googlemail.com> wrote in message 
news:1155718392.684202.17080@p79g2000cwp.googlegroups.com...

>> 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.

An important point identified by the SPARK annotation is that you have 
chosen to implement it as an Abstract State Machine (single instance shared 
by all clients), rather than an Abstract Data Type that can have multiple 
independent instances (with the Seed as a parameter).

As to the choice of name - I thought that SPARK's data refinement rules 
allowed you to change the view (effectively including the names used) 
between package specification and package body.

>> 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.

Rod's distinction between detail and information is a good one.  It should 
also be remembered that the objective of SPARK is to allow you to reason 
about what your program will do.  Often, in less rigorous design processes, 
you might assume that a subprogram you use has no unexpected consequences 
(e.g. side-effects).  SPARK is much more rigorous - it makes sure that 
subprograms have no side-effects: the consequence is that _all_ effects of a 
subprogram must be recorded (e.g. updating the Seed in the Random number 
example).

Regards
-- 
Stuart Palin