Re: [SPARK] Code safety and information hiding

["Jeffrey R. Carter" <spam.not.jrcarter@acm.not.spam.org>]

Maciej Sobczak wrote:
> Consider the following simple SPARK example:
> 
> package Random_Numbers is --# own Seed

You need to terminate this with ';'.

> type Seed_Type is private;

This is never referenced, so may be removed.

> procedure Rand(X out Float); --# global Seed

This should probably be

--# global in out Seed;

> --# derives Seed from Seed & X from Seed;
> 
> private -- ...

No private part needed, since we've removed Seed_Type.

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

No such coupling need exist. Suppose you decide during implementation
that the name of the state variable should really be Fred. This probably
means that you need to revisit the design decisions that lead to
choosing the name Seed, but maybe Seed is a good name for the clients of
the package, but not for the implementation. In that case, the body can
contain

--# own Seed is Fred;

The idea is that the spec contains the minimum information needed to 
reason formally about the behavior of the package. The existence and 
manipulation of the Seed is necessary for such reasoning.

[Aside: I really don't like the use of the term "global" for state 
variables. True global variables (in package specs) should be illegal; 
state variables are a different cup of fish and should not be tainted by 
the "global" label.]

-- 
Jeff Carter
"This trial is a travesty. It's a travesty of a mockery of a
sham of a mockery of a travesty of two mockeries of a sham. ...
Do you realize there's not a single homosexual on that jury?"
Bananas
27