From mboxrd@z Thu Jan 1 00:00:00 1970 X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on polar.synack.me X-Spam-Level: X-Spam-Status: No, score=-0.3 required=5.0 tests=BAYES_00, REPLYTO_WITHOUT_TO_CC autolearn=no autolearn_force=no version=3.4.4 X-Google-Thread: 103376,34257fd17abeba14 X-Google-Attributes: gid103376,public X-Google-Language: ENGLISH,ASCII-7-bit Path: g2news2.google.com!news3.google.com!newsfeed2.dallas1.level3.net!news.level3.com!newsfeed-00.mathworks.com!kanaga.switch.ch!switch.ch!newsserver.news.garr.it!newsserver.cilea.it!docenti.ing.unipi.it!o2943499 From: Colin Paul Gloster Newsgroups: comp.lang.ada Subject: Re: [SPARK] Code safety and information hiding Date: Mon, 21 Aug 2006 13:30:23 +0200 Organization: CILEA Message-ID: <20060821131232.Q662@docenti.ing.unipi.it> References: <%%QFg.913090$084.629274@attbi_s22> Reply-To: Colin Paul Gloster NNTP-Posting-Host: docenti.ing.unipi.it Mime-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII X-Trace: newsserver.cilea.it 1156159826 8981 131.114.28.20 (21 Aug 2006 11:30:26 GMT) X-Complaints-To: news@cilea.it NNTP-Posting-Date: 21 Aug 2006 11:30:26 GMT X-X-Sender: o2943499@docenti.ing.unipi.it In-Reply-To: Xref: g2news2.google.com comp.lang.ada:6294 Date: 2006-08-21T11:30:26+00:00 List-Id: 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