Re: Code safety and information hiding

[roderick.chapman@googlemail.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.

(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