Re: [SPARK] Code safety and information hiding

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

Jeffrey R. Carter wrote:

>> type Seed_Type is private;
> 
> This is never referenced, so may be removed.

I specifically wrote '-- ...' in the private part to show that it has 
some content, but not relevant to the main point.

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

The private part is needed to define Seed_Type, which was elided as not 
relevant.

But as I've said, it's not relevant. :-)

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

Interesting, but it looks that there is another solution to this: 
refinement. The specification only says that there is some State and the 
body clarifies what are the components of the State. This decouples the 
minor design decisions (like the choice of names in the implementation) 
from the clients, which then only need to know what affects the state - 
now treated in abstract terms - and what doesn't.


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

Agreed. Moreover, SPARK calls "global" even those variables, which are 
actually local in the scope that encloses the definition of the given 
subprogram. Intuitively, "globalness" of some name should not be a 
property of the place where the name is used.


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