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!news4.google.com!border1.nntp.dca.giganews.com!nntp.giganews.com!wns13feed!worldnet.att.net!attbi_s72.POSTED!53ab2750!not-for-mail From: "Jeffrey R. Carter" Organization: jrcarter at acm dot org User-Agent: Thunderbird 1.5.0.5 (Windows/20060719) MIME-Version: 1.0 Newsgroups: comp.lang.ada Subject: Re: [SPARK] Code safety and information hiding References: In-Reply-To: Content-Type: text/plain; charset=ISO-8859-1; format=flowed Content-Transfer-Encoding: 7bit Message-ID: NNTP-Posting-Host: 12.201.97.176 X-Complaints-To: abuse@mchsi.com X-Trace: attbi_s72 1155757772 12.201.97.176 (Wed, 16 Aug 2006 19:49:32 GMT) NNTP-Posting-Date: Wed, 16 Aug 2006 19:49:32 GMT Date: Wed, 16 Aug 2006 19:49:32 GMT Xref: g2news2.google.com comp.lang.ada:6231 Date: 2006-08-16T19:49:32+00:00 List-Id: Maciej Sobczak wrote: > Consider the following simple SPARK example: > > package Random_Numbers is --# own Seed You need to terminate this with ';'. > type Seed_Type is private; This is never referenced, so may be removed. > procedure Rand(X out Float); --# global Seed This should probably be --# global in out Seed; > --# derives Seed from Seed & X from Seed; > > private -- ... No private part needed, since we've removed Seed_Type. > end Random_Numbers; > > The issue with this example is the apparent strong coupling between > the specification of Rand (of the whole package, in fact) and the > implementation details that pop up in specs in terms of the Seed name > used in annotations. > > 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; The idea is that the spec contains the minimum information needed to reason formally about the behavior of the package. The existence and manipulation of the Seed is necessary for such reasoning. [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.] -- Jeff Carter "This trial is a travesty. It's a travesty of a mockery of a sham of a mockery of a travesty of two mockeries of a sham. ... Do you realize there's not a single homosexual on that jury?" Bananas 27