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=-1.9 required=5.0 tests=BAYES_00 autolearn=ham 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!news2.google.com!news.germany.com!feeder.ecngs.de!ecngs!feeder2.ecngs.de!130.59.10.21.MISMATCH!kanaga.switch.ch!news-zh.switch.ch!switch.ch!cernne03.cern.ch!cern.ch!news From: Maciej Sobczak Newsgroups: comp.lang.ada Subject: Re: [SPARK] Code safety and information hiding Date: Thu, 17 Aug 2006 09:01:21 +0200 Organization: CERN - European Laboratory for Particle Physics Message-ID: References: NNTP-Posting-Host: abpc10883.cern.ch Mime-Version: 1.0 Content-Type: text/plain; charset=ISO-8859-1; format=flowed Content-Transfer-Encoding: 7bit X-Trace: sunnews.cern.ch 1155798080 24716 (None) 137.138.37.241 X-Complaints-To: news@sunnews.cern.ch User-Agent: Thunderbird 1.5.0.5 (X11/20060801) In-Reply-To: Xref: g2news2.google.com comp.lang.ada:6237 Date: 2006-08-17T09:01:21+02:00 List-Id: 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/