[SPARK] Code safety and information hiding

[Maciej Sobczak <no.spam@no.spam.com>]

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/