Re: [SPARK] Code safety and information hiding

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

Maciej Sobczak wrote:
> 
> 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.

Right. That's what I was showing you, in its simplest version.

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

Those are what I called state variables.

-- 
Jeff Carter
"I'm particularly glad that these lovely children were
here today to hear that speech. Not only was it authentic
frontier gibberish, it expressed a courage little seen
in this day and age."
Blazing Saddles
88