Re: [SPARK] Code safety and information hiding

[Colin Paul Gloster <Colin_Paul_Gloster@ACM.org>]

Stephen A. Leake had written:

"[..]
type Distribute_Mode_Type is (Master_Mode, Remote_Mode, Single_Mode);
Distribute_Mode : Distribute_Mode_Type := Single_Mode;
[..]"

Jeffrey R. Carter responded:

"[..]
Again, it must be reasonable and meaningful for me to change the SW to
write this variable whenever it suits me.

If that's not the case, then I claim this should not be a variable.
Instead of being able to write

X.Distribute_Mode := X.Master_Mode;

I should have to call something like

function Request_Distribute_Mode_Change
    (New_Mode : Distribute_Mode_Type)
return Boolean;
-- Request mode change to New_Mode.
-- Returns True if the mode change is legal; False otherwise.

All the details of when a mode change may occur should be encapsulated
with the current mode value.
[..]"



During the next clock cycle it might no longer be legal to change mode.



On Sun, 20 Aug 2006, Stephen Leake wrote:

"[..]

Ah. You want the code to enforce the design rules. That's not possible
in general. Ada allows enforcing some design rules, but not ones at
this level.

In fact, for this particular variable, the rule is "only the
environment task may write to this variable, and only before any other
tasks are started".

People modifying the code must understand the design."


Obviously, if only one task exists which is permitted to write to the 
variable, then a getter and a setter are sufficient, unless someone 
modifies the code so that another task can also write. I accept that you 
have been posting about trying to make it impossible for people to make 
such a modification, and that this is not strictly achievable, but the 
getter and setter methods paradigm is well understood widely when only one 
owner is allowed to call the setter method, so why would you be especially 
worried that someone would not realize this for this simpler example you 
presented?


Stephen Leake has written:

"[..]

Hmm. Now that I think about it, it would be easy to implement a
run-time check for that rule. But it would be a waste of time in the
production system. Might still be worth it; I have other run-time
checks for similar rules (in particular, "symbols must be written
before being read") that are hard to check otherwise.

[..]"

Was simply Ada code run in the application to check the rule meant by 
that, or do you have customized run-time checks in your GNAT run-time 
kernel?

Regards,
Colin Paul Gloster